BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVILocalBellman

Transport the proof-indexed chronological optimal value across a stage equality.

theorem optimalValueAt_eq_of_eq (mdp : MDP State Action) {left right : Nat} (hleft : left <= mdp.horizon) (hright : right <= mdp.horizon) (h : left = right) : mdp.optimalValueAt left hleft = mdp.optimalValueAt right hright

Nonnegative rewards give a nonnegative optimal finite-horizon value.

theorem optimalValueAt_nonneg_of_reward_nonneg (mdp : MDP State Action) (hreward : forall state action, 0 <= mdp.reward state action) (stage : Nat) (hstage : stage <= mdp.horizon) (state : State) : 0 <= mdp.optimalValueAt stage hstage state

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

theorem decisionStageRemaining_succ_eq (mdp : MDP State Action) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) : (mdp.decisionStageRemaining remaining hremaining : Nat) + 1 = mdp.horizon - remaining

Transport the proof-indexed clipped Q surface across equality of the remaining-horizon coordinate.

theorem clippedQRemaining_eq_of_eq {mdp : MDP State Action} (previousQ : QTable mdp) (summary : TransitionCountSummary mdp) (defaultState : State) (bonusScale : Real) {left right : Nat} (hleft : left + 1 <= mdp.horizon) (hright : right + 1 <= mdp.horizon) (h : left = right) : clippedQRemaining previousQ summary defaultState bonusScale left hleft = clippedQRemaining previousQ summary defaultState bonusScale right hright

The selected value in the backward recursion is the selected entry of the chronological clipped Q table.

theorem clippedValueRemaining_succ_eq_selectedQ {mdp : MDP State Action} (previousQ : QTable mdp) (summary : TransitionCountSummary mdp) (defaultState : State) (bonusScale : Real) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) : clippedValueRemaining previousQ summary defaultState bonusScale (remaining + 1) hremaining state = clippedQRemaining previousQ summary defaultState bonusScale remaining hremaining state (clippedPolicyTable mdp previousQ summary defaultState bonusScale (mdp.decisionStageRemaining remaining hremaining) state)

Every entry of one clipped Q update is at most `H`.

theorem clippedQTable_le_horizon (mdp : MDP State Action) (previousQ : QTable mdp) (summary : TransitionCountSummary mdp) (defaultState : State) (bonusScale : Real) (stage : Fin mdp.horizon) (state : State) (action : Action) : clippedQTable mdp previousQ summary defaultState bonusScale stage state action <= (mdp.horizon : Real)

Clipping makes every selected upper value at most `H`, independently of whether the statistical event holds.

theorem clippedValueRemaining_le_horizon {mdp : MDP State Action} (previousQ : QTable mdp) (summary : TransitionCountSummary mdp) (defaultState : State) (bonusScale : Real) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) : clippedValueRemaining previousQ summary defaultState bonusScale remaining hremaining state <= (mdp.horizon : Real)

Pointwise optimal-Q dominance implies that the selected clipped value dominates the optimal value at the matching chronological stage.

theorem optimalValueAt_le_clippedValueRemaining {mdp : MDP State Action} (previousQ : QTable mdp) (summary : TransitionCountSummary mdp) (defaultState : State) (bonusScale : Real) (hdominates : QDominatesOptimal mdp (clippedQTable mdp previousQ summary defaultState bonusScale)) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) : mdp.optimalValueAt (mdp.horizon - remaining) (Nat.sub_le _ _ ) state <= clippedValueRemaining previousQ summary defaultState bonusScale remaining hremaining state

At a positive actual count, the selected clipped value minus the selected policy value propagates through the true transition kernel, plus exactly the empirical-model error and the configured bonus.

