BanditRLProof.RL.FiniteHorizonIIDAllCoordinateFiniteBatchConfidence

Explicit noncircular envelope for a fixed reward and transition budget.

def empiricalFiniteBatchValueEnvelope (rewardBound transitionBudget : Real) (remaining : Nat) : Real

Canonical empirical model for the all-coordinate route: exact generated rewards use radius zero, while every transition coordinate shares one fixed budget.

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

Deterministic lower-margin coordinate radius based on the genuine visit mean.

noncomputable def expectedCountTransitionCoordinateRadius {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (delta : Real) (stage : Fin mdp.horizon) (state : State) (action : Action) (_nextState : State) : Real

Outside the simultaneous event, realized count exceeds its deterministic lower margin.

theorem expectedCount_sub_radius_lt_count_of_not_mem_simultaneousCountBadEvent {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} {delta : Real} (batch : EpisodeBatch mdp episodes) (hbatch : batch ∉ policy.simultaneousCountBadEvent initialState episodes delta) (coordinate : VisitCoordinate mdp) : coordinate.expectedCount policy initialState episodes - simultaneousCountConfidenceRadius mdp episodes delta < (coordinate.count batch : Real)

The random-denominator transition error is bounded by the deterministic expected-count lower-margin radius.

theorem empiricalTransitionMass_abs_sub_transition_le_expectedCountRadius_of_not_mem {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} {delta : Real} (batch : EpisodeBatch mdp episodes) (hbatch : batch ∉ policy.simultaneousCountBadEvent initialState episodes delta) (defaultState : State) (coordinate : VisitCoordinate mdp) (hmargin : simultaneousCountConfidenceRadius mdp episodes delta < coordinate.expectedCount policy initialState episodes) (nextState : State) : |batch.empiricalTransitionMass defaultState coordinate.stage coordinate.state coordinate.action nextState - (mdp.transition (coordinate.state, coordinate.action)).real {nextState}| ≤ policy.expectedCountTransitionCoordinateRadius initialState episodes delta coordinate.stage coordinate.state coordinate.action nextState

Full-coordinate margins make every reward-consistent empirical reward exact.

theorem empiricalReward_eq_of_not_mem_simultaneousCountBadEvent {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} {delta : Real} (batch : EpisodeBatch mdp episodes) (hbatch : batch ∉ policy.simultaneousCountBadEvent initialState episodes delta) (hreward : batch.RewardConsistent) (hmargin : ∀ coordinate : VisitCoordinate mdp, simultaneousCountConfidenceRadius mdp episodes delta < coordinate.expectedCount policy initialState episodes) (stage : Fin mdp.horizon) (state : State) (action : Action) : batch.empiricalReward stage state action = mdp.reward state action

Exact empirical rewards and fixed nonnegative budgets give the explicit linear absolute envelope for every recursive optimistic value.

theorem upperValueRemaining_abs_le (hrewardExact : ∀ stage state action, batch.empiricalReward stage state action = mdp.reward state action) (hrewardBound : ∀ state action, |mdp.reward state action| ≤ rewardBound) (htransitionBudget_nonneg : 0 ≤ transitionBudget) : ∀ (remaining : Nat) (hremaining : remaining ≤ mdp.horizon) (state : State), |(mdp.allCoordinateEmpiricalFiniteBatchModel episodes batch defaultState transitionBudget).plan.upperValueRemaining remaining hremaining state| ≤ empiricalFiniteBatchValueEnvelope rewardBound transitionBudget remaining

Pathwise producer: full genuine occupancy margins, deterministic radius cover, and reward consistency construct the complete raw finite-batch confidence object.

noncomputable def allCoordinateEmpiricalFiniteBatchModelConfidence_of_not_mem {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} {delta : Real} (batch : EpisodeBatch mdp episodes) (hbatch : batch ∉ policy.simultaneousCountBadEvent initialState episodes delta) (hreward : batch.RewardConsistent) (defaultState : State) (rewardBound transitionBudget : Real) (hrewardBound : ∀ state action, |mdp.reward state action| ≤ rewardBound) (htransitionBudget_nonneg : 0 ≤ transitionBudget) (hmargin : ∀ coordinate : VisitCoordinate mdp, simultaneousCountConfidenceRadius mdp episodes delta < coordinate.expectedCount policy initialState episodes) (hcover : ∀ (remaining : Nat) (hremaining : remaining + 1 ≤ mdp.horizon) (state : State) (action : Action), (∑ nextState, policy.expectedCountTransitionCoordinateRadius initialState episodes delta (mdp.decisionStageRemaining remaining hremaining) state action nextState * empiricalFiniteBatchValueEnvelope rewardBound transitionBudget remaining) ≤ transitionBudget) : (mdp.allCoordinateEmpiricalFiniteBatchModel episodes batch defaultState transitionBudget).Confidence where

Mapped-iid confidence endpoint with the unchanged simultaneous-event failure budget. No additional reward or confidence event is introduced.

theorem iidEpisodeBatch_allCoordinate_finiteBatchModel_confidence {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta ≤ 1) (defaultState : State) (rewardBound transitionBudget : Real) (hrewardBound : ∀ state action, |mdp.reward state action| ≤ rewardBound) (htransitionBudget_nonneg : 0 ≤ transitionBudget) (hmargin : ∀ coordinate : VisitCoordinate mdp, simultaneousCountConfidenceRadius mdp episodes delta < coordinate.expectedCount policy initialState episodes) (hcover : ∀ (remaining : Nat) (hremaining : remaining + 1 ≤ mdp.horizon) (state : State) (action : Action), (∑ nextState, policy.expectedCountTransitionCoordinateRadius initialState episodes delta (mdp.decisionStageRemaining remaining hremaining) state action nextState * empiricalFiniteBatchValueEnvelope rewardBound transitionBudget remaining) ≤ transitionBudget) : MeasurableSet (policy.simultaneousCountBadEvent initialState episodes delta) ∧ (policy.iidEpisodeBatchMeasure initialState episodes) (policy.simultaneousCountBadEvent initialState episodes delta) ≤ ENNReal.ofReal delta ∧ ∀ᵐ batch ∂policy.iidEpisodeBatchMeasure initialState episodes, batch ∉ policy.simultaneousCountBadEvent initialState episodes delta → Nonempty (mdp.allCoordinateEmpiricalFiniteBatchModel episodes batch defaultState transitionBudget).Confidence

The produced confidence object immediately yields global optimism and the existing selected-radius single-episode expected-regret bound almost everywhere.

theorem iidEpisodeBatch_allCoordinate_optimism_and_expectedRegret {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta ≤ 1) (defaultState : State) (rewardBound transitionBudget : Real) (hrewardBound : ∀ state action, |mdp.reward state action| ≤ rewardBound) (htransitionBudget_nonneg : 0 ≤ transitionBudget) (hmargin : ∀ coordinate : VisitCoordinate mdp, simultaneousCountConfidenceRadius mdp episodes delta < coordinate.expectedCount policy initialState episodes) (hcover : ∀ (remaining : Nat) (hremaining : remaining + 1 ≤ mdp.horizon) (state : State) (action : Action), (∑ nextState, policy.expectedCountTransitionCoordinateRadius initialState episodes delta (mdp.decisionStageRemaining remaining hremaining) state action nextState * empiricalFiniteBatchValueEnvelope rewardBound transitionBudget remaining) ≤ transitionBudget) : MeasurableSet (policy.simultaneousCountBadEvent initialState episodes delta) ∧ (policy.iidEpisodeBatchMeasure initialState episodes) (policy.simultaneousCountBadEvent initialState episodes delta) ≤ ENNReal.ofReal delta ∧ ∀ᵐ batch ∂policy.iidEpisodeBatchMeasure initialState episodes, batch ∉ policy.simultaneousCountBadEvent initialState episodes delta → let model := mdp.allCoordinateEmpiricalFiniteBatchModel episodes batch defaultState transitionBudget (∀ 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