BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIBernsteinConfidence

True Bernoulli variance of one transition singleton.

noncomputable def transitionCoordinateVariance (mdp : MDP State Action) (state : State) (action : Action) (nextState : State) : Real

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

theorem transitionCoordinateVariance_nonneg (mdp : MDP State Action) (state : State) (action : Action) (nextState : State) : 0 <= mdp.transitionCoordinateVariance state action nextState

A centered transition indicator has exact second moment `p(1-p)`.

theorem integral_sq_indicator_sub_transitionMass (mdp : MDP State Action) (state : State) (action : Action) (nextState : State) : (∫ y, ((if y = nextState then 1 else 0) - (mdp.transition (state, action)).real {nextState}) ^ 2 ∂mdp.transition (state, action)) = mdp.transitionCoordinateVariance state action nextState

The visited transition singleton has a variance-sensitive compensated MGF. The hard `|tilt| <= 1` contract is the standard Bernstein small-tilt range.

theorem transitionResidualHead_variance_compensated_hasMGFUpperBoundAt (mdp : MDP State Action) (targetState : State) (targetAction : Action) (targetNextState : State) (currentState : State) (chosenAction : Action) (tilt : Real) (htilt : |tilt| <= 1) : Concentration.HasMGFUpperBoundAt (fun nextState => tilt * mdp.transitionResidualHead targetState targetAction targetNextState currentState (chosenAction, nextState) - tilt ^ 2 * mdp.transitionCoordinateVariance targetState targetAction targetNextState * mdp.transitionVisitHead targetState targetAction currentState (chosenAction, nextState)) 1 0 (mdp.transition (currentState, chosenAction))

The generated action/transition head preserves the exact coordinate variance compensator.

theorem actionStateKernel_transitionResidualHead_variance_compensated_hasMGFUpperBoundAt (mdp : MDP State Action) (policy : MarkovPolicy mdp) (targetState : State) (targetAction : Action) (targetNextState : State) (currentState : State) (stage : Fin mdp.horizon) (tilt : Real) (htilt : |tilt| <= 1) : Concentration.HasMGFUpperBoundAt (fun head : Action × State => tilt * mdp.transitionResidualHead targetState targetAction targetNextState currentState head - tilt ^ 2 * mdp.transitionCoordinateVariance targetState targetAction targetNextState * mdp.transitionVisitHead targetState targetAction currentState head) 1 0 (policy.actionStateKernel stage currentState)

The entire generated episode trace has the exact coordinate-variance compensator, with the compensating count equal to literal visits.

theorem trajectoryKernelRemaining_transitionResidual_variance_compensated_hasMGFUpperBoundAt (mdp : MDP State Action) (policy : MarkovPolicy mdp) (targetState : State) (targetAction : Action) (targetNextState : State) (tilt : Real) (htilt : |tilt| <= 1) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (currentState : State) : Concentration.HasMGFUpperBoundAt (fun trace => tilt * mdp.transitionResidualFrom targetState targetAction targetNextState remaining currentState trace - tilt ^ 2 * mdp.transitionCoordinateVariance targetState targetAction targetNextState * mdp.transitionVisitFrom targetState targetAction remaining currentState trace) 1 0 (policy.trajectoryKernelRemaining remaining hremaining currentState)

Integrating the random initial state keeps the exact coordinate-variance compensator on the generated trajectory measure.

theorem trajectoryMeasure_transitionResidual_variance_compensated_hasMGFUpperBoundAt (mdp : MDP State Action) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (targetState : State) (targetAction : Action) (targetNextState : State) (tilt : Real) (htilt : |tilt| <= 1) : Concentration.HasMGFUpperBoundAt (fun trajectory => tilt * mdp.transitionResidualFrom targetState targetAction targetNextState mdp.horizon trajectory.1 trajectory.2 - tilt ^ 2 * mdp.transitionCoordinateVariance targetState targetAction targetNextState * mdp.transitionVisitFrom targetState targetAction mdp.horizon trajectory.1 trajectory.2) 1 0 (policy.trajectoryMeasure initialState)

