OAI/NumberTheory/TotientAsymptotic/CofactorEnvelope.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The cofactor envelope from Mertens' published prime-product theorem. We use only its upper bound, stated as Theorem 1.1, equation (1.2), in J. D. Lichtman, Mertens' prime product formula, dissected, arXiv:2002.03361v3 (2021), citing Mertens (1874), J. reine angew. Math. 78, 46–62. This is an explicit conditional input.

  1. def OAI.TotientAsymptotic.primeEulerProduct line 18
  2. def OAI.TotientAsymptotic.MertensProductInput line 21
  3. lemma OAI.TotientAsymptotic.totient_ratio_product line 24
  4. lemma OAI.TotientAsymptotic.totient_ratio_le_eulerProduct line 44
  5. theorem OAI.TotientAsymptotic.sum_reciprocal_totient_le line 68

    Source documentation

    A deliberately coarse logarithmic-square envelope is sufficient for the small discrete cofactor. It avoids imposing any coprimality restrictions.

    theorem sum_reciprocal_totient_le (hmertens : MertensProductInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ N : ℕ, 2 ≤ N →
      (∑ n ∈ Finset.Icc 1 N, (n.totient : ℝ)⁻¹) ≤
        C*Real.log N*(1+Real.log N) := by
…

    Mentions: OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.N