Lean module · Foundations
BanditRLProof.Algorithms.CUCBConfidence
Peeling over the actual random number of observed outcomes.
Module map
Imports
BanditRLProof.Algorithms.CUCBConcentration, BanditRLProof.ProbabilityUnionBound
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.CUCB.observationCount_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.observationCount_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem observationCount_le {m : ℕ} (Y : ℕ → Feedback m) (n : ℕ) (i : Fin m) : observationCount Y n i≤n
def
BanditRLProof.CUCB.pathDeviation
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.pathDeviationReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def pathDeviation (D : Measure UnitOutcome) (i : Fin m) (n : ℕ) (lower : Bool) (Y : ℕ → Round A m) : ℝ
theorem
BanditRLProof.CUCB.path_deviation_slice
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.path_deviation_sliceReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem path_deviation_slice (n k : ℕ) (lower : Bool) (L : ℝ) (hL : 0≤L) (hk : 0<k) : (cucbTrajectory oracle environment) {Y | Real.sqrt ((k:ℝ)*L/2)≤pathDeviation D i n lower Y ∧ (observationCount (fun t => (Y t).2) n i : ℝ)≤k} ≤ ENNReal.ofReal (Real.exp (-L))
theorem
BanditRLProof.CUCB.path_deviation_confidence
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.path_deviation_confidenceReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem path_deviation_confidence (n : ℕ) (lower : Bool) (L : ℝ) (hL : 0≤L) : (cucbTrajectory oracle environment) {Y | 0<observationCount (fun t => (Y t).2) n i ∧ Real.sqrt ((observationCount (fun t => (Y t).2) n i : ℝ)*L/2)≤ pathDeviation D i n lower Y} ≤ (n:ENNReal)*ENNReal.ofReal (Real.exp (-L))