BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIRegretDecomposition

Previous Q table for successor episode `n+1`.

noncomputable def successorPreviousQ (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (n : Nat) : QTable mdp

Exact pooled summary available before successor episode `n+1`.

def successorSummary {mdp : MDP State Action} (trajectory : EpisodeBatchTrajectory mdp 1) (n : Nat) : TransitionCountSummary mdp

Greedy recurrent table actually used by successor episode `n+1`.

noncomputable def successorPolicyTable (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (n : Nat) : DeterministicMarkovPolicyTable mdp

Same-policy continuation gap in the successor episode.

noncomputable def successorPolicyGapRemaining (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (n remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) : Real

Per-stage deterministic charge. A zero previous count is paid by `H`; positive counts pay the `9HL/sqrt N` bonus/projection term plus the explicit `66 S H^2 L/N` Bernstein correction.

noncomputable def successorLocalCharge (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (n remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) : Real

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

theorem successorPolicyGapRemaining_mem_Icc {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) {episodes : Nat} {delta : Real} {trajectory : EpisodeBatchTrajectory mdp 1} (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hrewardNonneg : forall state action, 0 <= mdp.reward state action) (hrewardOne : forall state action, mdp.reward state action <= 1) (htrajectory : trajectory ∉ AdaptiveEpisodeBatchSource.simultaneousTransitionFailureEvent source episodes (logFactor (State := State) (Action := Action) mdp episodes delta)) (defaultState : State) (n : Nat) (hn : n + 1 <= episodes) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) : successorPolicyGapRemaining mdp defaultState episodes delta trajectory n remaining hremaining state ∈ Set.Icc (0 : Real) mdp.horizon

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

theorem successorLocalCharge_nonneg (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (n remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) : 0 <= successorLocalCharge mdp defaultState episodes delta trajectory n remaining hremaining state

Normalized weight at the start of a subproblem with `remaining` decisions.

noncomputable def normalizedBellmanRemainingWeight (mdp : MDP State Action) (remaining : Nat) : Real

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

theorem normalizedBellmanRemainingWeight_zero (mdp : MDP State Action) : normalizedBellmanRemainingWeight mdp mdp.horizon = 31 / 32

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

theorem normalizedBellmanRemainingWeight_succ_eq_chargeWeight (mdp : MDP State Action) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) : normalizedBellmanRemainingWeight mdp (remaining + 1) = normalizedBellmanChargeWeight mdp (mdp.decisionStageRemaining remaining hremaining)

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

theorem normalizedBellmanRemainingWeight_eq_stageWeight (mdp : MDP State Action) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) : normalizedBellmanRemainingWeight mdp remaining = normalizedBellmanWeight mdp (mdp.decisionStageRemaining remaining hremaining)

Weighted local charges along the state sequence reconstructed recursively from one successor batch.

noncomputable def successorWeightedChargeFrom (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (n : Nat) : (remaining : Nat) -> remaining <= mdp.horizon -> State -> StepTrace Action State remaining -> Real | 0, _, _, _ => 0 | remaining + 1, hremaining, state, trace => let stage := mdp.decisionStageRemaining remaining hremaining normalizedBellmanChargeWeight mdp stage * successorLocalCharge mdp defaultState episodes delta trajectory n remaining hremaining state + successorWeightedChargeFrom mdp defaultState episodes delta trajectory n remaining (by omega) (trace 0).2 (Fin.tail trace) /-- Full successor-episode charge on the canonical state reconstruction. -/ noncomputable def successorCanonicalWeightedCharge (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (n : Nat) : Real

Full successor-episode charge on the canonical state reconstruction.

noncomputable def successorCanonicalWeightedCharge (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (n : Nat) : Real

Chronological weighted charge of one successor episode.

noncomputable def successorWeightedChargeSum (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (n : Nat) : Real

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

theorem successorWeightedChargeSum_nonneg (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (n : Nat) : 0 <= successorWeightedChargeSum mdp defaultState episodes delta trajectory n

Weighted state-gap transported along one generated successor batch.

noncomputable def successorWeightedVisitedGap (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (n : Nat) (stage : Fin mdp.horizon) : Real

The good same-source transition event discharges the complete local inflated Bellman recursion at every successor episode and state.

theorem successorPolicyGapRemaining_le_inflation_mul_transition_add_charge {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) {episodes : Nat} {delta : Real} {trajectory : EpisodeBatchTrajectory mdp 1} (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hrewardNonneg : forall state action, 0 <= mdp.reward state action) (hrewardOne : forall state action, mdp.reward state action <= 1) (htrajectory : trajectory ∉ simultaneousTransitionFailureEvent source episodes (logFactor (State := State) (Action := Action) mdp episodes delta)) (defaultState : State) (n : Nat) (hn : n + 1 < episodes) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) : successorPolicyGapRemaining mdp defaultState episodes delta trajectory n (remaining + 1) hremaining state <= bellmanInflation mdp * mdp.transitionValue (successorPolicyGapRemaining mdp defaultState episodes delta trajectory n remaining (by omega)) state (successorPolicyTable mdp defaultState episodes delta trajectory n (mdp.decisionStageRemaining remaining hremaining) state) + successorLocalCharge mdp defaultState episodes delta trajectory n remaining hremaining state

On the joint confidence event, the globally clipped martingale feature is exactly the normalized recurrent policy gap.

theorem clippedSuccessorGapFeatureOfSummaries_eq_weight_mul_gap {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) {episodes : Nat} {delta : Real} {trajectory : EpisodeBatchTrajectory mdp 1} (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hrewardNonneg : forall state action, 0 <= mdp.reward state action) (hrewardOne : forall state action, mdp.reward state action <= 1) (htrajectory : trajectory ∉ simultaneousTransitionFailureEvent source episodes (logFactor (State := State) (Action := Action) mdp episodes delta)) (defaultState : State) (n : Nat) (hn : n + 1 <= episodes) (stage : Fin mdp.horizon) (state : State) : clippedSuccessorGapFeatureOfSummaries mdp defaultState episodes delta n (fun i => (trajectory i).transitionCountSummary) stage state = normalizedBellmanWeight mdp stage * successorPolicyGapRemaining mdp defaultState episodes delta trajectory n (mdp.horizon - (stage.val + 1)) (by omega) state

Exact weighted Bellman telescope for one successor episode. The charge, policy table, recursively reconstructed state path, and martingale innovation are all the same objects used by the recurrent generated source.

theorem normalizedGap_le_weightedChargeFrom_add_deterministicInnovation {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) {episodes : Nat} {delta : Real} {trajectory : EpisodeBatchTrajectory mdp 1} (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hrewardNonneg : forall state action, 0 <= mdp.reward state action) (hrewardOne : forall state action, mdp.reward state action <= 1) (htrajectory : trajectory ∉ simultaneousTransitionFailureEvent source episodes (logFactor (State := State) (Action := Action) mdp episodes delta)) (defaultState : State) (n : Nat) (hn : n + 1 < episodes) : forall (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) (trace : StepTrace Action State remaining), normalizedBellmanRemainingWeight mdp remaining * successorPolicyGapRemaining mdp defaultState episodes delta trajectory n remaining hremaining state <= successorWeightedChargeFrom mdp defaultState episodes delta trajectory n remaining hremaining state trace + mdp.sampledCumulativeDeterministicGapInnovationFrom (successorPolicyTable mdp defaultState episodes delta trajectory n) (clippedSuccessorGapFeatureOfSummaries mdp defaultState episodes delta n (fun i => (trajectory i).transitionCountSummary)) remaining hremaining state trace

The full-horizon successor policy gap is bounded by the globally capped canonical charge plus the exact successor Bellman innovation.

theorem successorPolicyGapRemaining_le_cap_mul_charge_add_innovation {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) {episodes : Nat} {delta : Real} {trajectory : EpisodeBatchTrajectory mdp 1} (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hrewardNonneg : forall state action, 0 <= mdp.reward state action) (hrewardOne : forall state action, mdp.reward state action <= 1) (htrajectory : trajectory ∉ simultaneousTransitionFailureEvent source episodes (logFactor (State := State) (Action := Action) mdp episodes delta)) (defaultState : State) (n : Nat) (hn : n + 1 < episodes) : successorPolicyGapRemaining mdp defaultState episodes delta trajectory n mdp.horizon le_rfl ((trajectory (n + 1)).reconstructedInitialState defaultState) <= bellmanWeightCap * (successorCanonicalWeightedCharge mdp defaultState episodes delta trajectory n + mdp.sampledCumulativeDeterministicGapInnovationFrom (successorPolicyTable mdp defaultState episodes delta trajectory n) (clippedSuccessorGapFeatureOfSummaries mdp defaultState episodes delta n (fun i => (trajectory i).transitionCountSummary)) mdp.horizon le_rfl ((trajectory (n + 1)).reconstructedInitialState defaultState) ((trajectory (n + 1)).reconstructedStepTrace))

Optimism converts the generated successor episode's policy-value pseudo-regret into the same recurrent policy gap used by the telescope.

theorem recurrentSource_generatedEpisodePseudoRegret_le_successorPolicyGapRemaining {mdp : MDP State Action} (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} {delta : Real} {trajectory : EpisodeBatchTrajectory mdp 1} (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hrewardNonneg : forall state action, 0 <= mdp.reward state action) (hrewardOne : forall state action, mdp.reward state action <= 1) (defaultState : State) (htrajectory : trajectory ∉ simultaneousTransitionFailureEvent (recurrentSource mdp initialState defaultState episodes delta) episodes (logFactor (State := State) (Action := Action) mdp episodes delta)) (n : Nat) (hn : n + 1 < episodes) : generatedEpisodePseudoRegret (recurrentSource mdp initialState defaultState episodes delta) defaultState trajectory (n + 1) <= successorPolicyGapRemaining mdp defaultState episodes delta trajectory n mdp.horizon le_rfl ((trajectory (n + 1)).reconstructedInitialState defaultState)

The named adaptive martingale process is definitionally the direct canonical innovation used in the successor telescope.

theorem recurrentBellmanInnovationProcess_succ_eq_canonical (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (n : Nat) : recurrentBellmanInnovationProcess mdp defaultState episodes delta (n + 1) trajectory = mdp.sampledCumulativeDeterministicGapInnovationFrom (successorPolicyTable mdp defaultState episodes delta trajectory n) (clippedSuccessorGapFeatureOfSummaries mdp defaultState episodes delta n (fun i => (trajectory i).transitionCountSummary)) mdp.horizon le_rfl ((trajectory (n + 1)).reconstructedInitialState defaultState) ((trajectory (n + 1)).reconstructedStepTrace)

End-to-end good-event decomposition for one generated successor episode.

theorem recurrentSource_generatedSuccessorPseudoRegret_le_charge_add_innovation {mdp : MDP State Action} (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} {delta : Real} {trajectory : EpisodeBatchTrajectory mdp 1} (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hrewardNonneg : forall state action, 0 <= mdp.reward state action) (hrewardOne : forall state action, mdp.reward state action <= 1) (defaultState : State) (htrajectory : trajectory ∉ simultaneousTransitionFailureEvent (recurrentSource mdp initialState defaultState episodes delta) episodes (logFactor (State := State) (Action := Action) mdp episodes delta)) (n : Nat) (hn : n + 1 < episodes) : generatedEpisodePseudoRegret (recurrentSource mdp initialState defaultState episodes delta) defaultState trajectory (n + 1) <= bellmanWeightCap * (successorCanonicalWeightedCharge mdp defaultState episodes delta trajectory n + recurrentBellmanInnovationProcess mdp defaultState episodes delta (n + 1) trajectory)