BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVITransitionValueConfidence

The normalized optimal continuation-value probe used by the sharp transition-value confidence coordinate. The symmetric shift avoids requiring nonnegativity merely to apply Hoeffding.

noncomputable def optimalTailProbe (mdp : MDP State Action) (stage : Fin mdp.horizon) (nextState : State) : Real

Under rewards in `[-1,1]`, the normalized optimal tail is in `[0,1]`.

theorem optimalTailProbe_mem_Icc (mdp : MDP State Action) (hreward : ∀ state action, |mdp.reward state action| <= 1) (stage : Fin mdp.horizon) (nextState : State) : mdp.optimalTailProbe stage nextState ∈ Set.Icc (0 : Real) 1

Linear transition residual for a fixed bounded probe. Writing it as the finite linear combination of singleton residuals makes its relation to the coordinate event explicit.

noncomputable def transitionFunctionalResidualHead (mdp : MDP State Action) (feature : State -> Real) (targetState : State) (targetAction : Action) (currentState : State) (head : Action × State) : Real

The same linear probe on a remaining generated trace.

noncomputable def transitionFunctionalResidualFrom (mdp : MDP State Action) (feature : State -> Real) (targetState : State) (targetAction : Action) (remaining : Nat) (currentState : State) (trace : StepTrace Action State remaining) : Real

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

theorem measurable_transitionFunctionalResidualFrom (mdp : MDP State Action) (feature : State -> Real) (targetState : State) (targetAction : Action) (remaining : Nat) : Measurable (fun p : State × StepTrace Action State remaining => mdp.transitionFunctionalResidualFrom feature targetState targetAction remaining p.1 p.2)

A finite-state transition integral is its finite singleton-mass sum.

theorem transitionValue_eq_sum_measureReal (mdp : MDP State Action) (feature : State -> Real) (state : State) (action : Action) : mdp.transitionValue feature state action = ∑ nextState : State, feature nextState * (mdp.transition (state, action)).real {nextState}

On a visited cell, the linear coordinate residual is exactly the centered bounded feature; away from the cell it is zero.

theorem transitionFunctionalResidualHead_eq (mdp : MDP State Action) (feature : State -> Real) (targetState : State) (targetAction : Action) (currentState : State) (head : Action × State) : mdp.transitionFunctionalResidualHead feature targetState targetAction currentState head = if currentState = targetState ∧ head.1 = targetAction then feature head.2 - mdp.transitionValue feature targetState targetAction else 0

The linear probe obeys the same chronological recursion as every singleton coordinate.

theorem transitionFunctionalResidualFrom_succ (mdp : MDP State Action) (feature : State -> Real) (targetState : State) (targetAction : Action) (remaining : Nat) (currentState : State) (trace : StepTrace Action State (remaining + 1)) : mdp.transitionFunctionalResidualFrom feature targetState targetAction (remaining + 1) currentState trace = mdp.transitionFunctionalResidualHead feature targetState targetAction currentState (trace 0) + mdp.transitionFunctionalResidualFrom feature targetState targetAction remaining (trace 0).2 (Fin.tail trace)

A `[0,1]` probe has the standard Hoeffding compensated MGF on one true transition draw.

theorem transitionFunctionalResidualHead_compensated_hasMGFUpperBoundAt (mdp : MDP State Action) (feature : State -> Real) (hfeature : ∀ nextState, feature nextState ∈ Set.Icc (0 : Real) 1) (targetState : State) (targetAction : Action) (currentState : State) (chosenAction : Action) (tilt : Real) : Concentration.HasMGFUpperBoundAt (fun nextState => tilt * mdp.transitionFunctionalResidualHead feature targetState targetAction currentState (chosenAction, nextState) - (tilt ^ 2 / 8) * mdp.transitionVisitHead targetState targetAction currentState (chosenAction, nextState)) 1 0 (mdp.transition (currentState, chosenAction))

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

theorem actionStateKernel_transitionFunctionalResidualHead_compensated_hasMGFUpperBoundAt (mdp : MDP State Action) (policy : MarkovPolicy mdp) (feature : State -> Real) (hfeature : ∀ nextState, feature nextState ∈ Set.Icc (0 : Real) 1) (targetState : State) (targetAction : Action) (currentState : State) (stage : Fin mdp.horizon) (tilt : Real) : Concentration.HasMGFUpperBoundAt (fun head : Action × State => tilt * mdp.transitionFunctionalResidualHead feature targetState targetAction currentState head - (tilt ^ 2 / 8) * mdp.transitionVisitHead targetState targetAction currentState head) 1 0 (policy.actionStateKernel stage currentState)

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

