BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVICoordinateAlignment

At a positive pooled count, the singleton mass of the planner's empirical kernel is exactly the pooled numerator divided by the pooled denominator.

theorem aggregateEmpiricalTransitionKernel_real_singleton_of_pos {mdp : MDP State Action} (summary : TransitionCountSummary mdp) (defaultState : State) (state : State) (action : Action) (nextState : State) (hpos : 0 < summary.aggregateVisitCount state action) : (summary.aggregateEmpiricalTransitionKernel defaultState (state, action)).real {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 bernsteinCoordinateThreshold_mul_probability_div_le {probability logBudget visits : Real} (hprobability : probability ∈ Set.Icc (0 : Real) 1) (hlog : 0 <= logBudget) (hvisits : 0 < visits) : bernsteinCoordinateThreshold logBudget (probability * (1 - probability) * visits) / visits <= 2 * Real.sqrt (2 * logBudget / visits) * Real.sqrt probability + 2 * logBudget / visits

A finite weighted Bernstein coordinate family controls a bounded continuation value. The small `z/(32H)` term is the self-bounding part used by the Bellman recursion; the remaining term is harmonic in the actual count.

theorem abs_sum_weight_mul_massError_le_transitionValue_div_thirtyTwo_add (probability empirical value : State -> Real) (horizon logBudget visits : Real) (hhorizon : 1 <= horizon) (hlog : 0 <= logBudget) (hvisits : 0 < visits) (hprobability : forall state, 0 <= probability state) (hvalue : forall state, value state ∈ Set.Icc (0 : Real) horizon) (hcoordinate : forall state, |empirical state - probability state| <= 2 * Real.sqrt (2 * logBudget / visits) * Real.sqrt (probability state) + 2 * logBudget / visits) : |∑ state : State, value state * (empirical state - probability state)| <= (∑ state : State, value state * probability state) / (32 * horizon) + 66 * Fintype.card State * horizon ^ 2 * logBudget / visits

The simultaneous singleton event controls the exact empirical mass error at the actual positive count. No expected count or auxiliary sample appears.

theorem abs_empiricalTransitionMass_sub_lt_bernstein {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) (defaultState : State) (index : BernsteinCoordinateIndex mdp episodes) (hactual : adaptiveCumulativeAggregateVisitCountAt trajectory index.round index.state index.action = index.count + 1) : |((adaptiveCumulativeEmpiricalModelStateAt trajectory index.round).1 |>.aggregateEmpiricalTransitionKernel defaultState (index.state, index.action)).real {index.nextState} - (mdp.transition (index.state, index.action)).real {index.nextState}| < bernsteinCoordinateThreshold logBudget (mdp.transitionCoordinateVariance index.state index.action index.nextState * (index.count + 1 : Nat)) / (index.count + 1 : Nat)

The exact generated singleton family yields the self-bounding transition value estimate used in the UCBVI recursion.

theorem abs_empiricalTransition_integral_sub_le_transitionValue_div_thirtyTwo_add {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) (defaultState : State) (round : Fin episodes) (state : State) (action : Action) (count : Fin (episodes * mdp.horizon)) (hactual : adaptiveCumulativeAggregateVisitCountAt trajectory round state action = count + 1) (value : State -> Real) (hvalue : forall nextState, value nextState ∈ Set.Icc (0 : Real) mdp.horizon) (hhorizon : 0 < mdp.horizon) (hlog : 0 <= logBudget) : |(∫ nextState, value nextState ∂TransitionCountSummary.aggregateEmpiricalTransitionKernel (adaptiveCumulativeEmpiricalModelStateAt trajectory round).1 defaultState (state, action)) - mdp.transitionValue value state action| <= mdp.transitionValue value state action / (32 * mdp.horizon) + 66 * Fintype.card State * (mdp.horizon : Real) ^ 2 * logBudget / (count + 1 : Nat)