BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIChargeSummation

Aggregate visits contributed by one actual generated batch.

def generatedBatchAggregateVisitIncrement {mdp : MDP State Action} (trajectory : EpisodeBatchTrajectory mdp 1) (state : State) (action : Action) (episode : Nat) : Nat

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

theorem batchedPrefixCount_generatedBatchAggregateVisitIncrement {mdp : MDP State Action} (trajectory : EpisodeBatchTrajectory mdp 1) (state : State) (action : Action) (round : Nat) : batchedPrefixCount (generatedBatchAggregateVisitIncrement trajectory state action) (round + 1) = adaptiveCumulativeAggregateVisitCountAt trajectory round state action

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

theorem generatedBatchAggregateVisitIncrement_le_horizon {mdp : MDP State Action} (trajectory : EpisodeBatchTrajectory mdp 1) (state : State) (action : Action) (episode : Nat) : generatedBatchAggregateVisitIncrement trajectory state action episode <= mdp.horizon

Every stored state/action record is aligned with its reconstructed full trajectory and with the deterministic recurrent choice. This is the exact portion of mapped-batch identity consumed by the regret ledger.

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

On an aligned successor batch, each canonical recursively selected state/action pair is exactly the corresponding stored empirical record.

theorem successorBatchAligned_step {mdp : MDP State Action} {defaultState : State} {episodes : Nat} {delta : Real} {trajectory : EpisodeBatchTrajectory mdp 1} {n : Nat} (haligned : SuccessorBatchAligned mdp defaultState episodes delta trajectory n) (stage : Fin mdp.horizon) : let batch := trajectory (n + 1) let reconstructed : State × StepTrace Action State mdp.horizon := (batch.reconstructedInitialState defaultState, batch.reconstructedStepTrace) (batch 0 stage).state = mdp.trajectoryStateAt reconstructed stage ∧ (batch 0 stage).action = successorPolicyTable mdp defaultState episodes delta trajectory n stage (mdp.trajectoryStateAt reconstructed stage)

Number of stored visits to one pair is the sum of its stage indicators.

theorem generatedBatchAggregateVisitIncrement_eq_indicatorSum {mdp : MDP State Action} (trajectory : EpisodeBatchTrajectory mdp 1) (state : State) (action : Action) (episode : Nat) : generatedBatchAggregateVisitIncrement trajectory state action episode = ∑ stage : Fin mdp.horizon, if (trajectory episode 0 stage).state = state ∧ (trajectory episode 0 stage).action = action then 1 else 0

The sum of all pair increments in one one-trajectory batch is exactly H.

theorem sum_generatedBatchAggregateVisitIncrement_eq_horizon {mdp : MDP State Action} (trajectory : EpisodeBatchTrajectory mdp 1) (episode : Nat) : ∑ state : State, ∑ action : Action, generatedBatchAggregateVisitIncrement trajectory state action episode = mdp.horizon

The clipped UCBVI-CH charge assigned to one state-action pair in one episode, using the literal strict-prefix count of generated batch records.

noncomputable def generatedPairLocalCharge (mdp : MDP State Action) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (state : State) (action : Action) (episode : Nat) : Real

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

theorem generatedPairLocalCharge_nonneg (mdp : MDP State Action) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (state : State) (action : Action) (episode : Nat) : 0 <= generatedPairLocalCharge mdp episodes delta trajectory state action episode

Alignment converts the policy-selected local charge at a recorded stage to the pair charge indexed by that record's exact state and action.

theorem successorLocalCharge_eq_generatedPairLocalCharge_of_aligned {mdp : MDP State Action} {defaultState : State} {episodes : Nat} {delta : Real} {trajectory : EpisodeBatchTrajectory mdp 1} {n : Nat} (haligned : SuccessorBatchAligned mdp defaultState episodes delta trajectory n) (stage : Fin mdp.horizon) : successorLocalCharge mdp defaultState episodes delta trajectory n (mdp.horizon - (stage.val + 1)) (by omega) (trajectory (n + 1) 0 stage).state = generatedPairLocalCharge mdp episodes delta trajectory (trajectory (n + 1) 0 stage).state (trajectory (n + 1) 0 stage).action (n + 1)