theorem clippedValueRemaining_sub_policyValueRemaining_le_of_pos {mdp : MDP State Action} (previousQ : QTable mdp) (summary : TransitionCountSummary mdp) (defaultState : State) (bonusScale modelError : Real) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) (hpos : 0 < summary.aggregateVisitCount state (clippedPolicyTable mdp previousQ summary defaultState bonusScale (mdp.decisionStageRemaining remaining hremaining) state)) (hmodel : (∫ nextState, clippedValueRemaining previousQ summary defaultState bonusScale remaining (by omega) nextState ∂summary.aggregateEmpiricalTransitionKernel defaultState (state, clippedPolicyTable mdp previousQ summary defaultState bonusScale (mdp.decisionStageRemaining remaining hremaining) state)) - mdp.transitionValue (clippedValueRemaining previousQ summary defaultState bonusScale remaining (by omega)) state (clippedPolicyTable mdp previousQ summary defaultState bonusScale (mdp.decisionStageRemaining remaining hremaining) state) <= modelError) : clippedValueRemaining previousQ summary defaultState bonusScale (remaining + 1) hremaining state - (clippedPolicyTable mdp previousQ summary defaultState bonusScale |>.toMarkovPolicy).valueRemaining (remaining + 1) hremaining state <= mdp.transitionValue (fun nextState => clippedValueRemaining previousQ summary defaultState bonusScale remaining (by omega) nextState - (clippedPolicyTable mdp previousQ summary defaultState bonusScale |>.toMarkovPolicy).valueRemaining remaining (by omega) nextState) state (clippedPolicyTable mdp previousQ summary defaultState bonusScale (mdp.decisionStageRemaining remaining hremaining) state) + modelError + bonusScale / Real.sqrt (summary.aggregateVisitCount state (clippedPolicyTable mdp previousQ summary defaultState bonusScale (mdp.decisionStageRemaining remaining hremaining) state))

Bellman gap between one clipped recurrent value surface and the policy selected by that same surface. Naming this exact difference keeps the generated-source recursion readable without hiding either policy identity.

noncomputable def clippedPolicyGapRemaining {mdp : MDP State Action} (previousQ : QTable mdp) (summary : TransitionCountSummary mdp) (defaultState : State) (bonusScale : Real) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) : Real

The deterministic positive-count recursion, expressed through the named same-policy gap.

theorem clippedPolicyGapRemaining_le_of_pos {mdp : MDP State Action} (previousQ : QTable mdp) (summary : TransitionCountSummary mdp) (defaultState : State) (bonusScale modelError : Real) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) (hpos : 0 < summary.aggregateVisitCount state (clippedPolicyTable mdp previousQ summary defaultState bonusScale (mdp.decisionStageRemaining remaining hremaining) state)) (hmodel : (∫ nextState, clippedValueRemaining previousQ summary defaultState bonusScale remaining (by omega) nextState ∂summary.aggregateEmpiricalTransitionKernel defaultState (state, clippedPolicyTable mdp previousQ summary defaultState bonusScale (mdp.decisionStageRemaining remaining hremaining) state)) - mdp.transitionValue (clippedValueRemaining previousQ summary defaultState bonusScale remaining (by omega)) state (clippedPolicyTable mdp previousQ summary defaultState bonusScale (mdp.decisionStageRemaining remaining hremaining) state) <= modelError) : clippedPolicyGapRemaining previousQ summary defaultState bonusScale (remaining + 1) hremaining state <= mdp.transitionValue (clippedPolicyGapRemaining previousQ summary defaultState bonusScale remaining (by omega)) state (clippedPolicyTable mdp previousQ summary defaultState bonusScale (mdp.decisionStageRemaining remaining hremaining) state) + modelError + bonusScale / Real.sqrt (summary.aggregateVisitCount state (clippedPolicyTable mdp previousQ summary defaultState bonusScale (mdp.decisionStageRemaining remaining hremaining) state))

On the same generated transition event, the model error of the selected clipped continuation is self-bounded by the true propagated policy-value gap. The other two terms are the sharp optimal-tail coordinate and the harmonic Bernstein correction.

