Lean module · Foundations
BanditRLProof.Algorithms.CUCBPolynomialRegret
Exact source polynomial-smoothness endpoints, including small horizons.
Module map
Imports
BanditRLProof.Algorithms.CUCBPolynomialIntegral, BanditRLProof.PowerCutoffNormalization
Imported by
BanditRLProof, BanditRLProof.Algorithms.CUCBFiniteSourceExample
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.CUCB.SourceModel.base_arm_count_pos
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.SourceModel.base_arm_count_posReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem base_arm_count_pos : 0<m
theorem
BanditRLProof.CUCB.SourceModel.approximationRegret_le_linear_gap
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.SourceModel.approximationRegret_le_linear_gapReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem approximationRegret_le_linear_gap (H : ℕ) : S.approximationRegret H≤(H:ℝ)*maxPositiveGap S.score M.trueInput S.alpha
theorem
BanditRLProof.CUCB.SourceModel.approximationRegret_one_le
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.SourceModel.approximationRegret_one_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem approximationRegret_one_le (c : ℝ) (hc : 1≤c) : S.approximationRegret 1≤c*(m:ℝ)*maxPositiveGap S.score M.trueInput S.alpha
theorem
BanditRLProof.CUCB.SourceModel.theorem_two_deterministic
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Indexed settings: Combinatorial bandits
Canonical node identity
declaration:BanditRLProof.CUCB.SourceModel.theorem_two_deterministicReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem theorem_two_deterministic (H : ℕ) (hH : 1≤H) (hp : M.globalMinTrigger=1) (γ ω : ℝ) (hγ : 0<γ) (hω : 0<ω) (hω1 : ω≤1) (hf : ∀u, 0≤u → S.modulus u=γ*u^ω) : S.approximationRegret H≤(2*γ/(2-ω))*(6*(m:ℝ)*Real.log (H:ℝ))^(ω/2)*(H:ℝ)^(1-ω/2)+ (1+Real.pi^2/3)*(m:ℝ)*maxPositiveGap S.score M.trueInput S.alpha
theorem
BanditRLProof.CUCB.SourceModel.theorem_two_probabilistic
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Indexed settings: Combinatorial bandits
Canonical node identity
declaration:BanditRLProof.CUCB.SourceModel.theorem_two_probabilisticReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem theorem_two_probabilistic (H : ℕ) (hH : 1≤H) (hp : M.globalMinTrigger<1) (γ ω : ℝ) (hγ : 0<γ) (hω : 0<ω) (hω1 : ω≤1) (hf : ∀u, 0≤u → S.modulus u=γ*u^ω) : S.approximationRegret H≤(2*γ/(2-ω))*(12*(m:ℝ)*Real.log (H:ℝ)/M.globalMinTrigger)^(ω/2)* (H:ℝ)^(1-ω/2)+(1+Real.pi^2/2)*(m:ℝ)*maxPositiveGap S.score M.trueInput S.alpha+ ∑i:Fin m, (24*Real.log (H:ℝ)/M.minTrigger i)*maxPositiveGap S.score M.trueInput S.alpha