Lean module · Foundations
BanditRLProof.Algorithms.CUCBImpossibleCase
The source impossible-case argument with actual CUCB indices, true score gaps, finite possible-trigger sets and the source sampling constant six.
Module map
Imports
BanditRLProof.Algorithms.CUCBSourceModel
Imported by
BanditRLProof, BanditRLProof.Algorithms.CUCBSufficientSampling
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.CUCB.confidenceRadius_lt_half
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.confidenceRadius_lt_halfReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem confidenceRadius_lt_half {m : ℕ} (Y : ℕ → Feedback m) (n : ℕ) (i : Fin m) (u : ℝ) (hu : 0<u) (hc : 6*Real.log ((n:ℝ)+1)/u^2 < (observationCount Y n i : ℝ)) : confidenceRadius Y n i (3*Real.log ((n:ℝ)+1)) < u/2
theorem
BanditRLProof.CUCB.SourceModel.not_bad_of_nice_and_sufficient_observations
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.not_bad_of_nice_and_sufficient_observationsReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem not_bad_of_nice_and_sufficient_observations (Y : ℕ → Feedback m) (n : ℕ) (a : A) (hnice : ∀i, |empiricalMean Y n i-(M.trueInput i:ℝ)|≤ confidenceRadius Y n i (3*Real.log ((n:ℝ)+1))) (horacle : S.alpha*scoreOptimum S.score (oracleInput Y n)≤S.score (oracleInput Y n) a) (hcount : ∀i∈M.possible a, 6*Real.log ((n:ℝ)+1)/(S.inverseGap a)^2 < (observationCount Y n i : ℝ)) : ¬0<S.gap a