BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVISimultaneousConfidence

One peeled singleton-transition query. `count` encodes the positive actual visit count `count + 1`.

structure BernsteinCoordinateIndex (mdp : MDP State Action) (episodes : Nat) where

One peeled optimal-tail scalar query.

structure OptimalTailIndex (mdp : MDP State Action) (episodes : Nat) where

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)

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)

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)

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

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

noncomputable def functionalTilt (logBudget visitBudget : Real) : Real

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

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

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

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

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

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)