Lean module · Foundations
BanditRLProof.Algorithms.CUCBThreshold
The exact piecewise sampling threshold of Chen et al. (JMLR 2016). Normalized analysis counters repair the mixed triggering-probability step. This file does not assert a CUCB trajectory or regret theorem.
Module map
Imports
No project-local imports.
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.CUCB.thresholdCoefficient
Compiled
`u` is the positive inverse-smoothness value at the current gap.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.thresholdCoefficientReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def thresholdCoefficient (u p : ℝ) : ℝ
def
BanditRLProof.CUCB.samplingThreshold
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.samplingThresholdReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def samplingThreshold (n : ℕ) (u p : ℝ) : ℝ
theorem
BanditRLProof.CUCB.thresholdCoefficient_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.thresholdCoefficient_posReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem thresholdCoefficient_pos {u p : ℝ} (hu : 0<u) (hp : 0<p) : 0<thresholdCoefficient u p
theorem
BanditRLProof.CUCB.samplingThreshold_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
Canonical node identity
declaration:BanditRLProof.CUCB.samplingThreshold_deterministicReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem samplingThreshold_deterministic (n : ℕ) (u : ℝ) : samplingThreshold n u 1 = 6 * Real.log n / u^2
theorem
BanditRLProof.CUCB.samplingThreshold_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
Canonical node identity
declaration:BanditRLProof.CUCB.samplingThreshold_probabilisticReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem samplingThreshold_probabilistic {n : ℕ} {u p : ℝ} (hn : 1≤n) (hp : p≠1) : samplingThreshold n u p = max (12*Real.log n/(u^2*p)) (24*Real.log n/p)
def
BanditRLProof.CUCB.normalizedCharge
Compiled
A definite, tie-fixed analysis choice. Its arguments depend only on the past counters, the current action and fixed instance parameters.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.normalizedChargeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def normalizedCharge {ι : Type*} (s : Finset ι) (hs : s.Nonempty) (N c : ι → ℝ) : ι
theorem
BanditRLProof.CUCB.normalizedCharge_spec
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.normalizedCharge_specReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem normalizedCharge_spec {ι : Type*} (s : Finset ι) (hs : s.Nonempty) (N c : ι → ℝ) : normalizedCharge s hs N c ∈ s ∧ ∀j∈s, N (normalizedCharge s hs N c) / c (normalizedCharge s hs N c) ≤ N j / c j
theorem
BanditRLProof.CUCB.normalizedCharge_sufficient
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.normalizedCharge_sufficientReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem normalizedCharge_sufficient {ι : Type*} (s : Finset ι) (hs : s.Nonempty) (N c : ι → ℝ) (hc : ∀i∈s, 0<c i) (L : ℝ) (hL : L*c (normalizedCharge s hs N c)<N (normalizedCharge s hs N c)) : ∀j∈s, L*c j<N j
theorem
BanditRLProof.CUCB.exists_normalized_charge
Compiled
For any finite nonempty possible-trigger set, an analysis charge exists whose sufficient sampling forces sufficient sampling of every member. The threshold coefficients may differ across arms, including p=1 vs p<1. No claim of predictability is made here; that requires the actual history.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.exists_normalized_chargeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem exists_normalized_charge {ι : Type*} (s : Finset ι) (hs : s.Nonempty) (N c : ι → ℝ) (hc : ∀i∈s, 0<c i) : ∃i∈s, ∀j∈s, ∀L : ℝ, L*c i<N i → L*c j<N j
theorem
BanditRLProof.CUCB.exists_threshold_charge
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.exists_threshold_chargeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem exists_threshold_charge {ι : Type*} (s : Finset ι) (hs : s.Nonempty) (N p : ι → ℝ) (u : ℝ) (hu : 0<u) (hp : ∀i∈s, 0<p i) : ∃i∈s, ∀j∈s, ∀n : ℕ, samplingThreshold n u (p i)<N i → samplingThreshold n u (p j)<N j