Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonIIDMultiBatchCumulativeConfidenceRegret

# Finite iid multibatch confidence and cumulative expected regret This module takes a finite Mathlib product of the compiled fixed-policy iid episode-batch law. Each product coordinate receives an equal confidence share. Outside the finite union of pulled-back count events, every batch-specific empirical model has a confidence witness, and the resulting one-episode expected-regret bounds sum over the finite product index. The data-generating policy is fixed across product coordinates. The optimistic policy may depend on its batch, but this is not an adaptive online trajectory law and the cumulative quantity is a sum of expected regrets, not realized cumulative regret.

Module map

Source: BanditRLProof/RL/FiniteHorizonIIDMultiBatchCumulativeConfidenceRegret.lean
Teaching chapter: 9. Finite-horizon reinforcement learning
Declarations: 16
Placeholders: 0

Imports

BanditRLProof.RL.FiniteHorizonIIDAllCoordinateFiniteBatchConfidence, BanditRLProof.ProbabilityUnionBound

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveEpisodeBatchLaw

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

def BanditRLProof.FiniteHorizonRL.multiBatchLocalDelta Compiled

Equal confidence share assigned to every product-batch coordinate.

noncomputable def multiBatchLocalDelta (rounds : Nat) (delta : Real) : Real

Source line 35 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidEpisodeBatchFamilyMeasure Compiled

Finite product of one fixed-policy iid episode-batch law.

