Lean module · Foundations
BanditRLProof.HeavyTailPowerSum
Finite fractional-power sum needed for the sample-index truncation bias.
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.
theorem
BanditRLProof.HeavyTail.rpow_increment_lower
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.rpow_increment_lowerReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem rpow_increment_lower (x a : ℝ) (hx : 0 ≤ x) (ha : 0 ≤ a) (ha1 : a ≤ 1) : a * (x+1)^(a-1) ≤ (x+1)^a - x^a
theorem
BanditRLProof.HeavyTail.sum_shifted_rpow_le
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.sum_shifted_rpow_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sum_shifted_rpow_le (a : ℝ) (ha : 0 < a) (ha1 : a ≤ 1) (n : ℕ) : (∑ s ∈ Finset.range n, ((s : ℝ)+1)^(a-1)) ≤ (n : ℝ)^a / a