Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVICounting
# Batched visit-count summation for recurrent UCBVI-CH The policy is frozen within each length-`H` episode, so every visit in that episode uses the same strict-prefix count. These lemmas retain that batching exactly: low-count overshoot costs at most one batch, while positive-count terms telescope through square-root and logarithmic potentials.
Module map
Imports
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIRegretDecomposition
Imported by
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIChargeSummation
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.batchedPrefixCount
Compiled
Strict-prefix cumulative mass of a batched nonnegative increment stream.
def batchedPrefixCount (increment : Nat -> Nat) (round : Nat) : Nat
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.batchedPrefixCount_zero
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
@[simp] theorem batchedPrefixCount_zero (increment : Nat -> Nat) : batchedPrefixCount increment 0 = 0
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.batchedPrefixCount_succ
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem batchedPrefixCount_succ (increment : Nat -> Nat) (round : Nat) : batchedPrefixCount increment (round + 1) = batchedPrefixCount increment round + increment round
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.batchedPrefixCount_mono
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem batchedPrefixCount_mono (increment : Nat -> Nat) : Monotone (batchedPrefixCount increment)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.sum_range_forwardDifference
Compiled Internal helper
No declaration docstring is present; use the chapter context and exact statement below.
private theorem sum_range_forwardDifference (f : Nat -> Real) (rounds : Nat) : (∑ round ∈ Finset.range rounds, (f (round + 1) - f round)) = f rounds - f 0
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.sum_low_batchedIncrement_le
Compiled
All increments whose strict-prefix mass is below a threshold occupy at most the threshold plus one batch.
theorem sum_low_batchedIncrement_le (increment : Nat -> Nat) (batch threshold rounds : Nat) (hincrement : forall round, increment round <= batch) : (∑ round ∈ Finset.range rounds, if batchedPrefixCount increment round < threshold then increment round else 0) <= threshold + batch
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.batched_ratio_le_two_log_increment
Compiled Internal helper
No declaration docstring is present; use the chapter context and exact statement below.
private theorem batched_ratio_le_two_log_increment {mass increment : Nat} (hmass : 0 < mass) (hincrement : increment <= mass) : (increment : Real) / mass <= 2 * (Real.log (mass + increment : Nat) - Real.log mass)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.sum_high_batchedRatio_le_log
Compiled
High-prefix reciprocal masses telescope into one logarithm.
theorem sum_high_batchedRatio_le_log (increment : Nat -> Nat) (batch threshold rounds : Nat) (hbatch : 0 < batch) (hthreshold : batch <= threshold) (hincrement : forall round, increment round <= batch) : (∑ round ∈ Finset.range rounds, if threshold <= batchedPrefixCount increment round then (increment round : Real) / batchedPrefixCount increment round else 0) <= 2 * Real.log (max 1 (batchedPrefixCount increment rounds) : Nat)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.batched_inverseSqrt_step
Compiled Internal helper
No declaration docstring is present; use the chapter context and exact statement below.
private theorem batched_inverseSqrt_step {mass increment batch : Nat} (hmass : 0 < mass) (hincrement : increment <= batch) : (increment : Real) / Real.sqrt mass <= 2 * (Real.sqrt (mass + increment : Nat) - Real.sqrt mass) + (batch : Real) * ((increment : Real) / mass)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.sum_positive_batchedInvSqrt_le
Compiled
Batched inverse-square-root masses retain the leading constant two; all within-episode staleness is isolated in one low-count batch and one logarithm.
theorem sum_positive_batchedInvSqrt_le (increment : Nat -> Nat) (batch rounds : Nat) (hbatch : 0 < batch) (hincrement : forall round, increment round <= batch) : (∑ round ∈ Finset.range rounds, if batchedPrefixCount increment round = 0 then 0 else (increment round : Real) / Real.sqrt (batchedPrefixCount increment round)) <= 2 * Real.sqrt (batchedPrefixCount increment rounds) + 2 * batch + 2 * batch * Real.log ((max 1 (batchedPrefixCount increment rounds) : Nat) : Real)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.sum_positive_batchedMinReciprocal_le
Compiled
A reciprocal correction clipped at one horizon pays the threshold region once (plus one stale batch) and then telescopes logarithmically.
theorem sum_positive_batchedMinReciprocal_le (increment : Nat -> Nat) (batch threshold rounds : Nat) (cap coefficient : Real) (hbatch : 0 < batch) (hthreshold : batch <= threshold) (hincrement : forall round, increment round <= batch) (hcap : 0 <= cap) (hcoefficient : 0 <= coefficient) : (∑ round ∈ Finset.range rounds, if batchedPrefixCount increment round = 0 then 0 else (increment round : Real) * min cap (coefficient / batchedPrefixCount increment round)) <= cap * (threshold + batch) + 2 * coefficient * Real.log ((max 1 (batchedPrefixCount increment rounds) : Nat) : Real)