OAI/NumberTheory/TotientAsymptotic/SmoothTotientMass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The finite-set consequence of Ford, The distribution of totients, Lemma 4.3 (2013 revision), proved from the counting bootstrap and Rankin tail.

  1. lemma OAI.TotientAsymptotic.smooth_mass_log_budget line 13
  2. lemma OAI.TotientAsymptotic.smooth_mass_exponential line 28
  3. theorem OAI.TotientAsymptotic.smooth_totient_reciprocal_mass line 40