Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIExpectedRegret
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.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.measurable_generatedPolicyTableReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.measurable_generatedEpisodeInitialStateReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.measurable_generatedEpisodePseudoRegretReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.measurable_cumulativeEpisodePseudoRegretReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Indexed settings: Finite-horizon tabular reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.integral_cumulativeEpisodePseudoRegret_recurrentSource_le_canonicalRegretBound_add_failureReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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 := State) (Action := Action) mdp episodes delta + (episodes : Real) * mdp.horizon * delta