Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIMartingaleTuning
Tuned Bellman-innovation tail for canonical recurrent UCBVI-CH.
Module map
Imports
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIProbabilityBudget
Imported by
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVITerminal
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.bellmanInnovationThreshold
Compiled
Bellman-martingale charge used in the frozen `20/250` terminal.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.bellmanInnovationThresholdReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def bellmanInnovationThreshold (mdp : MDP State Action) (episodes : Nat) (delta : Real) : Real
def
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.bellmanInnovationTilt
Compiled
Chernoff tilt optimized for the deterministic `K H^3` variance budget.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.bellmanInnovationTiltReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def bellmanInnovationTilt (mdp : MDP State Action) (episodes : Nat) (delta : Real) : Real
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.bellmanInnovationThreshold_nonneg
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.bellmanInnovationThreshold_nonnegReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem bellmanInnovationThreshold_nonneg (mdp : MDP State Action) (episodes : Nat) (delta : Real) : 0 <= bellmanInnovationThreshold (State := State) (Action := Action) mdp episodes delta
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.bellmanInnovationTilt_pos
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.bellmanInnovationTilt_posReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem bellmanInnovationTilt_pos (mdp : MDP State Action) (episodes : Nat) (delta : Real) (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : 0 < bellmanInnovationTilt (State := State) (Action := Action) mdp episodes delta
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.bellmanInnovationTilt_exponent_le_neg_two_logFactor
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.bellmanInnovationTilt_exponent_le_neg_two_logFactorReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem bellmanInnovationTilt_exponent_le_neg_two_logFactor (mdp : MDP State Action) (episodes : Nat) (delta : Real) (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : -bellmanInnovationTilt (State := State) (Action := Action) mdp episodes delta * bellmanInnovationThreshold (State := State) (Action := Action) mdp episodes delta + (bellmanInnovationTilt (State := State) (Action := Action) mdp episodes delta ^ 2 / 8) * ((episodes : Real) * ((mdp.horizon : Real) * (mdp.horizon : Real) ^ 2)) <= -2 * logFactor (State := State) (Action := Action) mdp episodes delta
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.recurrentSource_trajectoryMeasure_bellmanInnovation_sum_ge_threshold_le_fifth
Compiled
The tuned Bellman-innovation tail consumes at most one fifth of `delta`.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.recurrentSource_trajectoryMeasure_bellmanInnovation_sum_ge_threshold_le_fifthReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem recurrentSource_trajectoryMeasure_bellmanInnovation_sum_ge_threshold_le_fifth (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) : let source := recurrentSource mdp initialState defaultState episodes delta source.trajectoryMeasure {trajectory | bellmanInnovationThreshold (State := State) (Action := Action) mdp episodes delta <= (Finset.range episodes).sum (fun round => recurrentBellmanInnovationProcess mdp defaultState episodes delta round trajectory)} <= ENNReal.ofReal (delta / 5)