The exact one-episode batch image of the generated trace inherits the coordinate-variance MGF.

theorem iidEpisodeBatchMeasure_one_aggregateTransitionResidual_variance_compensated_hasMGFUpperBoundAt {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (state : State) (action : Action) (nextState : State) (tilt : Real) (htilt : |tilt| <= 1) : Concentration.HasMGFUpperBoundAt (fun batch : EpisodeBatch mdp 1 => tilt * batch.aggregateTransitionResidual state action nextState - tilt ^ 2 * mdp.transitionCoordinateVariance state action nextState * batch.aggregateVisitReal state action) 1 0 (policy.iidEpisodeBatchMeasure initialState 1)

Every successor episode in the recurrent generated process inherits the same coordinate-variance compensated conditional MGF.

theorem aggregateTransitionResidual_succ_variance_compensated_hasCondMGFUpperBoundAt {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] [StandardBorelSpace (EpisodeBatch mdp 1)] [StandardBorelSpace (EpisodeBatchTrajectory mdp 1)] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (state : State) (action : Action) (nextState : State) (n : Nat) (tilt : Real) (htilt : |tilt| <= 1) : Concentration.HasCondMGFUpperBoundAt (mΩ

Coordinate zero has the same exact coordinate-variance certificate under the initial marginal of the generated recurrent trajectory.

theorem aggregateTransitionResidual_zero_variance_compensated_hasMGFUpperBoundAt {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (state : State) (action : Action) (nextState : State) (tilt : Real) (htilt : |tilt| <= 1) : Concentration.HasMGFUpperBoundAt (fun trajectory : EpisodeBatchTrajectory mdp 1 => tilt * source.aggregateTransitionResidualIncrement state action nextState 0 trajectory - tilt ^ 2 * mdp.transitionCoordinateVariance state action nextState * source.aggregateVisitIncrement state action 0 trajectory) 1 0 source.trajectoryMeasure

Fixed-tilt actual-count upper tail with the true transition-coordinate variance.

theorem measure_aggregateTransitionResidualSum_ge_inter_visitSum_le_variance {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] [StandardBorelSpace (EpisodeBatch mdp 1)] [StandardBorelSpace (EpisodeBatchTrajectory mdp 1)] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (state : State) (action : Action) (nextState : State) (rounds : Nat) (tilt threshold visitBudget : Real) (htilt : 0 < tilt) (htilt_le : tilt <= 1) : source.trajectoryMeasure {trajectory | threshold <= ∑ i ∈ Finset.range rounds, source.aggregateTransitionResidualIncrement state action nextState i trajectory ∧ (∑ i ∈ Finset.range rounds, source.aggregateVisitIncrement state action i trajectory) <= visitBudget} <= ENNReal.ofReal (Real.exp (-tilt * threshold + tilt ^ 2 * mdp.transitionCoordinateVariance state action nextState * visitBudget))

Two-sided coordinate-variance prefix tail on the same generated law.

theorem measure_abs_aggregateTransitionResidualSum_ge_inter_visitSum_le_variance {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] [StandardBorelSpace (EpisodeBatch mdp 1)] [StandardBorelSpace (EpisodeBatchTrajectory mdp 1)] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (state : State) (action : Action) (nextState : State) (rounds : Nat) (tilt threshold visitBudget : Real) (htilt : 0 < tilt) (htilt_le : tilt <= 1) : source.trajectoryMeasure {trajectory | threshold <= |∑ i ∈ Finset.range rounds, source.aggregateTransitionResidualIncrement state action nextState i trajectory| ∧ (∑ i ∈ Finset.range rounds, source.aggregateVisitIncrement state action i trajectory) <= visitBudget} <= 2 * ENNReal.ofReal (Real.exp (-tilt * threshold + tilt ^ 2 * mdp.transitionCoordinateVariance state action nextState * visitBudget))