BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVISameSourceConfidence

One transition-coordinate residual on a chronological trace head.

def transitionResidualHead (mdp : MDP State Action) (targetState : State) (targetAction : Action) (targetNextState : State) (currentState : State) (head : Action × State) : Real

The realized visit charged by one transition-coordinate residual.

def transitionVisitHead (_mdp : MDP State Action) (targetState : State) (targetAction : Action) (currentState : State) (head : Action × State) : Real

Sum of one fixed transition residual over the remaining generated trace.

def transitionResidualFrom (mdp : MDP State Action) (targetState : State) (targetAction : Action) (targetNextState : State) : (remaining : Nat) -> State -> StepTrace Action State remaining -> Real | 0, _currentState, _trace => 0 | remaining + 1, currentState, trace => mdp.transitionResidualHead targetState targetAction targetNextState currentState (trace 0) + mdp.transitionResidualFrom targetState targetAction targetNextState remaining (trace 0).2 (Fin.tail trace) /-- Sum of actual visits to one state-action coordinate over the remaining trace. -/ def transitionVisitFrom (mdp : MDP State Action) (targetState : State) (targetAction : Action) : (remaining : Nat) -> State -> StepTrace Action State remaining -> Real | 0, _currentState, _trace => 0 | remaining + 1, currentState, trace => mdp.transitionVisitHead targetState targetAction currentState (trace 0) + mdp.transitionVisitFrom targetState targetAction remaining (trace 0).2 (Fin.tail trace) omit [Nonempty State] [Nonempty Action] in theorem measurable_transitionResidualFrom (mdp : MDP State Action) (targetState : State) (targetAction : Action) (targetNextState : State) (remaining : Nat) : Measurable (fun p : State × StepTrace Action State remaining => mdp.transitionResidualFrom targetState targetAction targetNextState remaining p.1 p.2)

Sum of actual visits to one state-action coordinate over the remaining trace.

def transitionVisitFrom (mdp : MDP State Action) (targetState : State) (targetAction : Action) : (remaining : Nat) -> State -> StepTrace Action State remaining -> Real | 0, _currentState, _trace => 0 | remaining + 1, currentState, trace => mdp.transitionVisitHead targetState targetAction currentState (trace 0) + mdp.transitionVisitFrom targetState targetAction remaining (trace 0).2 (Fin.tail trace) omit [Nonempty State] [Nonempty Action] in theorem measurable_transitionResidualFrom (mdp : MDP State Action) (targetState : State) (targetAction : Action) (targetNextState : State) (remaining : Nat) : Measurable (fun p : State × StepTrace Action State remaining => mdp.transitionResidualFrom targetState targetAction targetNextState remaining p.1 p.2)

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

theorem measurable_transitionResidualFrom (mdp : MDP State Action) (targetState : State) (targetAction : Action) (targetNextState : State) (remaining : Nat) : Measurable (fun p : State × StepTrace Action State remaining => mdp.transitionResidualFrom targetState targetAction targetNextState remaining p.1 p.2)

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

theorem measurable_transitionVisitFrom (mdp : MDP State Action) (targetState : State) (targetAction : Action) (remaining : Nat) : Measurable (fun p : State × StepTrace Action State remaining => mdp.transitionVisitFrom targetState targetAction remaining p.1 p.2)

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

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

One generated action/transition head pays only its realized visit budget.

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

The whole generated finite trace satisfies the same fixed-tilt exponential bound, with compensator equal to its literal state-action visit count.

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

Residual recursion is exactly the chronological finite sum.

theorem transitionResidualFrom_eq_sum (mdp : MDP State Action) (targetState : State) (targetAction : Action) (targetNextState : State) (remaining : Nat) (currentState : State) (trace : StepTrace Action State remaining) : mdp.transitionResidualFrom targetState targetAction targetNextState remaining currentState trace = ∑ stage : Fin remaining, mdp.transitionResidualHead targetState targetAction targetNextState (StepTrace.stateAt currentState trace stage) (trace stage)

