BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIMartingaleTuning

Tuned Bellman-innovation tail for canonical recurrent UCBVI-CH.

Module map

Declarations
6
Placeholders
0

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.

noncomputable def bellmanInnovationThreshold (mdp : MDP State Action) (episodes : Nat) (delta : Real) : Real
Source line 22 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.bellmanInnovationTilt Compiled

Chernoff tilt optimized for the deterministic `K H^3` variance budget.

noncomputable def bellmanInnovationTilt (mdp : MDP State Action) (episodes : Nat) (delta : Real) : Real
Source line 29 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.bellmanInnovationThreshold_nonneg Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem bellmanInnovationThreshold_nonneg (mdp : MDP State Action) (episodes : Nat) (delta : Real) : 0 <= bellmanInnovationThreshold (State
Source line 35 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.bellmanInnovationTilt_pos Compiled

No declaration docstring is present; use the chapter context and exact statement below.

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
Source line 46 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.bellmanInnovationTilt_exponent_le_neg_two_logFactor Compiled

No declaration docstring is present; use the chapter context and exact statement below.

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
Source line 66 Chapter context: Finite-horizon RL
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`.

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
Source line 105 Open teaching explanation Chapter context: Finite-horizon RL