Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIRecurrentOptimism
Bellman optimism for every queried policy of the one recurrent source.
Module map
Imports
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIOptimism
Imported by
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIEpisodeRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.cumulativeSummaryOfSequence_prefixTransitionSummaries_eq
Compiled
The planner fold and the statistical state use literally the same prefix transition summary.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.cumulativeSummaryOfSequence_prefixTransitionSummaries_eqReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem cumulativeSummaryOfSequence_prefixTransitionSummaries_eq {mdp : MDP State Action} (trajectory : EpisodeBatchTrajectory mdp 1) (round : Nat) : cumulativeSummaryOfSequence (prefixTransitionSummaries (Preorder.frestrictLe round trajectory)) = (adaptiveCumulativeEmpiricalModelStateAt trajectory round).1
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.AdaptiveEpisodeBatchSource.recurrentQTableOfTrajectory_dominatesOptimal
Compiled
Every finite Q-table fold through the first `n` actually generated episodes is optimistic on the proved same-source event.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.AdaptiveEpisodeBatchSource.recurrentQTableOfTrajectory_dominatesOptimalReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem recurrentQTableOfTrajectory_dominatesOptimal {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) {episodes : Nat} {delta : Real} {trajectory : EpisodeBatchTrajectory mdp 1} (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) (htrajectory : trajectory ∉ simultaneousTransitionFailureEvent source episodes (logFactor (State := State) (Action := Action) mdp episodes delta)) (defaultState : State) : ∀ n, n <= episodes -> QDominatesOptimal mdp (recurrentQTableOfSummaries mdp defaultState (scale (State := State) (Action := Action) mdp episodes delta) n (fun i => (trajectory i).transitionCountSummary))
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.AdaptiveEpisodeBatchSource.recurrentSuccessor_selectedQ_ge_optimalQ
Compiled
The generated successor episode selects an action whose actual recurrent Q value dominates every optimal action value.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.AdaptiveEpisodeBatchSource.recurrentSuccessor_selectedQ_ge_optimalQReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem recurrentSuccessor_selectedQ_ge_optimalQ {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) {episodes : Nat} {delta : Real} {trajectory : EpisodeBatchTrajectory mdp 1} (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) (htrajectory : trajectory ∉ simultaneousTransitionFailureEvent source episodes (logFactor (State := State) (Action := Action) mdp episodes delta)) (defaultState : State) (round : Fin episodes) (stage : Fin mdp.horizon) (state : State) (action : Action) : optimalQAt mdp stage state action <= recurrentQTableOfSummaries mdp defaultState (scale (State := State) (Action := Action) mdp episodes delta) (round + 1) (fun i => (trajectory i).transitionCountSummary) stage state (recurrentPolicyTableOfSummaries mdp defaultState (scale (State := State) (Action := Action) mdp episodes delta) (round + 1) (fun i => (trajectory i).transitionCountSummary) stage state)