BanditRLProof.RL.FiniteHorizonStochasticRewardIIDAllCoordinateEmpiricalModelConfidence

Reward erasure preserves the state immediately preceding every coordinate.

theorem rewardStepTrace_stateAt_eq_trajectoryStateAt_eraseTrajectory (mdp : MDP State Action) (trajectory : State × RewardStepTrace Action State mdp.horizon) (stage : Fin mdp.horizon) : RewardStepTrace.stateAt trajectory.1 trajectory.2 stage = mdp.trajectoryStateAt (MeanCompatibleRewardKernel.eraseTrajectory (mdp

Sampled and known-reward projections have identical stage states.

theorem sampledEpisodeStep_state_eq_knownRewardEpisodeStep (mdp : MDP State Action) (trajectory : State × RewardStepTrace Action State mdp.horizon) (stage : Fin mdp.horizon) : (mdp.sampledEpisodeStepOfStochasticTrajectory trajectory stage).state = (mdp.episodeStepOfTrajectory (MeanCompatibleRewardKernel.eraseTrajectory (mdp

Sampled and known-reward projections have identical stage actions.

theorem sampledEpisodeStep_action_eq_knownRewardEpisodeStep (mdp : MDP State Action) (trajectory : State × RewardStepTrace Action State mdp.horizon) (stage : Fin mdp.horizon) : (mdp.sampledEpisodeStepOfStochasticTrajectory trajectory stage).action = (mdp.episodeStepOfTrajectory (MeanCompatibleRewardKernel.eraseTrajectory (mdp

Sampled and known-reward projections have identical next states.

theorem sampledEpisodeStep_nextState_eq_knownRewardEpisodeStep (mdp : MDP State Action) (trajectory : State × RewardStepTrace Action State mdp.horizon) (stage : Fin mdp.horizon) : (mdp.sampledEpisodeStepOfStochasticTrajectory trajectory stage).nextState = (mdp.episodeStepOfTrajectory (MeanCompatibleRewardKernel.eraseTrajectory (mdp

Actual sampled-reward and known-reward projections have the same visit counts.

theorem sampledEpisodeBatch_visitCount_eq_knownRewardEpisodeBatch (mdp : MDP State Action) (episodes : Nat) (trajectories : Fin episodes -> State × RewardStepTrace Action State mdp.horizon) (stage : Fin mdp.horizon) (state : State) (action : Action) : (mdp.sampledEpisodeBatchOfStochasticTrajectories episodes trajectories).visitCount stage state action = (MeanCompatibleRewardKernel.knownRewardEpisodeBatchOfStochasticTrajectories (mdp

Actual sampled-reward and known-reward projections have the same transition counts.

theorem sampledEpisodeBatch_transitionCount_eq_knownRewardEpisodeBatch (mdp : MDP State Action) (episodes : Nat) (trajectories : Fin episodes -> State × RewardStepTrace Action State mdp.horizon) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : (mdp.sampledEpisodeBatchOfStochasticTrajectories episodes trajectories).transitionCount stage state action nextState = (MeanCompatibleRewardKernel.knownRewardEpisodeBatchOfStochasticTrajectories (mdp

Count event pulled back along the actual sampled-reward batch projection. Its set is source-independent, while the receiver aligns it with the source's iid stochastic trajectory measure and reward event used by the combined route.

noncomputable def stochasticSampledBatchCountBadEvent (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (delta : Real) : Set (Fin episodes -> State × RewardStepTrace Action State mdp.horizon)

Membership in the sampled and known-reward pullbacks of the count event agrees.

theorem mem_stochasticSampledBatchCountBadEvent_iff_knownReward (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (delta : Real) (trajectories : Fin episodes -> State × RewardStepTrace Action State mdp.horizon) : trajectories ∈ source.stochasticSampledBatchCountBadEvent policy initialState episodes delta ↔ MeanCompatibleRewardKernel.knownRewardEpisodeBatchOfStochasticTrajectories (mdp

The pulled-back sampled-batch count event is measurable.

theorem measurableSet_stochasticSampledBatchCountBadEvent (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (delta : Real) : MeasurableSet (source.stochasticSampledBatchCountBadEvent policy initialState episodes delta)

The actual sampled-batch count event inherits the compiled count failure share.

theorem iidStochasticTrajectoryFamilyMeasure_stochasticSampledBatchCountBadEvent_le (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : (source.iidStochasticTrajectoryFamilyMeasure policy initialState episodes) (source.stochasticSampledBatchCountBadEvent policy initialState episodes delta) <= ENNReal.ofReal delta

Equal reward confidence share for every stage/state/action coordinate.

noncomputable def simultaneousRewardDelta (mdp : MDP State Action) (delta : Real) : Real

Deterministic fixed-coordinate reward-sum confidence radius.

noncomputable def simultaneousRewardSumConfidenceRadius (mdp : MDP State Action) (episodes : Nat) (varianceProxy : NNReal) (delta : Real) : Real

One visit coordinate's sampled-reward deviation event.

noncomputable def rewardCoordinateBadEvent (source : MeanCompatibleRewardKernel mdp) (episodes : Nat) (varianceProxy : NNReal) (delta : Real) (coordinate : VisitCoordinate mdp) : Set (Fin episodes -> State × RewardStepTrace Action State mdp.horizon)

Union of every stage/state/action sampled-reward deviation event.

noncomputable def simultaneousRewardBadEvent (source : MeanCompatibleRewardKernel mdp) (episodes : Nat) (varianceProxy : NNReal) (delta : Real) : Set (Fin episodes -> State × RewardStepTrace Action State mdp.horizon)

Every fixed reward-coordinate event is measurable.

theorem measurableSet_rewardCoordinateBadEvent (source : MeanCompatibleRewardKernel mdp) (episodes : Nat) (varianceProxy : NNReal) (delta : Real) (coordinate : VisitCoordinate mdp) : MeasurableSet (source.rewardCoordinateBadEvent episodes varianceProxy delta coordinate)

The all-coordinate reward union is measurable.

theorem measurableSet_simultaneousRewardBadEvent (source : MeanCompatibleRewardKernel mdp) (episodes : Nat) (varianceProxy : NNReal) (delta : Real) : MeasurableSet (source.simultaneousRewardBadEvent episodes varianceProxy delta)

A nonempty reward-coordinate family receives a positive equal share.

theorem simultaneousRewardDelta_pos (mdp : MDP State Action) (hcoordinate : Nonempty (VisitCoordinate mdp)) {delta : Real} (hdelta : 0 < delta) : 0 < simultaneousRewardDelta mdp delta

A global reward share at most one gives each coordinate a share at most one.

theorem simultaneousRewardDelta_le_one (mdp : MDP State Action) (hcoordinate : Nonempty (VisitCoordinate mdp)) {delta : Real} (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : simultaneousRewardDelta mdp delta <= 1

The finite all-coordinate sampled-reward union consumes only its reward share.

theorem iidStochasticTrajectoryFamilyMeasure_simultaneousRewardBadEvent_le [StandardBorelSpace State] [StandardBorelSpace Action] (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (varianceProxy : NNReal) (law : source.UniformSubgaussianRewardLaw varianceProxy) (htotal : 0 < ((((episodes : NNReal) * varianceProxy : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : (source.iidStochasticTrajectoryFamilyMeasure policy initialState episodes) (source.simultaneousRewardBadEvent episodes varianceProxy delta) <= ENNReal.ofReal delta

Outside the reward union, every masked reward sum is strictly inside its radius.

theorem maskedRewardDeviation_sum_abs_lt_of_not_mem_simultaneousRewardBadEvent (source : MeanCompatibleRewardKernel mdp) {episodes : Nat} {varianceProxy : NNReal} {delta : Real} (trajectories : Fin episodes -> State × RewardStepTrace Action State mdp.horizon) (htrajectories : trajectories ∉ source.simultaneousRewardBadEvent episodes varianceProxy delta) (coordinate : VisitCoordinate mdp) : |∑ episode : Fin episodes, source.maskedRewardDeviationAtEpisode coordinate.stage coordinate.state coordinate.action episode trajectories| < simultaneousRewardSumConfidenceRadius mdp episodes varianceProxy delta

The masked iid reward sum is exactly reward sum minus visit count times mean.

theorem maskedRewardDeviation_sum_eq_sampledBatch_rewardSum_sub (source : MeanCompatibleRewardKernel mdp) {episodes : Nat} (trajectories : Fin episodes -> State × RewardStepTrace Action State mdp.horizon) (stage : Fin mdp.horizon) (state : State) (action : Action) : (∑ episode : Fin episodes, source.maskedRewardDeviationAtEpisode stage state action episode trajectories) = (mdp.sampledEpisodeBatchOfStochasticTrajectories episodes trajectories).rewardSum stage state action - ((mdp.sampledEpisodeBatchOfStochasticTrajectories episodes trajectories).visitCount stage state action : Real) * mdp.reward state action

Deterministic reward-mean radius based on the genuine lower count margin. Its formula is source-independent; the receiver keeps it adjacent to the source-indexed reward event and empirical-reward consumer.

noncomputable def expectedCountRewardCoordinateRadius (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (varianceProxy : NNReal) (countDelta rewardDelta : Real) (coordinate : VisitCoordinate mdp) : Real

Outside both events, a sampled empirical reward obeys its deterministic radius.

theorem sampledBatch_empiricalReward_abs_sub_le_expectedCountRewardCoordinateRadius (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} {varianceProxy : NNReal} {countDelta rewardDelta : Real} (trajectories : Fin episodes -> State × RewardStepTrace Action State mdp.horizon) (hcount : trajectories ∉ source.stochasticSampledBatchCountBadEvent policy initialState episodes countDelta) (hreward : trajectories ∉ source.simultaneousRewardBadEvent episodes varianceProxy rewardDelta) (coordinate : VisitCoordinate mdp) (hmargin : simultaneousCountConfidenceRadius mdp episodes countDelta < coordinate.expectedCount policy initialState episodes) : let batch := mdp.sampledEpisodeBatchOfStochasticTrajectories episodes trajectories |batch.empiricalReward coordinate.stage coordinate.state coordinate.action - mdp.reward coordinate.state coordinate.action| <= source.expectedCountRewardCoordinateRadius policy initialState episodes varianceProxy countDelta rewardDelta coordinate

Linear value envelope with one empirical-reward error and one reward bonus.

def stochasticEmpiricalFiniteBatchValueEnvelope (rewardBound rewardBudget transitionBudget : Real) (remaining : Nat) : Real

Canonical empirical model retaining sampled rewards and fixed reward/transition budgets.

noncomputable def stochasticAllCoordinateEmpiricalFiniteBatchModel (mdp : MDP State Action) (episodes : Nat) (batch : EpisodeBatch mdp episodes) (defaultState : State) (rewardBudget transitionBudget : Real) : FiniteBatchModel mdp episodes where

Reward error and fixed budgets give a noncircular linear optimistic-value envelope.

theorem upperValueRemaining_abs_le (hrewardError : forall stage state action, |batch.empiricalReward stage state action - mdp.reward state action| <= rewardBudget) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (hrewardBudget_nonneg : 0 <= rewardBudget) (htransitionBudget_nonneg : 0 <= transitionBudget) : forall (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State), |(mdp.stochasticAllCoordinateEmpiricalFiniteBatchModel episodes batch defaultState rewardBudget transitionBudget).plan.upperValueRemaining remaining hremaining state| <= stochasticEmpiricalFiniteBatchValueEnvelope rewardBound rewardBudget transitionBudget remaining

Pathwise stochastic sampled-batch producer for the complete confidence object.

noncomputable def stochasticAllCoordinateEmpiricalFiniteBatchModelConfidence_of_not_mem {mdp : MDP State Action} (source : mdp.MeanCompatibleRewardKernel) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} {varianceProxy : NNReal} {countDelta rewardDelta : Real} (trajectories : Fin episodes -> State × RewardStepTrace Action State mdp.horizon) (hcount : trajectories ∉ source.stochasticSampledBatchCountBadEvent policy initialState episodes countDelta) (hreward : trajectories ∉ source.simultaneousRewardBadEvent episodes varianceProxy rewardDelta) (defaultState : State) (rewardBound rewardBudget transitionBudget : Real) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (hrewardBudget_nonneg : 0 <= rewardBudget) (htransitionBudget_nonneg : 0 <= transitionBudget) (hmargin : forall coordinate : VisitCoordinate mdp, simultaneousCountConfidenceRadius mdp episodes countDelta < coordinate.expectedCount policy initialState episodes) (hrewardCover : forall coordinate : VisitCoordinate mdp, source.expectedCountRewardCoordinateRadius policy initialState episodes varianceProxy countDelta rewardDelta coordinate <= rewardBudget) (htransitionCover : forall (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) (action : Action), (∑ nextState, policy.expectedCountTransitionCoordinateRadius initialState episodes countDelta (mdp.decisionStageRemaining remaining hremaining) state action nextState * stochasticEmpiricalFiniteBatchValueEnvelope rewardBound rewardBudget transitionBudget remaining) <= transitionBudget) : (mdp.stochasticAllCoordinateEmpiricalFiniteBatchModel episodes (mdp.sampledEpisodeBatchOfStochasticTrajectories episodes trajectories) defaultState rewardBudget transitionBudget).Confidence

The one bad event used by the stochastic empirical-model route: the pulled-back count event or one of the sampled-reward coordinate events.

noncomputable def stochasticAllCoordinateEmpiricalModelBadEvent (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (varianceProxy : NNReal) (countDelta rewardDelta : Real) : Set (Fin episodes -> State × RewardStepTrace Action State mdp.horizon)

The combined count-and-reward empirical-model event is measurable.

theorem measurableSet_stochasticAllCoordinateEmpiricalModelBadEvent (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (varianceProxy : NNReal) (countDelta rewardDelta : Real) : MeasurableSet (source.stochasticAllCoordinateEmpiricalModelBadEvent policy initialState episodes varianceProxy countDelta rewardDelta)

The two separately calibrated failure shares add under the combined event.

theorem iidStochasticTrajectoryFamilyMeasure_stochasticAllCoordinateEmpiricalModelBadEvent_le [StandardBorelSpace State] [StandardBorelSpace Action] (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (hepisodes : 0 < episodes) (varianceProxy : NNReal) (law : source.UniformSubgaussianRewardLaw varianceProxy) (htotal : 0 < ((((episodes : NNReal) * varianceProxy : NNReal) : Real))) (countDelta : Real) (hcountDelta : 0 < countDelta) (hcountDelta_le_one : countDelta <= 1) (rewardDelta : Real) (hrewardDelta : 0 < rewardDelta) (hrewardDelta_le_one : rewardDelta <= 1) : (source.iidStochasticTrajectoryFamilyMeasure policy initialState episodes) (source.stochasticAllCoordinateEmpiricalModelBadEvent policy initialState episodes varianceProxy countDelta rewardDelta) <= ENNReal.ofReal countDelta + ENNReal.ofReal rewardDelta

The iid stochastic-reward trajectory law produces a measurable all-coordinate confidence event for the empirical model built from the actual sampled rewards.

theorem iidStochasticTrajectoryFamilyMeasure_allCoordinate_finiteBatchModel_confidence [StandardBorelSpace State] [StandardBorelSpace Action] {mdp : MDP State Action} (source : mdp.MeanCompatibleRewardKernel) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (hepisodes : 0 < episodes) (varianceProxy : NNReal) (law : source.UniformSubgaussianRewardLaw varianceProxy) (htotal : 0 < ((((episodes : NNReal) * varianceProxy : NNReal) : Real))) (countDelta : Real) (hcountDelta : 0 < countDelta) (hcountDelta_le_one : countDelta <= 1) (rewardDelta : Real) (hrewardDelta : 0 < rewardDelta) (hrewardDelta_le_one : rewardDelta <= 1) (defaultState : State) (rewardBound rewardBudget transitionBudget : Real) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (hrewardBudget_nonneg : 0 <= rewardBudget) (htransitionBudget_nonneg : 0 <= transitionBudget) (hmargin : forall coordinate : VisitCoordinate mdp, simultaneousCountConfidenceRadius mdp episodes countDelta < coordinate.expectedCount policy initialState episodes) (hrewardCover : forall coordinate : VisitCoordinate mdp, source.expectedCountRewardCoordinateRadius policy initialState episodes varianceProxy countDelta rewardDelta coordinate <= rewardBudget) (htransitionCover : forall (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) (action : Action), (∑ nextState, policy.expectedCountTransitionCoordinateRadius initialState episodes countDelta (mdp.decisionStageRemaining remaining hremaining) state action nextState * stochasticEmpiricalFiniteBatchValueEnvelope rewardBound rewardBudget transitionBudget remaining) <= transitionBudget) : let event := source.stochasticAllCoordinateEmpiricalModelBadEvent policy initialState episodes varianceProxy countDelta rewardDelta MeasurableSet event ∧ (source.iidStochasticTrajectoryFamilyMeasure policy initialState episodes) event <= ENNReal.ofReal countDelta + ENNReal.ofReal rewardDelta ∧ forall trajectories, trajectories ∉ event -> Nonempty (mdp.stochasticAllCoordinateEmpiricalFiniteBatchModel episodes (mdp.sampledEpisodeBatchOfStochasticTrajectories episodes trajectories) defaultState rewardBudget transitionBudget).Confidence

Outside the compiled stochastic empirical-model event, the sampled model is globally optimistic and its recommended policy satisfies the existing selected-radius expected-regret bound.

theorem iidStochasticTrajectoryFamilyMeasure_allCoordinate_optimism_and_expectedRegret [StandardBorelSpace State] [StandardBorelSpace Action] {mdp : MDP State Action} (source : mdp.MeanCompatibleRewardKernel) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (hepisodes : 0 < episodes) (varianceProxy : NNReal) (law : source.UniformSubgaussianRewardLaw varianceProxy) (htotal : 0 < ((((episodes : NNReal) * varianceProxy : NNReal) : Real))) (countDelta : Real) (hcountDelta : 0 < countDelta) (hcountDelta_le_one : countDelta <= 1) (rewardDelta : Real) (hrewardDelta : 0 < rewardDelta) (hrewardDelta_le_one : rewardDelta <= 1) (defaultState : State) (rewardBound rewardBudget transitionBudget : Real) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (hrewardBudget_nonneg : 0 <= rewardBudget) (htransitionBudget_nonneg : 0 <= transitionBudget) (hmargin : forall coordinate : VisitCoordinate mdp, simultaneousCountConfidenceRadius mdp episodes countDelta < coordinate.expectedCount policy initialState episodes) (hrewardCover : forall coordinate : VisitCoordinate mdp, source.expectedCountRewardCoordinateRadius policy initialState episodes varianceProxy countDelta rewardDelta coordinate <= rewardBudget) (htransitionCover : forall (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) (action : Action), (∑ nextState, policy.expectedCountTransitionCoordinateRadius initialState episodes countDelta (mdp.decisionStageRemaining remaining hremaining) state action nextState * stochasticEmpiricalFiniteBatchValueEnvelope rewardBound rewardBudget transitionBudget remaining) <= transitionBudget) : let event := source.stochasticAllCoordinateEmpiricalModelBadEvent policy initialState episodes varianceProxy countDelta rewardDelta MeasurableSet event ∧ (source.iidStochasticTrajectoryFamilyMeasure policy initialState episodes) event <= ENNReal.ofReal countDelta + ENNReal.ofReal rewardDelta ∧ forall trajectories, trajectories ∉ event -> let model := mdp.stochasticAllCoordinateEmpiricalFiniteBatchModel episodes (mdp.sampledEpisodeBatchOfStochasticTrajectories episodes trajectories) defaultState rewardBudget transitionBudget (forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= model.plan.upperValueRemaining mdp.horizon le_rfl state) ∧ model.plan.optimisticPolicy.expectedRegret initialState <= model.plan.optimisticPolicy.occupancySumRemaining (fun remaining hremaining state => 2 * model.plan.selectedRadiusRemaining remaining hremaining state) mdp.horizon le_rfl initialState