theorem trajectoryKernelRemaining_transitionFunctionalResidual_compensated_hasMGFUpperBoundAt (mdp : MDP State Action) (policy : MarkovPolicy mdp) (feature : State -> Real) (hfeature : ∀ nextState, feature nextState ∈ Set.Icc (0 : Real) 1) (targetState : State) (targetAction : Action) (tilt : Real) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (currentState : State) : Concentration.HasMGFUpperBoundAt (fun trace => tilt * mdp.transitionFunctionalResidualFrom feature targetState targetAction remaining currentState trace - (tilt ^ 2 / 8) * mdp.transitionVisitFrom targetState targetAction remaining currentState trace) 1 0 (policy.trajectoryKernelRemaining remaining hremaining currentState)

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

theorem trajectoryMeasure_transitionFunctionalResidual_compensated_hasMGFUpperBoundAt (mdp : MDP State Action) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (feature : State -> Real) (hfeature : ∀ nextState, feature nextState ∈ Set.Icc (0 : Real) 1) (targetState : State) (targetAction : Action) (tilt : Real) : Concentration.HasMGFUpperBoundAt (fun trajectory => tilt * mdp.transitionFunctionalResidualFrom feature targetState targetAction mdp.horizon trajectory.1 trajectory.2 - (tilt ^ 2 / 8) * mdp.transitionVisitFrom targetState targetAction mdp.horizon trajectory.1 trajectory.2) 1 0 (policy.trajectoryMeasure initialState)

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

theorem transitionFunctionalResidualFrom_eq_aggregateFunctionalResidual (mdp : MDP State Action) (feature : State -> Real) (targetState : State) (targetAction : Action) (trajectory : State × StepTrace Action State mdp.horizon) : mdp.transitionFunctionalResidualFrom feature targetState targetAction mdp.horizon trajectory.1 trajectory.2 = ∑ nextState : State, feature nextState * EpisodeBatch.aggregateTransitionResidual (mdp.episodeBatchOfTrajectories 1 (fun _ => trajectory)) targetState targetAction nextState

A bounded transition functional is another finite coordinate of the same aggregate singleton-residual table.

noncomputable def aggregateTransitionFunctionalResidual {mdp : MDP State Action} (batch : EpisodeBatch mdp 1) (feature : State -> Real) (state : State) (action : Action) : Real

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

theorem measurable_aggregateTransitionFunctionalResidual {mdp : MDP State Action} (feature : State -> Real) (state : State) (action : Action) : Measurable (fun batch : EpisodeBatch mdp 1 => batch.aggregateTransitionFunctionalResidual feature state action)

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

theorem abs_aggregateTransitionFunctionalResidual_le {mdp : MDP State Action} (batch : EpisodeBatch mdp 1) (feature : State -> Real) (hfeature : ∀ nextState, feature nextState ∈ Set.Icc (0 : Real) 1) (state : State) (action : Action) : |batch.aggregateTransitionFunctionalResidual feature state action| <= 2 * Fintype.card State * (mdp.horizon : Real)

At a positive pooled count, empirical transition integration is the exact normalized finite count sum.

theorem integral_aggregateEmpiricalTransitionKernel_eq_sum_div {mdp : MDP State Action} (summary : TransitionCountSummary mdp) (defaultState : State) (feature : State -> Real) (state : State) (action : Action) (hpos : 0 < summary.aggregateVisitCount state action) : (∫ nextState, feature nextState ∂summary.aggregateEmpiricalTransitionKernel defaultState (state, action)) = (∑ nextState : State, feature nextState * (summary.aggregateTransitionCount state action nextState : Real)) / (summary.aggregateVisitCount state action : Real)

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

