BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.Lean-verified build · exact declarations linked.

Lean module · UCB

BanditRLProof.Algorithms.UCBArmStreamAsymptotics

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

Declarations
15
Placeholders
0

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`.

Used in these reading views: Bandit Book · Reinforcement Learning Book

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.armStreamPSeriesTerm

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def armStreamPSeriesTerm (t : Nat) : NNReal
Source line 23 Chapter context: UCB
def BanditRLProof.UCB.armStreamPSeriesTailBound Compiled

A fixed finite upper bound for every `constSum 4 n`.

Used in these reading views: Bandit Book · Reinforcement Learning Book

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.armStreamPSeriesTailBound

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def armStreamPSeriesTailBound : NNReal
Source line 27 Chapter context: UCB
theorem BanditRLProof.UCB.armStreamPSeriesTerm_summable Compiled

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

Used in these reading views: Bandit Book · Reinforcement Learning Book

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.armStreamPSeriesTerm_summable

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem armStreamPSeriesTerm_summable : Summable armStreamPSeriesTerm
Source line 30 Chapter context: UCB
theorem BanditRLProof.UCB.indexTail_four_eq_coe_armStreamPSeriesTerm Compiled

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

Used in these reading views: Bandit Book · Reinforcement Learning Book

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.indexTail_four_eq_coe_armStreamPSeriesTerm

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem indexTail_four_eq_coe_armStreamPSeriesTerm (t : Nat) : indexTail 4 t = (armStreamPSeriesTerm t : ENNReal)
Source line 35 Chapter context: UCB
theorem BanditRLProof.UCB.constSum_four_le_armStreamPSeriesTailBound Compiled

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

Used in these reading views: Bandit Book · Reinforcement Learning Book

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.constSum_four_le_armStreamPSeriesTailBound

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem constSum_four_le_armStreamPSeriesTailBound (n : Nat) : constSum 4 n <= (armStreamPSeriesTailBound : ENNReal)
Source line 40 Chapter context: UCB
theorem BanditRLProof.UCB.constSum_four_toReal_le_armStreamPSeriesTailBound Compiled

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

Used in these reading views: Bandit Book · Reinforcement Learning Book

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.constSum_four_toReal_le_armStreamPSeriesTailBound

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem constSum_four_toReal_le_armStreamPSeriesTailBound (n : Nat) : (constSum 4 n).toReal <= (armStreamPSeriesTailBound : Real)
Source line 52 Chapter context: UCB
def BanditRLProof.UCB.armStreamAsymptoticModelCoefficient Compiled

Fixed kernel-dependent coefficient for the one-policy logarithmic envelope.

Used in these reading views: Bandit Book · Reinforcement Learning Book

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.armStreamAsymptoticModelCoefficient

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def armStreamAsymptoticModelCoefficient {K : Nat} (nu : Kernel (Fin K) Real) (sigma2 : NNReal) : Real
Source line 62 Chapter context: UCB
theorem BanditRLProof.UCB.armStreamAsymptoticModelCoefficient_nonneg Compiled

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

Used in these reading views: Bandit Book · Reinforcement Learning Book

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.armStreamAsymptoticModelCoefficient_nonneg

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem armStreamAsymptoticModelCoefficient_nonneg {K : Nat} (hK : 0 < K) (nu : Kernel (Fin K) Real) (sigma2 : NNReal) : 0 <= armStreamAsymptoticModelCoefficient nu sigma2
Source line 69 Chapter context: UCB
theorem BanditRLProof.UCB.lml_sum_four_le_armStreamAsymptoticModelCoefficient Compiled

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

Used in these reading views: Bandit Book · Reinforcement Learning Book

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.lml_sum_four_le_armStreamAsymptoticModelCoefficient

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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))
Source line 86 Chapter context: UCB
def BanditRLProof.UCB.armStreamExpectedRegret Compiled

Expected regret of one fixed recursive arm-stream UCB process.

Used in these reading views: Bandit Book · Reinforcement Learning Book

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.armStreamExpectedRegret

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def armStreamExpectedRegret {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (n : Nat) : Real
Source line 149 Chapter context: UCB
theorem BanditRLProof.UCB.armStreamExpectedRegret_nonneg_and_le Compiled

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

Used in these reading views: Bandit Book · Reinforcement Learning Book

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.armStreamExpectedRegret_nonneg_and_le

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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))
Source line 157 Chapter context: UCB
theorem BanditRLProof.UCB.armStreamExpectedRegret_isBigO_log Compiled

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

Used in these reading views: Bandit Book · Reinforcement Learning Book

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.armStreamExpectedRegret_isBigO_log

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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))
Source line 182 Chapter context: UCB
theorem BanditRLProof.UCB.armStreamExpectedRegret_isLittleO_natCast_succ Compiled

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

Used in these reading views: Bandit Book · Reinforcement Learning Book

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.armStreamExpectedRegret_isLittleO_natCast_succ

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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))
Source line 223 Chapter context: UCB
def BanditRLProof.UCB.armStreamExpectedAverageRegret Compiled

Expected regret of the fixed arm-stream policy normalized by `n + 1`.

Used in these reading views: Bandit Book · Reinforcement Learning Book

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.armStreamExpectedAverageRegret

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def armStreamExpectedAverageRegret {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (n : Nat) : Real
Source line 236 Chapter context: UCB
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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.armStreamExpectedAverageRegret_tendsto_zero

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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)
Source line 245 Chapter context: UCB