OAI/NumberTheory/JointDickman/Amplification/DyadicTailSum.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.geometric_sum_under_cap line 12
2. theorem OAI.JointDickman.dyadic_power_sum_bound line 36
3. def OAI.JointDickman.tailSaving line 54
4. theorem OAI.JointDickman.tailSaving_pos line 56
5. theorem OAI.JointDickman.tail_chernoff_factor_bound line 58
6. theorem OAI.JointDickman.dyadic_tail_chernoff_sum line 79

   Source documentation

   The dyadic union bound is uniform in the number of endpoints and in C.

   theorem dyadic_tail_chernoff_sum (S : Finset ℕ) {B Y K C : ℝ}
       (hB : 0 < B) (hY : 0 < Y) (M : ℕ → ℝ)
       (hM : ∀ i ∈ S, Real.log (B / ((2 : ℝ) ^ i * Y)) - K ≤ M i)
       (hcap : ∀ i ∈ S, (2 : ℝ) ^ i * Y ≤ B) :
       (∑ i ∈ S, Real.exp ((1 / 10 : ℝ) * ((2 / 5 : ℝ) * Real.log (B / ((2 : ℝ) ^ i * Y)) - C) +
         ((Real.exp (-(1 / 10 : ℝ)) - 1) / 2) * M i)) ≤
         (Real.exp (K * ((1 - Real.exp (-(1 / 10 : ℝ))) / 2)) *
           ((2 : ℝ) ^ tailSaving / ((2 : ℝ) ^ tailSaving - 1))) * Real.exp (-(1 / 10 : ℝ) * C) := by
   …

   Mentions: OAI.JointDickman.tailSaving