Visit recursion is exactly the chronological finite sum.

theorem transitionVisitFrom_eq_sum (mdp : MDP State Action) (targetState : State) (targetAction : Action) (remaining : Nat) (currentState : State) (trace : StepTrace Action State remaining) : mdp.transitionVisitFrom targetState targetAction remaining currentState trace = ∑ stage : Fin remaining, mdp.transitionVisitHead targetState targetAction (StepTrace.stateAt currentState trace stage) (trace stage)

The full-trace residual is the aggregate transition count minus the true singleton mass times the aggregate visit count.

theorem transitionResidualFrom_eq_aggregateCounts (mdp : MDP State Action) (targetState : State) (targetAction : Action) (targetNextState : State) (trajectory : State × StepTrace Action State mdp.horizon) : mdp.transitionResidualFrom targetState targetAction targetNextState mdp.horizon trajectory.1 trajectory.2 = ((mdp.episodeBatchOfTrajectories 1 (fun _ => trajectory)) |>.transitionCountSummary.aggregateTransitionCount targetState targetAction targetNextState : Real) - ((mdp.episodeBatchOfTrajectories 1 (fun _ => trajectory)) |>.transitionCountSummary.aggregateVisitCount targetState targetAction : Real) * (mdp.transition (targetState, targetAction)).real {targetNextState}

The full-trace compensator is the aggregate visit count of its one-batch image.

theorem transitionVisitFrom_eq_aggregateVisitCount (mdp : MDP State Action) (targetState : State) (targetAction : Action) (trajectory : State × StepTrace Action State mdp.horizon) : mdp.transitionVisitFrom targetState targetAction mdp.horizon trajectory.1 trajectory.2 = ((mdp.episodeBatchOfTrajectories 1 (fun _ => trajectory)) |>.transitionCountSummary.aggregateVisitCount targetState targetAction : Real)

The compensated fixed-tilt witness after integrating the random initial state.

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

The generated one-batch aggregate transition residual.

noncomputable def aggregateTransitionResidual {mdp : MDP State Action} (batch : EpisodeBatch mdp 1) (state : State) (action : Action) (nextState : State) : Real

The generated one-batch aggregate state-action visit count as a real.

def aggregateVisitReal {mdp : MDP State Action} (batch : EpisodeBatch mdp 1) (state : State) (action : Action) : Real

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

theorem measurable_aggregateTransitionResidual {mdp : MDP State Action} (state : State) (action : Action) (nextState : State) : Measurable (fun batch : EpisodeBatch mdp 1 => batch.aggregateTransitionResidual state action nextState)

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

theorem measurable_aggregateVisitReal {mdp : MDP State Action} (state : State) (action : Action) : Measurable (fun batch : EpisodeBatch mdp 1 => batch.aggregateVisitReal state action)

One generated episode contributes at most one pooled visit per stage.

theorem aggregateVisitCount_le_horizon {mdp : MDP State Action} (batch : EpisodeBatch mdp 1) (state : State) (action : Action) : batch.transitionCountSummary.aggregateVisitCount state action <= mdp.horizon

The one-episode transition residual is bounded by twice the horizon.

theorem abs_aggregateTransitionResidual_le_two_mul_horizon {mdp : MDP State Action} (batch : EpisodeBatch mdp 1) (state : State) (action : Action) (nextState : State) : |batch.aggregateTransitionResidual state action nextState| <= 2 * (mdp.horizon : Real)

The exact one-episode generated batch law inherits the trace-level compensated MGF; no independent empirical batch is introduced.

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

Canonical finite-prefix filtration presented with the actual `frestrictLe` history object consumed by `AdaptiveEpisodeBatchSource`. It is extensionally the usual product filtration, but this presentation keeps conditional kernels definitionally aligned with the generated source.

noncomputable def batchPrefixFiltration {mdp : MDP State Action} (episodes : Nat) : @Filtration (EpisodeBatchTrajectory mdp episodes) Nat _ MeasurableSpace.pi where