noncomputable def iidEpisodeBatchFamilyMeasure {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (rounds episodes : Nat) : Measure (Fin rounds -> EpisodeBatch mdp episodes)

Source line 41 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidEpisodeBatchFamilyMeasure_map_eval Compiled

Every product coordinate has the compiled single-batch marginal law.

theorem iidEpisodeBatchFamilyMeasure_map_eval {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (rounds episodes : Nat) (round : Fin rounds) : (policy.iidEpisodeBatchFamilyMeasure initialState rounds episodes).map (Function.eval round) = policy.iidEpisodeBatchMeasure initialState episodes

Source line 51 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MarkovPolicy.multiBatchRoundBadEvent Compiled

Pullback of one local simultaneous-count event to a product coordinate.

def multiBatchRoundBadEvent {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (rounds episodes : Nat) (delta : Real) (round : Fin rounds) : Set (Fin rounds -> EpisodeBatch mdp episodes)

Source line 64 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MarkovPolicy.multiBatchSimultaneousCountBadEvent Compiled

Union of the local simultaneous-count events over all product batches.

def multiBatchSimultaneousCountBadEvent {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (rounds episodes : Nat) (delta : Real) : Set (Fin rounds -> EpisodeBatch mdp episodes)

Source line 75 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.measurableSet_multiBatchSimultaneousCountBadEvent Compiled

The pulled-back finite union is measurable.

theorem measurableSet_multiBatchSimultaneousCountBadEvent {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (rounds episodes : Nat) (delta : Real) : MeasurableSet (policy.multiBatchSimultaneousCountBadEvent initialState rounds episodes delta)

Source line 85 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidEpisodeBatchFamilyMeasure_roundBadEvent_le Compiled

Each pulled-back local event has its equal-share probability bound.

theorem iidEpisodeBatchFamilyMeasure_roundBadEvent_le {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (rounds : Nat) (hrounds : 0 < rounds) (episodes : Nat) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (round : Fin rounds) : (policy.iidEpisodeBatchFamilyMeasure initialState rounds episodes) (policy.multiBatchRoundBadEvent initialState rounds episodes delta round) <= ENNReal.ofReal (multiBatchLocalDelta rounds delta)

Source line 100 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidEpisodeBatchFamilyMeasure_multiBatchSimultaneousCountBadEvent_le Compiled

Equal-share union over product coordinates retains the global delta.

theorem iidEpisodeBatchFamilyMeasure_multiBatchSimultaneousCountBadEvent_le {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (rounds : Nat) (hrounds : 0 < rounds) (episodes : Nat) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : (policy.iidEpisodeBatchFamilyMeasure initialState rounds episodes) (policy.multiBatchSimultaneousCountBadEvent initialState rounds episodes delta) <= ENNReal.ofReal delta

Source line 133 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidEpisodeBatchFamilyMeasure_rewardConsistent_ae Compiled

Every product batch is reward-consistent almost everywhere.

theorem iidEpisodeBatchFamilyMeasure_rewardConsistent_ae {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (rounds episodes : Nat) : ∀ᵐ batches ∂policy.iidEpisodeBatchFamilyMeasure initialState rounds episodes, ∀ round, (batches round).RewardConsistent

Source line 158 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MarkovPolicy.multiBatchEmpiricalModelAt Compiled

Batch-specific canonical empirical model at one product coordinate.

noncomputable def multiBatchEmpiricalModelAt {mdp : MDP State Action} (_policy : MarkovPolicy mdp) {rounds episodes : Nat} (batches : Fin rounds -> EpisodeBatch mdp episodes) (defaultState : State) (transitionBudget : Real) (round : Fin rounds) : MDP.FiniteBatchModel mdp episodes

Source line 174 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MarkovPolicy.multiBatchCumulativeExpectedRegret Compiled

Sum of batch-specific optimistic-policy expected regrets.

noncomputable def multiBatchCumulativeExpectedRegret {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) {rounds episodes : Nat} (batches : Fin rounds -> EpisodeBatch mdp episodes) (defaultState : State) (transitionBudget : Real) : Real

Source line 183 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MarkovPolicy.multiBatchCumulativeSelectedRadiusOccupancy Compiled

Sum of the batch-specific selected-radius occupancy bounds.

noncomputable def multiBatchCumulativeSelectedRadiusOccupancy {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) {rounds episodes : Nat} (batches : Fin rounds -> EpisodeBatch mdp episodes) (defaultState : State) (transitionBudget : Real) : Real

Source line 192 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MarkovPolicy.allCoordinateConfidenceFamily_of_not_mem Compiled

Pathwise confidence-family producer outside the finite pulled-back bad-event union, assuming the generated reward-consistency support at every coordinate.

noncomputable def allCoordinateConfidenceFamily_of_not_mem {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {rounds episodes : Nat} {delta : Real} (batches : Fin rounds -> EpisodeBatch mdp episodes) (hbatches : batches ∉ policy.multiBatchSimultaneousCountBadEvent initialState rounds episodes delta) (hreward : ∀ round, (batches round).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 (multiBatchLocalDelta rounds delta) < coordinate.expectedCount policy initialState episodes) (hcover : ∀ (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) (action : Action), (∑ nextState, policy.expectedCountTransitionCoordinateRadius initialState episodes (multiBatchLocalDelta rounds delta) (mdp.decisionStageRemaining remaining hremaining) state action nextState * empiricalFiniteBatchValueEnvelope rewardBound transitionBudget remaining) <= transitionBudget) : ∀ round, (policy.multiBatchEmpiricalModelAt batches defaultState transitionBudget round).Confidence

Source line 209 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.confidenceFamily_optimism_and_cumulativeExpectedRegret Compiled

Finite sums preserve all roundwise optimism and expected-regret bounds.

theorem confidenceFamily_optimism_and_cumulativeExpectedRegret {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {rounds episodes : Nat} (batches : Fin rounds -> EpisodeBatch mdp episodes) (defaultState : State) (transitionBudget : Real) (confidence : ∀ round, (policy.multiBatchEmpiricalModelAt batches defaultState transitionBudget round).Confidence) : (∀ round state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (policy.multiBatchEmpiricalModelAt batches defaultState transitionBudget round).plan.upperValueRemaining mdp.horizon le_rfl state) ∧ policy.multiBatchCumulativeExpectedRegret initialState batches defaultState transitionBudget <= policy.multiBatchCumulativeSelectedRadiusOccupancy initialState batches defaultState transitionBudget

Source line 251 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidEpisodeBatchFamily_allCoordinate_finiteBatchModel_confidence Compiled

Mapped finite-product confidence endpoint: one global-delta event and an a.e. family of confidence witnesses, with no measurable witness selection claim.

theorem iidEpisodeBatchFamily_allCoordinate_finiteBatchModel_confidence {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (rounds : Nat) (hrounds : 0 < rounds) (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 (multiBatchLocalDelta rounds delta) < coordinate.expectedCount policy initialState episodes) (hcover : ∀ (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) (action : Action), (∑ nextState, policy.expectedCountTransitionCoordinateRadius initialState episodes (multiBatchLocalDelta rounds delta) (mdp.decisionStageRemaining remaining hremaining) state action nextState * empiricalFiniteBatchValueEnvelope rewardBound transitionBudget remaining) <= transitionBudget) : MeasurableSet (policy.multiBatchSimultaneousCountBadEvent initialState rounds episodes delta) ∧ (policy.iidEpisodeBatchFamilyMeasure initialState rounds episodes) (policy.multiBatchSimultaneousCountBadEvent initialState rounds episodes delta) <= ENNReal.ofReal delta ∧ ∀ᵐ batches ∂policy.iidEpisodeBatchFamilyMeasure initialState rounds episodes, batches ∉ policy.multiBatchSimultaneousCountBadEvent initialState rounds episodes delta -> Nonempty (∀ round, (policy.multiBatchEmpiricalModelAt batches defaultState transitionBudget round).Confidence)

Source line 286 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidEpisodeBatchFamily_allCoordinate_optimism_and_cumulativeExpectedRegret Compiled

Route endpoint: the same finite-product event simultaneously yields optimism for every batch model and the cumulative finite sum of expected-regret bounds.

theorem iidEpisodeBatchFamily_allCoordinate_optimism_and_cumulativeExpectedRegret {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (rounds : Nat) (hrounds : 0 < rounds) (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 (multiBatchLocalDelta rounds delta) < coordinate.expectedCount policy initialState episodes) (hcover : ∀ (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) (action : Action), (∑ nextState, policy.expectedCountTransitionCoordinateRadius initialState episodes (multiBatchLocalDelta rounds delta) (mdp.decisionStageRemaining remaining hremaining) state action nextState * empiricalFiniteBatchValueEnvelope rewardBound transitionBudget remaining) <= transitionBudget) : MeasurableSet (policy.multiBatchSimultaneousCountBadEvent initialState rounds episodes delta) ∧ (policy.iidEpisodeBatchFamilyMeasure initialState rounds episodes) (policy.multiBatchSimultaneousCountBadEvent initialState rounds episodes delta) <= ENNReal.ofReal delta ∧ ∀ᵐ batches ∂policy.iidEpisodeBatchFamilyMeasure initialState rounds episodes, batches ∉ policy.multiBatchSimultaneousCountBadEvent initialState rounds episodes delta -> (∀ round state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (policy.multiBatchEmpiricalModelAt batches defaultState transitionBudget round).plan.upperValueRemaining mdp.horizon le_rfl state) ∧ policy.multiBatchCumulativeExpectedRegret initialState batches defaultState transitionBudget <= policy.multiBatchCumulativeSelectedRadiusOccupancy initialState batches defaultState transitionBudget

Source line 339 Chapter context: Finite-horizon RL