Lean module · Foundations
BanditRLProof.HOOTailSum
Summable confidence failures after the HOO path/depth union.
Module map
Imports
BanditRLProof.HeavyTailTailSum
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.HOO.selectionFailureBudget
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.HOO.selectionFailureBudgetReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def selectionFailureBudget (n : ℕ) : ℝ
theorem
BanditRLProof.HOO.selection_failure_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.HOO.selection_failure_exp_eqReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem selection_failure_exp_eq (n : ℕ) : Real.exp (-4*Real.log (max (n:ℝ) 2)) = 1/(max (n:ℝ) 2)^4
theorem
BanditRLProof.HOO.selection_failure_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.HOO.selection_failure_le_telescopeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem selection_failure_le_telescope (n : ℕ) (hn : 2 ≤ n) : selectionFailureBudget n ≤ 2 * (1/((n:ℝ)-1) - 1/n)
theorem
BanditRLProof.HOO.selection_failure_sum_le_three
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.HOO.selection_failure_sum_le_threeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem selection_failure_sum_le_three (N : ℕ) : (∑ n ∈ Finset.range N, selectionFailureBudget n) ≤ 3