Transport pointwise fixed-tilt MGF bounds through an identified conditional kernel map. This is the fixed-MGF analogue of the repository's centered sub-Gaussian condExpKernel bridge.

theorem hasCondMGFUpperBoundAt_of_condExpKernel_map_eq {Omega : Type*} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (mcond : MeasurableSpace Omega) (hmcond : mcond <= mOmega) (X : Omega -> Real) (hX : @Measurable Omega Real mOmega inferInstance X) (tilt budget : Real) (target : Omega -> Measure Real) (hintegrable : ∀ s, Integrable (fun omega => Real.exp (s * X omega)) mu) (hmap : Filter.Eventually (fun omega => @Measure.map Omega Real mOmega inferInstance X ((@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ mcond) omega) = target omega) (ae (@MeasureTheory.Measure.trim Omega mcond mOmega mu hmcond))) (htarget : Filter.Eventually (fun omega => Concentration.HasMGFUpperBoundAt id tilt budget (target omega)) (ae (@MeasureTheory.Measure.trim Omega mcond mOmega mu hmcond))) : Concentration.HasCondMGFUpperBoundAt mcond hmcond X tilt budget mu

Transport a fixed-tilt conditional MGF certificate across propositionally equal conditioning measurable spaces.

theorem hasCondMGFUpperBoundAt_congr_measurableSpace {Omega : Type*} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (mcond mcond' : MeasurableSpace Omega) (hmcond : mcond <= mOmega) (hmcond' : mcond' <= mOmega) (hspaces : mcond = mcond') (X : Omega -> Real) (tilt budget : Real) (h : Concentration.HasCondMGFUpperBoundAt mcond hmcond X tilt budget mu) : Concentration.HasCondMGFUpperBoundAt mcond' hmcond' X tilt budget mu

Residual of the last batch visible in a finite generated prefix.

