Lean module · UCB
BanditRLProof.Algorithms.UCBArmStreamAsymptotics
# One-policy asymptotics for the canonical arm-stream UCB process This module keeps one recursive `armStreamAction` and one `armStreamMeasure` fixed across all horizons. At exploration scale `c = 4`, the finite tail term in the exact LML-shaped regret bound is uniformly bounded by a convergent NNReal p-series, yielding logarithmic expected regret and vanishing expected average regret for the same policy and measure.
Module map
Imports
BanditRLProof.Algorithms.UCBArmStreamExpectedPullCount, BanditRLProof.Algorithms.UCBConditionalRewardPairTrajectorySampledAsymptotics
Imported by
BanditRLProof, BanditRLProof.Algorithms.UCBArmStreamFiniteArmRewardLaws
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.UCB.armStreamPSeriesTerm
Compiled
The summable cubic tail that controls `indexTail 4`.
noncomputable def armStreamPSeriesTerm (t : Nat) : NNReal
def
BanditRLProof.UCB.armStreamPSeriesTailBound
Compiled
A fixed finite upper bound for every `constSum 4 n`.
noncomputable def armStreamPSeriesTailBound : NNReal
theorem
BanditRLProof.UCB.armStreamPSeriesTerm_summable
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem armStreamPSeriesTerm_summable : Summable armStreamPSeriesTerm
theorem
BanditRLProof.UCB.indexTail_four_eq_coe_armStreamPSeriesTerm
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem indexTail_four_eq_coe_armStreamPSeriesTerm (t : Nat) : indexTail 4 t = (armStreamPSeriesTerm t : ENNReal)
theorem
BanditRLProof.UCB.constSum_four_le_armStreamPSeriesTailBound
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem constSum_four_le_armStreamPSeriesTailBound (n : Nat) : constSum 4 n <= (armStreamPSeriesTailBound : ENNReal)
theorem
BanditRLProof.UCB.constSum_four_toReal_le_armStreamPSeriesTailBound
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem constSum_four_toReal_le_armStreamPSeriesTailBound (n : Nat) : (constSum 4 n).toReal <= (armStreamPSeriesTailBound : Real)
def
BanditRLProof.UCB.armStreamAsymptoticModelCoefficient
Compiled
Fixed kernel-dependent coefficient for the one-policy logarithmic envelope.
noncomputable def armStreamAsymptoticModelCoefficient {K : Nat} (nu : Kernel (Fin K) Real) (sigma2 : NNReal) : Real
theorem
BanditRLProof.UCB.armStreamAsymptoticModelCoefficient_nonneg
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem armStreamAsymptoticModelCoefficient_nonneg {K : Nat} (hK : 0 < K) (nu : Kernel (Fin K) Real) (sigma2 : NNReal) : 0 <= armStreamAsymptoticModelCoefficient nu sigma2
theorem
BanditRLProof.UCB.lml_sum_four_le_armStreamAsymptoticModelCoefficient
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem lml_sum_four_le_armStreamAsymptoticModelCoefficient {K : Nat} (hK : 0 < K) (nu : Kernel (Fin K) Real) (sigma2 : NNReal) (n : Nat) : (Finset.univ : Finset (Fin K)).sum (fun arm => 8 * 4 * (sigma2 : Real) * Real.log ((n + 1 : Nat) : Real) / realKernelGap nu arm + realKernelGap nu arm * (2 + 2 * (constSum 4 n).toReal)) <= armStreamAsymptoticModelCoefficient nu sigma2 * (1 + Real.log ((n + 1 : Nat) : Real))
def
BanditRLProof.UCB.armStreamExpectedRegret
Compiled
Expected regret of one fixed recursive arm-stream UCB process.
noncomputable def armStreamExpectedRegret {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (n : Nat) : Real
theorem
BanditRLProof.UCB.armStreamExpectedRegret_nonneg_and_le
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem armStreamExpectedRegret_nonneg_and_le {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (hsigma2 : sigma2 ≠ 0) (hsubG : ∀ arm : Fin K, HasSubgaussianMGF (fun reward => reward - realKernelMean nu arm) sigma2 (nu arm)) (n : Nat) : 0 <= armStreamExpectedRegret hK sigma2 nu n ∧ armStreamExpectedRegret hK sigma2 nu n <= armStreamAsymptoticModelCoefficient nu sigma2 * (1 + Real.log ((n + 1 : Nat) : Real))
theorem
BanditRLProof.UCB.armStreamExpectedRegret_isBigO_log
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem armStreamExpectedRegret_isBigO_log {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (hsigma2 : sigma2 ≠ 0) (hsubG : ∀ arm : Fin K, HasSubgaussianMGF (fun reward => reward - realKernelMean nu arm) sigma2 (nu arm)) : (armStreamExpectedRegret hK sigma2 nu) =O[atTop] (fun n : Nat => Real.log ((n + 1 : Nat) : Real))
theorem
BanditRLProof.UCB.armStreamExpectedRegret_isLittleO_natCast_succ
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem armStreamExpectedRegret_isLittleO_natCast_succ {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (hsigma2 : sigma2 ≠ 0) (hsubG : ∀ arm : Fin K, HasSubgaussianMGF (fun reward => reward - realKernelMean nu arm) sigma2 (nu arm)) : (armStreamExpectedRegret hK sigma2 nu) =o[atTop] (fun n : Nat => ((n + 1 : Nat) : Real))
def
BanditRLProof.UCB.armStreamExpectedAverageRegret
Compiled
Expected regret of the fixed arm-stream policy normalized by `n + 1`.
noncomputable def armStreamExpectedAverageRegret {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (n : Nat) : Real
theorem
BanditRLProof.UCB.armStreamExpectedAverageRegret_tendsto_zero
Compiled
One fixed canonical arm-stream UCB policy has vanishing expected average regret under its one fixed product measure.
theorem armStreamExpectedAverageRegret_tendsto_zero {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (hsigma2 : sigma2 ≠ 0) (hsubG : ∀ arm : Fin K, HasSubgaussianMGF (fun reward => reward - realKernelMean nu arm) sigma2 (nu arm)) : Tendsto (armStreamExpectedAverageRegret hK sigma2 nu) atTop (nhds 0)