Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIExpectedRegret
# Expected regret of the canonical generated Hoeffding UCBVI-CH source This file first closes the small measurability bridge from the recurrent finite table to policy-value pseudo-regret. It then integrates the compiled high-probability terminal, charging the deterministic `K H` envelope only on the measurable hull of the proved failure event. The resulting corollary therefore retains the required `K H delta` term.
Module map
Imports
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVITerminal
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.measurable_generatedPolicyTable
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem measurable_generatedPolicyTable (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (episode : Nat) : Measurable (fun trajectory : EpisodeBatchTrajectory mdp 1 => generatedPolicyTable mdp defaultState episodes delta trajectory episode)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.measurable_generatedEpisodeInitialState
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem measurable_generatedEpisodeInitialState (mdp : MDP State Action) (defaultState : State) : Measurable (generatedEpisodeInitialState mdp defaultState)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.measurable_generatedEpisodePseudoRegret
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem measurable_generatedEpisodePseudoRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (defaultState : State) (episodes : Nat) (delta : Real) (episode : Nat) : Measurable (fun trajectory : EpisodeBatchTrajectory mdp 1 => generatedEpisodePseudoRegret (recurrentSource mdp initialState defaultState episodes delta) defaultState trajectory episode)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.measurable_cumulativeEpisodePseudoRegret
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem measurable_cumulativeEpisodePseudoRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (defaultState : State) (episodes : Nat) (delta : Real) : Measurable (fun trajectory : EpisodeBatchTrajectory mdp 1 => cumulativeEpisodePseudoRegret (recurrentSource mdp initialState defaultState episodes delta) defaultState episodes trajectory)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.integral_cumulativeEpisodePseudoRegret_recurrentSource_le_canonicalRegretBound_add_failure
Compiled
Canonical finite-time expected pseudo-regret. The `K H delta` summand is the explicit contribution of the proved terminal failure event.
theorem integral_cumulativeEpisodePseudoRegret_recurrentSource_le_canonicalRegretBound_add_failure (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 ∫ trajectory, cumulativeEpisodePseudoRegret source defaultState episodes trajectory ∂source.trajectoryMeasure <= canonicalRegretBound (State