Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVITerminal
# Canonical generated Hoeffding UCBVI-CH terminal The terminal below uses one recurrent source, its exact `Kernel.trajMeasure`, the confidence family proved on that law, the policy-value regret generated by the same strict-prefix planner, and no caller-supplied confidence premise.
Module map
Imports
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIMartingaleTuning
Imported by
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIExpectedRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.canonicalRegretBound
Compiled
Frozen Azar--Osband--Munos-shaped Hoeffding UCBVI-CH bound.
noncomputable def canonicalRegretBound (mdp : MDP State Action) (episodes : Nat) (delta : Real) : Real
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.canonicalRegretBound_nonneg
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem canonicalRegretBound_nonneg (mdp : MDP State Action) (episodes : Nat) (delta : Real) : 0 <= canonicalRegretBound (State
def
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.alignmentFailureEvent
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
noncomputable def alignmentFailureEvent (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) : Set (EpisodeBatchTrajectory mdp 1)
def
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.canonicalFailureEvent
Compiled
Complete terminal failure set: same-source confidence, Bellman innovation, and the measure-zero generated-record alignment complement.
noncomputable def canonicalFailureEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (defaultState : State) (episodes : Nat) (delta : Real) : Set (EpisodeBatchTrajectory mdp 1)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.recurrentSource_trajectoryMeasure_alignmentFailureEvent_eq_zero
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem recurrentSource_trajectoryMeasure_alignmentFailureEvent_eq_zero (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (defaultState : State) (episodes : Nat) (delta : Real) (hhorizon : 0 < mdp.horizon) : (recurrentSource mdp initialState defaultState episodes delta).trajectoryMeasure (alignmentFailureEvent mdp defaultState episodes delta) = 0
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.recurrentSource_trajectoryMeasure_canonicalFailureEvent_le
Compiled
The complete generated terminal failure set costs at most `delta`.
theorem recurrentSource_trajectoryMeasure_canonicalFailureEvent_le (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace (EpisodeBatch mdp 1)] [StandardBorelSpace (EpisodeBatchTrajectory mdp 1)] (defaultState : State) (episodes : Nat) (delta : Real) (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hrewardNonneg : ∀ state action, 0 <= mdp.reward state action) (hrewardOne : ∀ state action, mdp.reward state action <= 1) : (recurrentSource mdp initialState defaultState episodes delta).trajectoryMeasure (canonicalFailureEvent (initialState
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.sum_shift_recurrentBellmanInnovation_eq
Compiled Internal helper
No declaration docstring is present; use the chapter context and exact statement below.
private theorem sum_shift_recurrentBellmanInnovation_eq (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) : (Finset.range (episodes - 1)).sum (fun n => recurrentBellmanInnovationProcess mdp defaultState episodes delta (n + 1) trajectory) = (Finset.range episodes).sum (fun round => recurrentBellmanInnovationProcess mdp defaultState episodes delta round trajectory)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.sqrt_totalSteps_mul_card_eq_paper
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sqrt_totalSteps_mul_card_eq_paper (mdp : MDP State Action) (episodes : Nat) : Real.sqrt (totalSteps mdp episodes : Nat) * Real.sqrt ((Fintype.card State * Fintype.card Action : Nat) : Real) = Real.sqrt mdp.horizon * Real.sqrt ((Fintype.card State : Real) * Fintype.card Action * episodes)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.cumulativeEpisodePseudoRegret_le_canonicalRegretBound_of_not_mem
Compiled
Pathwise generated regret bound outside the proved terminal failure set.
theorem cumulativeEpisodePseudoRegret_le_canonicalRegretBound_of_not_mem (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (defaultState : State) (episodes : Nat) (delta : Real) (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hrewardNonneg : ∀ state action, 0 <= mdp.reward state action) (hrewardOne : ∀ state action, mdp.reward state action <= 1) (trajectory : EpisodeBatchTrajectory mdp 1) (htrajectory : trajectory ∉ canonicalFailureEvent (initialState
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.recurrentSource_trajectoryMeasure_cumulativeEpisodePseudoRegret_gt_canonicalRegretBound_le
Compiled
Canonical generated-policy high-probability regret terminal.
theorem recurrentSource_trajectoryMeasure_cumulativeEpisodePseudoRegret_gt_canonicalRegretBound_le (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace (EpisodeBatch mdp 1)] [StandardBorelSpace (EpisodeBatchTrajectory mdp 1)] (defaultState : State) (episodes : Nat) (delta : Real) (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hrewardNonneg : ∀ state action, 0 <= mdp.reward state action) (hrewardOne : ∀ state action, mdp.reward state action <= 1) : let source := recurrentSource mdp initialState defaultState episodes delta source.trajectoryMeasure {trajectory | canonicalRegretBound (State