BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.Lean-verified build · exact declarations linked.

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIProbabilityBudget

Paper-scale probability arithmetic for canonical recurrent UCBVI-CH.

Module map

Declarations
7
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVISimultaneousConfidence, BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIAlignment

Imported by

BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIMartingaleTuning

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.card_bernsteinCoordinateIndex 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 identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.card_bernsteinCoordinateIndex

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem card_bernsteinCoordinateIndex (mdp : MDP State Action) (episodes : Nat) : Fintype.card (BernsteinCoordinateIndex mdp episodes) = episodes * Fintype.card State * Fintype.card Action * Fintype.card State * (episodes * mdp.horizon)
Source line 22 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.card_optimalTailIndex 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 identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.card_optimalTailIndex

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem card_optimalTailIndex (mdp : MDP State Action) (episodes : Nat) : Fintype.card (OptimalTailIndex mdp episodes) = episodes * mdp.horizon * Fintype.card State * Fintype.card Action * (episodes * mdp.horizon)
Source line 40 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.exp_neg_two_mul_logFactor_eq Compiled

Exact exponential simplification at the paper logarithmic factor.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.exp_neg_two_mul_logFactor_eq

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem exp_neg_two_mul_logFactor_eq (mdp : MDP State Action) (episodes : Nat) (delta : Real) (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : Real.exp (-2 * logFactor (State := State) (Action := Action) mdp episodes delta) = (delta / (confidenceNumerator (State := State) (Action := Action) mdp episodes : Nat)) ^ 2
Source line 60 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.exp_neg_two_mul_logFactor_sq_le Compiled

The optimal-tail scalar term is no larger than the coordinate term because the task log factor is at least one.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.exp_neg_two_mul_logFactor_sq_le

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem exp_neg_two_mul_logFactor_sq_le (mdp : MDP State Action) (episodes : Nat) (delta : Real) (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : Real.exp (-2 * logFactor (State := State) (Action := Action) mdp episodes delta ^ 2) <= Real.exp (-2 * logFactor (State := State) (Action := Action) mdp episodes delta)
Source line 90 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.ofReal_card_mul_two_mul_exp_le Compiled Internal helper

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 identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.ofReal_card_mul_two_mul_exp_le

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

private theorem ofReal_card_mul_two_mul_exp_le (card : Nat) (x budget : Real) (hx : 0 <= x) (hbudget : 0 <= budget) (h : (card : Real) * (2 * x) <= budget) : (card : ENNReal) * (2 * ENNReal.ofReal x) <= ENNReal.ofReal budget
Source line 103 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.simultaneousTransitionTailBudget_le_fifth Compiled

The complete coordinate-plus-optimal-tail confidence family consumes at most one fifth of `delta`.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.simultaneousTransitionTailBudget_le_fifth

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem simultaneousTransitionTailBudget_le_fifth (mdp : MDP State Action) (episodes : Nat) (delta : Real) (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : (Fintype.card (BernsteinCoordinateIndex mdp episodes) : ENNReal) * (2 * ENNReal.ofReal (Real.exp (-2 * logFactor (State := State) (Action := Action) mdp episodes delta))) + (Fintype.card (OptimalTailIndex mdp episodes) : ENNReal) * (2 * ENNReal.ofReal (Real.exp (-2 * logFactor (State := State) (Action := Action) mdp episodes delta ^ 2))) <= ENNReal.ofReal (delta / 5)
Source line 118 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.recurrentSource_trajectoryMeasure_simultaneousTransitionFailureEvent_le_fifth Compiled

Specialized same-source confidence event probability.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.recurrentSource_trajectoryMeasure_simultaneousTransitionFailureEvent_le_fifth

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem recurrentSource_trajectoryMeasure_simultaneousTransitionFailureEvent_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) (hreward : ∀ state action, |mdp.reward state action| <= 1) : let source := recurrentSource mdp initialState defaultState episodes delta source.trajectoryMeasure (AdaptiveEpisodeBatchSource.simultaneousTransitionFailureEvent source episodes (logFactor (State := State) (Action := Action) mdp episodes delta)) <= ENNReal.ofReal (delta / 5)
Source line 234 Open teaching explanation Chapter context: Finite-horizon RL