Lean module · Foundations
BanditRLProof.HeavyTailGapThreshold
An explicit integer sample budget makes twice the chosen radius smaller than the gap.
Module map
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.HeavyTail.gapThreshold
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.HeavyTail.gapThresholdReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def gapThreshold (ε u gap : ℝ) (T : ℕ) : ℕ
theorem
BanditRLProof.HeavyTail.gapThreshold_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.HeavyTail.gapThreshold_posReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem gapThreshold_pos (ε u gap : ℝ) (T : ℕ) : 0 < gapThreshold ε u gap T
theorem
BanditRLProof.HeavyTail.confidenceLog_mono
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.HeavyTail.confidenceLog_monoReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem confidenceLog_mono {t T : ℕ} (ht : t ≤ T) : confidenceLog t ≤ confidenceLog T
theorem
BanditRLProof.HeavyTail.twice_radius_lt_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.HeavyTail.twice_radius_lt_gapReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem twice_radius_lt_gap (ε u gap : ℝ) (hε : 0 < ε) (hu : 0 < u) (hg : 0 < gap) (t T n : ℕ) (ht : t ≤ T) (hn : gapThreshold ε u gap T ≤ n) : 2 * confidenceRadius ε u t n < gap