theorem selectedUpperTransitionModelError_le {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) (previousQ : QTable mdp) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) (count : Fin (episodes * mdp.horizon)) (hactual : adaptiveCumulativeAggregateVisitCountAt trajectory round state (clippedPolicyTable mdp previousQ (adaptiveCumulativeEmpiricalModelStateAt trajectory round).1 defaultState (scale (State := State) (Action := Action) mdp episodes delta) (mdp.decisionStageRemaining remaining hremaining) state) = count + 1) (hdominates : QDominatesOptimal mdp (clippedQTable mdp previousQ (adaptiveCumulativeEmpiricalModelStateAt trajectory round).1 defaultState (scale (State := State) (Action := Action) mdp episodes delta))) (hhorizon : 0 < mdp.horizon) (hrewardNonneg : forall state action, 0 <= mdp.reward state action) (hlog : 0 <= logBudget) : (∫ nextState, clippedValueRemaining previousQ (adaptiveCumulativeEmpiricalModelStateAt trajectory round).1 defaultState (scale (State := State) (Action := Action) mdp episodes delta) remaining (by omega) nextState ∂TransitionCountSummary.aggregateEmpiricalTransitionKernel (adaptiveCumulativeEmpiricalModelStateAt trajectory round).1 defaultState (state, clippedPolicyTable mdp previousQ (adaptiveCumulativeEmpiricalModelStateAt trajectory round).1 defaultState (scale (State := State) (Action := Action) mdp episodes delta) (mdp.decisionStageRemaining remaining hremaining) state)) - mdp.transitionValue (clippedValueRemaining previousQ (adaptiveCumulativeEmpiricalModelStateAt trajectory round).1 defaultState (scale (State := State) (Action := Action) mdp episodes delta) remaining (by omega)) state (clippedPolicyTable mdp previousQ (adaptiveCumulativeEmpiricalModelStateAt trajectory round).1 defaultState (scale (State := State) (Action := Action) mdp episodes delta) (mdp.decisionStageRemaining remaining hremaining) state) <= mdp.transitionValue (fun nextState => clippedValueRemaining previousQ (adaptiveCumulativeEmpiricalModelStateAt trajectory round).1 defaultState (scale (State := State) (Action := Action) mdp episodes delta) remaining (by omega) nextState - ((clippedPolicyTable mdp previousQ (adaptiveCumulativeEmpiricalModelStateAt trajectory round).1 defaultState (scale (State := State) (Action := Action) mdp episodes delta)).toMarkovPolicy.valueRemaining remaining (by omega) nextState)) state (clippedPolicyTable mdp previousQ (adaptiveCumulativeEmpiricalModelStateAt trajectory round).1 defaultState (scale (State := State) (Action := Action) mdp episodes delta) (mdp.decisionStageRemaining remaining hremaining) state) / (32 * mdp.horizon) + 2 * mdp.horizon * logBudget / Real.sqrt (count + 1 : Nat) + 66 * Fintype.card State * (mdp.horizon : Real) ^ 2 * logBudget / (count + 1 : Nat)

Complete local UCBVI-CH recursion at an actual positive generated count. The `7HL` planner bonus and the `2HL` sharp transition-value deviation combine to `9HL`; the remaining coordinate term is self-bounded by the propagated same-policy gap plus the explicit harmonic correction.

theorem selectedPolicyGap_le_of_actual_count {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) {episodes : Nat} {delta : Real} {trajectory : EpisodeBatchTrajectory mdp 1} (htrajectory : trajectory ∉ simultaneousTransitionFailureEvent source episodes (logFactor (State := State) (Action := Action) mdp episodes delta)) (defaultState : State) (round : Fin episodes) (previousQ : QTable mdp) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) (count : Fin (episodes * mdp.horizon)) (hactual : adaptiveCumulativeAggregateVisitCountAt trajectory round state (clippedPolicyTable mdp previousQ (adaptiveCumulativeEmpiricalModelStateAt trajectory round).1 defaultState (scale (State := State) (Action := Action) mdp episodes delta) (mdp.decisionStageRemaining remaining hremaining) state) = count + 1) (hdominates : QDominatesOptimal mdp (clippedQTable mdp previousQ (adaptiveCumulativeEmpiricalModelStateAt trajectory round).1 defaultState (scale (State := State) (Action := Action) mdp episodes delta))) (hhorizon : 0 < mdp.horizon) (hrewardNonneg : forall state action, 0 <= mdp.reward state action) : clippedPolicyGapRemaining previousQ (adaptiveCumulativeEmpiricalModelStateAt trajectory round).1 defaultState (scale (State := State) (Action := Action) mdp episodes delta) (remaining + 1) hremaining state <= mdp.transitionValue (clippedPolicyGapRemaining previousQ (adaptiveCumulativeEmpiricalModelStateAt trajectory round).1 defaultState (scale (State := State) (Action := Action) mdp episodes delta) remaining (by omega)) state (clippedPolicyTable mdp previousQ (adaptiveCumulativeEmpiricalModelStateAt trajectory round).1 defaultState (scale (State := State) (Action := Action) mdp episodes delta) (mdp.decisionStageRemaining remaining hremaining) state) + mdp.transitionValue (clippedPolicyGapRemaining previousQ (adaptiveCumulativeEmpiricalModelStateAt trajectory round).1 defaultState (scale (State := State) (Action := Action) mdp episodes delta) remaining (by omega)) state (clippedPolicyTable mdp previousQ (adaptiveCumulativeEmpiricalModelStateAt trajectory round).1 defaultState (scale (State := State) (Action := Action) mdp episodes delta) (mdp.decisionStageRemaining remaining hremaining) state) / (32 * mdp.horizon) + 9 * mdp.horizon * logFactor (State := State) (Action := Action) mdp episodes delta / Real.sqrt (count + 1 : Nat) + 66 * Fintype.card State * (mdp.horizon : Real) ^ 2 * logFactor (State := State) (Action := Action) mdp episodes delta / (count + 1 : Nat)