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.
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.
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
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.
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