Lean module · Foundations
BanditRLProof.HeavyTailTailSum
Finite uniform budget for the actual two-arm, two-sided confidence union.
Module map
Imports
Imported by
BanditRLProof.Algorithms.HeavyTailExpectedCount, BanditRLProof.HOOTailSum
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.HeavyTail.scheduled_exp_eq
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.scheduled_exp_eqReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem scheduled_exp_eq (t : ℕ) : Real.exp (-confidenceLog t) = 1 / (max (t : ℝ) 2)^4
theorem
BanditRLProof.HeavyTail.cubic_tail_le_telescope
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.cubic_tail_le_telescopeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem cubic_tail_le_telescope (t : ℕ) (ht : 2 ≤ t) : 4*t*Real.exp (-confidenceLog t) ≤ 1 / ((t : ℝ)-1) - 1/t
theorem
BanditRLProof.HeavyTail.reciprocal_telescope
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.reciprocal_telescopeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem reciprocal_telescope (n : ℕ) : (∑ s ∈ Finset.range n, (1 / ((s : ℝ)+1) - 1/((s : ℝ)+2))) = 1 - 1/((n : ℝ)+1)
theorem
BanditRLProof.HeavyTail.scheduled_tail_sum_le_two
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.scheduled_tail_sum_le_twoReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem scheduled_tail_sum_le_two (T : ℕ) : (∑ t ∈ Finset.range T, 4*t*Real.exp (-confidenceLog t)) ≤ 2