OAI/NumberTheory/TotientAsymptotic/DyadicSuffix.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TotientAsymptotic.suffix_power_sum_le line 13
2. def OAI.TotientAsymptotic.dyadicSuffixWeight line 24
3. lemma OAI.TotientAsymptotic.dyadicSuffixWeight_eq line 27
4. lemma OAI.TotientAsymptotic.dyadic_suffix_summable line 38
5. lemma OAI.TotientAsymptotic.dyadic_suffix_weight_sum line 48
6. theorem OAI.TotientAsymptotic.dyadic_suffix_exponential_bound line 67

   Source documentation

   In logarithmic height the total reciprocal collision mass decays like exp (-σ B)/σ. No factor exp B is lost in the dyadic summation.

   theorem dyadic_suffix_exponential_bound {σ B : ℝ} (hσ : 0 < σ) {N : ℕ} (hN : 1 ≤ N)
       (hNB : Real.exp B ≤ (N : ℝ)*Real.log 2) :
       (∑' n : ℕ, dyadicSuffixWeight σ (n+N+1)) ≤
         Real.exp (-σ*B)/(σ*Real.log 2) := by
   …

   Mentions: OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.dyadicSuffixWeight