noncomputable def aggregateTransitionResidualPrefix {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (state : State) (action : Action) (nextState : State) (round : Nat) (history : EpisodeBatchPrefix mdp 1 round) : Real

Visit count of the last batch visible in a finite generated prefix.

def aggregateVisitPrefix {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (state : State) (action : Action) (round : Nat) (history : EpisodeBatchPrefix mdp 1 round) : Real

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

theorem measurable_aggregateTransitionResidualPrefix {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (state : State) (action : Action) (nextState : State) (round : Nat) : Measurable (source.aggregateTransitionResidualPrefix state action nextState round)

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

theorem measurable_aggregateVisitPrefix {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (state : State) (action : Action) (round : Nat) : Measurable (source.aggregateVisitPrefix state action round)

The actual one-episode transition residual at adaptive coordinate `round`.

noncomputable def aggregateTransitionResidualIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (state : State) (action : Action) (nextState : State) (round : Nat) (trajectory : EpisodeBatchTrajectory mdp 1) : Real

The actual pooled visit count at adaptive coordinate `round`.

def aggregateVisitIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (state : State) (action : Action) (round : Nat) (trajectory : EpisodeBatchTrajectory mdp 1) : Real

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

theorem measurable_aggregateTransitionResidualIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (state : State) (action : Action) (nextState : State) (round : Nat) : Measurable (source.aggregateTransitionResidualIncrement state action nextState round)

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

theorem measurable_aggregateVisitIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (state : State) (action : Action) (round : Nat) : Measurable (source.aggregateVisitIncrement state action round)

The compensated residual process is adapted to the canonical prefix filtration.

theorem aggregateTransitionResidual_compensated_stronglyAdapted_piLE {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (state : State) (action : Action) (nextState : State) (tilt varianceCoeff : Real) : StronglyAdapted (batchPrefixFiltration (mdp

Any measurable real statistic of the next generated episode has exactly the mapped history kernel as its regular conditional law. This reusable bridge is stated for the whole generated batch, so downstream confidence proofs do not replace the recurrent process by an offline batch model.

theorem trajectoryMeasure_condDistrib_batchStatistic {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (n : Nat) (statistic : EpisodeBatch mdp episodes -> Real) (hstatistic : Measurable statistic) : ProbabilityTheory.condDistrib (fun trajectory : EpisodeBatchTrajectory mdp episodes => statistic (trajectory (n + 1))) (Preorder.frestrictLe n) source.trajectoryMeasure =ᵐ[ source.trajectoryMeasure.map (Preorder.frestrictLe n)] (source.batchKernel n).map statistic

Trimmed conditional-expectation-kernel law for an arbitrary measurable real statistic of the next generated episode.

theorem condExpKernel_map_batchStatistic_eq_batchKernel {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] [StandardBorelSpace (EpisodeBatchTrajectory mdp episodes)] (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (n : Nat) (statistic : EpisodeBatch mdp episodes -> Real) (hstatistic : Measurable statistic) : Filter.Eventually (fun trajectory : EpisodeBatchTrajectory mdp episodes => Measure.map (fun path : EpisodeBatchTrajectory mdp episodes => statistic (path (n + 1))) (ProbabilityTheory.condExpKernel source.trajectoryMeasure ((inferInstance : MeasurableSpace (EpisodeBatchPrefix mdp episodes n)).comap (Preorder.frestrictLe n)) trajectory) = ((source.batchKernel n).map statistic) (Preorder.frestrictLe n trajectory)) (ae (source.trajectoryMeasure.trim (Preorder.measurable_frestrictLe n).comap_le))

Every compensated adaptive residual increment is globally exponentially integrable.

theorem integrable_exp_mul_aggregateTransitionResidual_compensatedIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (state : State) (action : Action) (nextState : State) (round : Nat) (tilt varianceCoeff s : Real) : Integrable (fun trajectory : EpisodeBatchTrajectory mdp 1 => Real.exp (s * (tilt * source.aggregateTransitionResidualIncrement state action nextState round trajectory - varianceCoeff * source.aggregateVisitIncrement state action round trajectory))) source.trajectoryMeasure

At every successor episode, the actual transition residual has the same visit-charged fixed-tilt conditional MGF under the recurrent source law.

theorem aggregateTransitionResidual_succ_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) : Concentration.HasCondMGFUpperBoundAt (mΩ

Coordinate zero has the same compensated MGF certificate under the exact initial marginal of the generated recurrent trajectory.

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

Summing the adaptive one-batch residuals through coordinate `round` recovers the exact pooled numerator minus its true transition mass.

theorem sum_aggregateTransitionResidualIncrement_eq_prefixAggregateResidual {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (trajectory : EpisodeBatchTrajectory mdp 1) (round : Nat) (state : State) (action : Action) (nextState : State) : (∑ i ∈ Finset.range (round + 1), source.aggregateTransitionResidualIncrement state action nextState i trajectory) = (adaptiveCumulativeAggregateTransitionCountAt trajectory round state action nextState : Real) - (adaptiveCumulativeAggregateVisitCountAt trajectory round state action : Real) * (mdp.transition (state, action)).real {nextState}

The compensator sum is literally the aggregate visit denominator used by the recurrent planner at the same generated prefix.

theorem sum_aggregateVisitIncrement_eq_prefixAggregateVisitCount {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (trajectory : EpisodeBatchTrajectory mdp 1) (round : Nat) (state : State) (action : Action) : (∑ i ∈ Finset.range (round + 1), source.aggregateVisitIncrement state action i trajectory) = (adaptiveCumulativeAggregateVisitCountAt trajectory round state action : Real)

Fixed-tilt, actual-count upper tail for one pooled transition coordinate on a finite prefix of the generated recurrent process. The random count is retained in the event; no expected-occupancy lower bound is substituted.

theorem measure_aggregateTransitionResidualSum_ge_inter_visitSum_le {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) : 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 / 8) * visitBudget))

Two-sided version of the exact-count prefix tail. Both signs are proved from the same generated conditional law; the factor two is only the final finite union.

theorem measure_abs_aggregateTransitionResidualSum_ge_inter_visitSum_le {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) : 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 / 8) * visitBudget))