Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVISimultaneousConfidence
# Finite same-source confidence family for cumulative UCBVI-CH The family contains two genuinely generated transition coordinates: every next-state singleton, with its Bernoulli variance; and the normalized optimal continuation value at every stage. The second coordinate is not postulated as an external confidence premise. It is proved from the same recursive episode source and is linked to the singleton residual family by the exact finite linear identity in `FiniteHorizonAdaptiveCumulativeUCBVITransitionValueConfidence`.
Module map
Imports
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIConfidenceTuning, BanditRLProof.ProbabilityUnionBound
Imported by
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIOptimalTailAlignment, BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIProbabilityBudget
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
structure
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.BernsteinCoordinateIndex
Compiled
One peeled singleton-transition query. `count` encodes the positive actual visit count `count + 1`.
structure BernsteinCoordinateIndex (mdp : MDP State Action) (episodes : Nat) where
structure
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.OptimalTailIndex
Compiled
One peeled optimal-tail scalar query.
structure OptimalTailIndex (mdp : MDP State Action) (episodes : Nat) where
def
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.AdaptiveEpisodeBatchSource.bernsteinCoordinateFailureEvent
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
noncomputable def bernsteinCoordinateFailureEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (logBudget : Real) (index : BernsteinCoordinateIndex mdp episodes) : Set (EpisodeBatchTrajectory mdp 1)
def
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.AdaptiveEpisodeBatchSource.optimalTailFailureEvent
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
noncomputable def optimalTailFailureEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (logBudget : Real) (index : OptimalTailIndex mdp episodes) : Set (EpisodeBatchTrajectory mdp 1)
def
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.AdaptiveEpisodeBatchSource.simultaneousTransitionFailureEvent
Compiled
The complete finite same-source transition confidence failure set.
noncomputable def simultaneousTransitionFailureEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (episodes : Nat) (logBudget : Real) : Set (EpisodeBatchTrajectory mdp 1)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.AdaptiveEpisodeBatchSource.trajectoryMeasure_bernsteinCoordinateFailureEvent_le
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem trajectoryMeasure_bernsteinCoordinateFailureEvent_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] [StandardBorelSpace (EpisodeBatch mdp 1)] [StandardBorelSpace (EpisodeBatchTrajectory mdp 1)] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (logBudget : Real) (hlog : 0 < logBudget) (index : BernsteinCoordinateIndex mdp episodes) : source.trajectoryMeasure (bernsteinCoordinateFailureEvent source logBudget index) <= 2 * ENNReal.ofReal (Real.exp (-2 * logBudget))
def
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.AdaptiveEpisodeBatchSource.functionalTilt
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
noncomputable def functionalTilt (logBudget visitBudget : Real) : Real
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.AdaptiveEpisodeBatchSource.functionalTilt_pos
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem functionalTilt_pos {logBudget visitBudget : Real} (hlog : 0 < logBudget) (hvisit : 0 < visitBudget) : 0 < functionalTilt logBudget visitBudget
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.AdaptiveEpisodeBatchSource.functionalTilt_exponent_eq
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem functionalTilt_exponent_eq {logBudget visitBudget : Real} (hvisit : 0 < visitBudget) : -functionalTilt logBudget visitBudget * (logBudget * Real.sqrt visitBudget) + (functionalTilt logBudget visitBudget ^ 2 / 8) * visitBudget = -2 * logBudget ^ 2
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.AdaptiveEpisodeBatchSource.trajectoryMeasure_optimalTailFailureEvent_le
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem trajectoryMeasure_optimalTailFailureEvent_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] [StandardBorelSpace (EpisodeBatch mdp 1)] [StandardBorelSpace (EpisodeBatchTrajectory mdp 1)] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (hreward : ∀ state action, |mdp.reward state action| <= 1) (logBudget : Real) (hlog : 0 < logBudget) (index : OptimalTailIndex mdp episodes) : source.trajectoryMeasure (optimalTailFailureEvent source logBudget index) <= 2 * ENNReal.ofReal (Real.exp (-2 * logBudget ^ 2))
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.AdaptiveEpisodeBatchSource.trajectoryMeasure_simultaneousTransitionFailureEvent_le
Compiled
A transparent finite-union bound. The later UCBVI specialization proves that the displayed right hand side is at most its allotted fraction of `delta`; keeping this intermediate theorem exact makes the event accounting auditable.
theorem trajectoryMeasure_simultaneousTransitionFailureEvent_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] [StandardBorelSpace (EpisodeBatch mdp 1)] [StandardBorelSpace (EpisodeBatchTrajectory mdp 1)] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (hreward : ∀ state action, |mdp.reward state action| <= 1) (episodes : Nat) (logBudget : Real) (hlog : 0 < logBudget) : source.trajectoryMeasure (simultaneousTransitionFailureEvent source episodes logBudget) <= (Fintype.card (BernsteinCoordinateIndex mdp episodes) : ENNReal) * (2 * ENNReal.ofReal (Real.exp (-2 * logBudget))) + (Fintype.card (OptimalTailIndex mdp episodes) : ENNReal) * (2 * ENNReal.ofReal (Real.exp (-2 * logBudget ^ 2)))
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.AdaptiveEpisodeBatchSource.abs_coordinateResidual_lt_of_not_mem_simultaneousTransitionFailureEvent
Compiled
Outside the joint event, every peeled singleton residual is strictly below its variance-sensitive threshold whenever the peel equals the actual count.
theorem abs_coordinateResidual_lt_of_not_mem_simultaneousTransitionFailureEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) {episodes : Nat} {logBudget : Real} {trajectory : EpisodeBatchTrajectory mdp 1} (htrajectory : trajectory ∉ simultaneousTransitionFailureEvent source episodes logBudget) (index : BernsteinCoordinateIndex mdp episodes) (hcount : (∑ i ∈ Finset.range (index.round + 1), source.aggregateVisitIncrement index.state index.action i trajectory) = (index.count + 1 : Nat)) : |∑ i ∈ Finset.range (index.round + 1), source.aggregateTransitionResidualIncrement index.state index.action index.nextState i trajectory| < bernsteinCoordinateThreshold logBudget (mdp.transitionCoordinateVariance index.state index.action index.nextState * (index.count + 1 : Nat))
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.AdaptiveEpisodeBatchSource.abs_optimalTailResidual_lt_of_not_mem_simultaneousTransitionFailureEvent
Compiled
The sharp optimal-tail scalar coordinate is extracted from the same joint event, again at its exact actual-count peel.
theorem abs_optimalTailResidual_lt_of_not_mem_simultaneousTransitionFailureEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) {episodes : Nat} {logBudget : Real} {trajectory : EpisodeBatchTrajectory mdp 1} (htrajectory : trajectory ∉ simultaneousTransitionFailureEvent source episodes logBudget) (index : OptimalTailIndex mdp episodes) (hcount : (∑ i ∈ Finset.range (index.round + 1), source.aggregateVisitIncrement index.state index.action i trajectory) = (index.count + 1 : Nat)) : |∑ i ∈ Finset.range (index.round + 1), source.aggregateTransitionFunctionalResidualIncrement (mdp.optimalTailProbe index.stage) index.state index.action i trajectory| < logBudget * Real.sqrt (index.count + 1 : Nat)