Lean module · Foundations
BanditRLProof.Algorithms.CUCBConcentration
Count-compensated concentration on the actual randomized CUCB path. Both initial and conditional MGF premises are produced from its environment.
Module map
Imports
BanditRLProof.Algorithms.CUCBConditionalMGF
Imported by
BanditRLProof, BanditRLProof.Algorithms.CUCBChargedConcentration, BanditRLProof.Algorithms.CUCBConfidence
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.CUCB.pathNoise
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.pathNoiseReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def pathNoise (D : Measure UnitOutcome) (i : Fin m) (t : ℕ) (Y : ℕ → Round A m) : ℝ
def
BanditRLProof.CUCB.pathCount
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.pathCountReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def pathCount (i : Fin m) (t : ℕ) (Y : ℕ → Round A m) : ℝ
theorem
BanditRLProof.CUCB.measurable_round_piLE
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.measurable_round_piLEReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_round_piLE (n : ℕ) : Measurable[Filtration.piLE n] (fun Y : ℕ → Round A m => Y n)
theorem
BanditRLProof.CUCB.path_compensated_adapted
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_compensated_adaptedReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem path_compensated_adapted (D : Measure UnitOutcome) (i : Fin m) (tilt : ℝ) : StronglyAdapted Filtration.piLE (fun t (Y : ℕ → Round A m) => tilt*pathNoise D i t Y-tilt^2/8*pathCount i t Y)
theorem
BanditRLProof.CUCB.path_noise_count_tail
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_noise_count_tailReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem path_noise_count_tail (n : ℕ) (tilt threshold budget : ℝ) (htilt : 0≤tilt) : (cucbTrajectory oracle environment) {Y | threshold≤∑t∈Finset.range n, pathNoise D i t Y ∧ (∑t∈Finset.range n, pathCount i t Y)≤budget} ≤ ENNReal.ofReal (Real.exp (-tilt*threshold+tilt^2/8*budget))
theorem
BanditRLProof.CUCB.path_noise_count_tail_optimized
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_noise_count_tail_optimizedReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem path_noise_count_tail_optimized (n : ℕ) (threshold budget : ℝ) (hx : 0≤threshold) (hb : 0<budget) : (cucbTrajectory oracle environment) {Y | threshold≤∑t∈Finset.range n, pathNoise D i t Y ∧ (∑t∈Finset.range n, pathCount i t Y)≤budget} ≤ ENNReal.ofReal (Real.exp (-2*threshold^2/budget))
theorem
BanditRLProof.CUCB.path_negative_noise_count_tail
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_negative_noise_count_tailReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem path_negative_noise_count_tail (n : ℕ) (tilt threshold budget : ℝ) (htilt : 0≤tilt) : (cucbTrajectory oracle environment) {Y | threshold≤-(∑t∈Finset.range n, pathNoise D i t Y) ∧ (∑t∈Finset.range n, pathCount i t Y)≤budget} ≤ ENNReal.ofReal (Real.exp (-tilt*threshold+tilt^2/8*budget))
theorem
BanditRLProof.CUCB.path_negative_noise_count_tail_optimized
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_negative_noise_count_tail_optimizedReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem path_negative_noise_count_tail_optimized (n : ℕ) (threshold budget : ℝ) (hx : 0≤threshold) (hb : 0<budget) : (cucbTrajectory oracle environment) {Y | threshold≤-(∑t∈Finset.range n, pathNoise D i t Y) ∧ (∑t∈Finset.range n, pathCount i t Y)≤budget} ≤ ENNReal.ofReal (Real.exp (-2*threshold^2/budget))
theorem
BanditRLProof.CUCB.sum_pathCount
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.sum_pathCountReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sum_pathCount (n : ℕ) (Y : ℕ → Round A m) : (∑t∈Finset.range n, pathCount i t Y) = (observationCount (fun t => (Y t).2) n i : ℝ)
theorem
BanditRLProof.CUCB.sum_pathNoise
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.sum_pathNoiseReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sum_pathNoise (n : ℕ) (Y : ℕ → Round A m) : (∑t∈Finset.range n, pathNoise D i t Y) = observationSum (fun t => (Y t).2) n i - (observationCount (fun t => (Y t).2) n i : ℝ)*marginalMean D
theorem
BanditRLProof.CUCB.observed_sum_upper_tail
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.observed_sum_upper_tailReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem observed_sum_upper_tail (n : ℕ) (threshold budget : ℝ) (hx : 0≤threshold) (hb : 0<budget) : (cucbTrajectory oracle environment) {Y | threshold≤observationSum (fun t => (Y t).2) n i - (observationCount (fun t => (Y t).2) n i : ℝ)*marginalMean D ∧ (observationCount (fun t => (Y t).2) n i : ℝ)≤budget} ≤ ENNReal.ofReal (Real.exp (-2*threshold^2/budget))
theorem
BanditRLProof.CUCB.observed_sum_lower_tail
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.observed_sum_lower_tailReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem observed_sum_lower_tail (n : ℕ) (threshold budget : ℝ) (hx : 0≤threshold) (hb : 0<budget) : (cucbTrajectory oracle environment) {Y | threshold≤(observationCount (fun t => (Y t).2) n i : ℝ)*marginalMean D - observationSum (fun t => (Y t).2) n i ∧ (observationCount (fun t => (Y t).2) n i : ℝ)≤budget} ≤ ENNReal.ofReal (Real.exp (-2*threshold^2/budget))