OAI/NumberTheory/TotientAsymptotic/PublishedNormality.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Ford, The distribution of totients, revised arXiv:1104.3264v2 (2013), Lemma 2.6, p. 9. The author-hosted PDF states uniformity for x > 3 and S > 2: https://www.ford126.web.illinois.edu/wwwpapers/totients.pdf . Only this count of exceptional primes is assumed. Reciprocal-weight and actual good-witness discard estimates are derived separately.

  1. def OAI.TotientAsymptotic.nonNormalPrimes line 19
  2. def OAI.TotientAsymptotic.FordLemma26Input line 23

    Source documentation

    The precise published exceptional-prime estimate, at integer endpoints.

    def FordLemma26Input : Prop :=
…
  3. lemma OAI.TotientAsymptotic.normal_two line 28