BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIOptimalTailAlignment

Integrating the normalized optimal-tail probe against two probability measures and subtracting transports exactly back to the `V*` difference.

theorem integral_optimalValue_sub_eq_two_mul_horizon_mul_integral_probe_sub (mdp : MDP State Action) (summary : TransitionCountSummary mdp) (defaultState : State) (stage : Fin mdp.horizon) (state : State) (action : Action) : (∫ nextState, mdp.optimalValueAt (stage + 1) (Nat.succ_le_of_lt stage.isLt) nextState ∂summary.aggregateEmpiricalTransitionKernel defaultState (state, action)) - mdp.transitionValue (mdp.optimalValueAt (stage + 1) (Nat.succ_le_of_lt stage.isLt)) state action = 2 * (mdp.horizon : Real) * ((∫ nextState, mdp.optimalTailProbe stage nextState ∂summary.aggregateEmpiricalTransitionKernel defaultState (state, action)) - mdp.transitionValue (mdp.optimalTailProbe stage) state action)

Outside the proved joint event, the empirical transition kernel consumed by the planner has the sharp `V*` projection error at every peeled positive actual count. No confidence statement is supplied by the caller.

theorem abs_empiricalTransition_optimalValue_sub_lt {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 : OptimalTailIndex mdp episodes) (hactual : adaptiveCumulativeAggregateVisitCountAt trajectory index.round index.state index.action = index.count + 1) : |(∫ nextState, mdp.optimalValueAt (index.stage + 1) (Nat.succ_le_of_lt index.stage.isLt) nextState ∂TransitionCountSummary.aggregateEmpiricalTransitionKernel (adaptiveCumulativeEmpiricalModelStateAt trajectory index.round).1 defaultState (index.state, index.action)) - mdp.transitionValue (mdp.optimalValueAt (index.stage + 1) (Nat.succ_le_of_lt index.stage.isLt)) index.state index.action| < 2 * (mdp.horizon : Real) * logBudget / Real.sqrt (index.count + 1 : Nat)