One generated episode's unweighted local charge is exactly the sum of pair charges repeated by the actual state-action visit multiplicities.

theorem sum_successorLocalCharge_eq_sum_pairIncrement_mul_charge_of_aligned {mdp : MDP State Action} {defaultState : State} {episodes : Nat} {delta : Real} {trajectory : EpisodeBatchTrajectory mdp 1} {n : Nat} (haligned : SuccessorBatchAligned mdp defaultState episodes delta trajectory n) : (∑ stage : Fin mdp.horizon, successorLocalCharge mdp defaultState episodes delta trajectory n (mdp.horizon - (stage.val + 1)) (by omega) (trajectory (n + 1) 0 stage).state) = ∑ state : State, ∑ action : Action, (generatedBatchAggregateVisitIncrement trajectory state action (n + 1) : Real) * generatedPairLocalCharge mdp episodes delta trajectory state action (n + 1)

Chronological global stage corresponding to a coordinate of a remaining suffix.

def remainingGlobalStage (mdp : MDP State Action) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (stage : Fin remaining) : Fin mdp.horizon

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

theorem successorLocalCharge_eq_of_remaining_eq (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (n : Nat) {left right : Nat} (hleft : left + 1 <= mdp.horizon) (hright : right + 1 <= mdp.horizon) (h : left = right) (state : State) : successorLocalCharge mdp defaultState episodes delta trajectory n left hleft state = successorLocalCharge mdp defaultState episodes delta trajectory n right hright state

Proof-irrelevant chronological wrapper around the remaining-indexed local charge. Keeping the proof argument out of finite sums avoids dependent rewrites in the charge telescope.

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

The recursive charge is exactly its chronological finite sum.

theorem successorWeightedChargeFrom_eq_sum (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (n : Nat) : forall (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) (trace : StepTrace Action State remaining), successorWeightedChargeFrom mdp defaultState episodes delta trajectory n remaining hremaining state trace = ∑ stage : Fin remaining, normalizedBellmanChargeWeight mdp (remainingGlobalStage mdp remaining hremaining stage) * successorStageLocalCharge mdp defaultState episodes delta trajectory n (remainingGlobalStage mdp remaining hremaining stage) (StepTrace.stateAt state trace stage)

On an aligned generated successor batch, the recursively reconstructed canonical charge is the chronological recorded charge sum.

theorem successorCanonicalWeightedCharge_eq_successorWeightedChargeSum_of_aligned {mdp : MDP State Action} {defaultState : State} {episodes : Nat} {delta : Real} {trajectory : EpisodeBatchTrajectory mdp 1} {n : Nat} (haligned : SuccessorBatchAligned mdp defaultState episodes delta trajectory n) : successorCanonicalWeightedCharge mdp defaultState episodes delta trajectory n = successorWeightedChargeSum mdp defaultState episodes delta trajectory n

One aligned canonical successor charge is dominated by its unweighted state-action multiplicity sum.

theorem successorCanonicalWeightedCharge_le_sum_pairIncrement_mul_charge_of_aligned {mdp : MDP State Action} {defaultState : State} {episodes : Nat} {delta : Real} {trajectory : EpisodeBatchTrajectory mdp 1} {n : Nat} (hhorizon : 0 < mdp.horizon) (haligned : SuccessorBatchAligned mdp defaultState episodes delta trajectory n) : successorCanonicalWeightedCharge mdp defaultState episodes delta trajectory n <= ∑ state : State, ∑ action : Action, (generatedBatchAggregateVisitIncrement trajectory state action (n + 1) : Real) * generatedPairLocalCharge mdp episodes delta trajectory state action (n + 1)

Total pair charge over the first `episodes` generated batches.

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

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

theorem generatedPairChargeTerm_nonneg (mdp : MDP State Action) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (state : State) (action : Action) (episode : Nat) : 0 <= (generatedBatchAggregateVisitIncrement trajectory state action episode : Real) * generatedPairLocalCharge mdp episodes delta trajectory state action episode

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

private theorem sum_range_succ_shift_le_sum_range (f : Nat -> Real) (rounds : Nat) (hf : forall n, 0 <= f n) : (Finset.range (rounds - 1)).sum (fun n => f (n + 1)) <= (Finset.range rounds).sum f

Summing all aligned successor episodes is dominated by the all-batch pair charge ledger; coordinate zero appears only on the right and is nonnegative.

theorem sum_successorCanonicalWeightedCharge_le_totalGeneratedPairCharge {mdp : MDP State Action} {defaultState : State} {episodes : Nat} {delta : Real} {trajectory : EpisodeBatchTrajectory mdp 1} (hhorizon : 0 < mdp.horizon) (haligned : forall n, n + 1 < episodes -> SuccessorBatchAligned mdp defaultState episodes delta trajectory n) : (Finset.range (episodes - 1)).sum (fun n => successorCanonicalWeightedCharge mdp defaultState episodes delta trajectory n) <= totalGeneratedPairCharge mdp episodes delta trajectory

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

private theorem min_add_le_add_min {cap x y : Real} (hx : 0 <= x) : min cap (x + y) <= x + min cap y

Natural threshold at which the clipped reciprocal correction starts its logarithmic telescope.

noncomputable def reciprocalChargeThreshold (mdp : MDP State Action) (episodes : Nat) (delta : Real) : Nat

Exact one-pair accounting before the final paper-constant simplification.

theorem sum_generatedPairCharge_le_accounting (mdp : MDP State Action) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (state : State) (action : Action) (hhorizon : 0 < mdp.horizon) (hlog : 1 <= logFactor (State

The accounting ledger fits the explicit per-pair `18/238` budget.

theorem sum_generatedPairCharge_le_explicit (mdp : MDP State Action) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (state : State) (action : Action) (hhorizon : 0 < mdp.horizon) (hlog : 1 <= logFactor (State

On the positive task domain the paper logarithmic factor is at least one. The factor `5` in the confidence numerator is deliberately retained here: it is what makes the statement true uniformly for every `delta <= 1`.

theorem one_le_logFactor (mdp : MDP State Action) (episodes : Nat) (delta : Real) (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : 1 <= logFactor (State

A single state-action pair is visited at most once per stage, hence at most `episodes * H` times in the complete generated ledger.

theorem batchedPrefixCount_generatedBatchAggregateVisitIncrement_le_totalSteps (mdp : MDP State Action) (episodes : Nat) (trajectory : EpisodeBatchTrajectory mdp 1) (state : State) (action : Action) : batchedPrefixCount (generatedBatchAggregateVisitIncrement trajectory state action) episodes <= totalSteps mdp episodes

The logarithm of every final pair count is controlled by the single paper logarithmic factor used by the generated policy.

theorem log_max_batchedPrefixCount_le_logFactor (mdp : MDP State Action) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (state : State) (action : Action) (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : Real.log ((max 1 (batchedPrefixCount (generatedBatchAggregateVisitIncrement trajectory state action) episodes) : Nat) : Real) <= logFactor (State

The aggregate count ledger is exact: summing final counts over every state-action pair gives the number `episodes * H` of generated transitions.

theorem sum_batchedPrefixCount_generatedBatchAggregateVisitIncrement_eq_totalSteps (mdp : MDP State Action) (episodes : Nat) (trajectory : EpisodeBatchTrajectory mdp 1) : (∑ state : State, ∑ action : Action, batchedPrefixCount (generatedBatchAggregateVisitIncrement trajectory state action) episodes) = totalSteps mdp episodes

Cauchy--Schwarz converts the exact visit ledger into the canonical `sqrt(S A K H)` exploration scale.

theorem sum_sqrt_batchedPrefixCount_le (mdp : MDP State Action) (episodes : Nat) (trajectory : EpisodeBatchTrajectory mdp 1) : (∑ state : State, ∑ action : Action, Real.sqrt (batchedPrefixCount (generatedBatchAggregateVisitIncrement trajectory state action) episodes)) <= Real.sqrt (totalSteps mdp episodes : Nat) * Real.sqrt ((Fintype.card State * Fintype.card Action : Nat) : Real)

Global deterministic charge budget for every generated batch in the canonical recurrent UCBVI-CH ledger. The two square-root factors are kept separate here so the exact total-count identity remains visible.

theorem totalGeneratedPairCharge_le_explicit (mdp : MDP State Action) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : totalGeneratedPairCharge mdp episodes delta trajectory <= 18 * (mdp.horizon : Real) * logFactor (State