theorem iidEpisodeBatchMeasure_one_aggregateTransitionFunctionalResidual_compensated_hasMGFUpperBoundAt {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (feature : State -> Real) (hfeature : ∀ nextState, feature nextState ∈ Set.Icc (0 : Real) 1) (state : State) (action : Action) (tilt : Real) : Concentration.HasMGFUpperBoundAt (fun batch : EpisodeBatch mdp 1 => tilt * batch.aggregateTransitionFunctionalResidual feature state action - (tilt ^ 2 / 8) * batch.aggregateVisitReal state action) 1 0 (policy.iidEpisodeBatchMeasure initialState 1)

Fixed-round functional residual read from the actual generated batch.

noncomputable def aggregateTransitionFunctionalResidualPrefix {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (feature : State -> Real) (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.

noncomputable def aggregateTransitionFunctionalResidualIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (feature : State -> Real) (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_aggregateTransitionFunctionalResidualPrefix {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (feature : State -> Real) (state : State) (action : Action) (round : Nat) : Measurable (source.aggregateTransitionFunctionalResidualPrefix feature state action round)

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

theorem measurable_aggregateTransitionFunctionalResidualIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (feature : State -> Real) (state : State) (action : Action) (round : Nat) : Measurable (source.aggregateTransitionFunctionalResidualIncrement feature state action round)

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

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

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

theorem integrable_exp_mul_aggregateTransitionFunctionalResidual_compensatedIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (feature : State -> Real) (hfeature : ∀ nextState, feature nextState ∈ Set.Icc (0 : Real) 1) (state : State) (action : Action) (round : Nat) (tilt varianceCoeff s : Real) : Integrable (fun trajectory : EpisodeBatchTrajectory mdp 1 => Real.exp (s * (tilt * source.aggregateTransitionFunctionalResidualIncrement feature state action round trajectory - varianceCoeff * source.aggregateVisitIncrement state action round trajectory))) source.trajectoryMeasure

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

theorem aggregateTransitionFunctionalResidual_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) (feature : State -> Real) (hfeature : ∀ nextState, feature nextState ∈ Set.Icc (0 : Real) 1) (state : State) (action : Action) (n : Nat) (tilt : Real) : Concentration.HasCondMGFUpperBoundAt (mΩ

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

theorem aggregateTransitionFunctionalResidual_zero_compensated_hasMGFUpperBoundAt {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (feature : State -> Real) (hfeature : ∀ nextState, feature nextState ∈ Set.Icc (0 : Real) 1) (state : State) (action : Action) (tilt : Real) : Concentration.HasMGFUpperBoundAt (fun trajectory : EpisodeBatchTrajectory mdp 1 => tilt * source.aggregateTransitionFunctionalResidualIncrement feature state action 0 trajectory - (tilt ^ 2 / 8) * source.aggregateVisitIncrement state action 0 trajectory) 1 0 source.trajectoryMeasure

Summing the generated functional-probe increments is exactly the finite linear combination of the cumulative singleton residuals.

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

At positive actual count, the functional residual divided by that count is exactly `(P_hat-P) feature` for the empirical kernel consumed by the planner.

theorem aggregateTransitionFunctionalResidual_eq_count_mul_transitionValue_sub {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (trajectory : EpisodeBatchTrajectory mdp 1) (round : Nat) (defaultState : State) (feature : State -> Real) (state : State) (action : Action) (hpos : 0 < adaptiveCumulativeAggregateVisitCountAt trajectory round state action) : (∑ i ∈ Finset.range (round + 1), source.aggregateTransitionFunctionalResidualIncrement feature state action i trajectory) = (adaptiveCumulativeAggregateVisitCountAt trajectory round state action : Real) * ((∫ nextState, feature nextState ∂TransitionCountSummary.aggregateEmpiricalTransitionKernel (adaptiveCumulativeEmpiricalModelStateAt trajectory round).1 defaultState (state, action)) - mdp.transitionValue feature state action)

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

theorem measure_abs_aggregateTransitionFunctionalResidualSum_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) (feature : State -> Real) (hfeature : ∀ nextState, feature nextState ∈ Set.Icc (0 : Real) 1) (state : State) (action : Action) (rounds : Nat) (tilt threshold visitBudget : Real) (htilt : 0 < tilt) : source.trajectoryMeasure {trajectory | threshold <= |∑ i ∈ Finset.range rounds, source.aggregateTransitionFunctionalResidualIncrement feature state action i trajectory| ∧ (∑ i ∈ Finset.range rounds, source.aggregateVisitIncrement state action i trajectory) <= visitBudget} <= 2 * ENNReal.ofReal (Real.exp (-tilt * threshold + (tilt ^ 2 / 8) * visitBudget))