OAI/NumberTheory/TotientAsymptotic/TotientRatioLogLog.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A uniform log-log bound for the elementary totient ratio.

  1. lemma OAI.TotientAsymptotic.totient_factor_large_prime line 11
  2. lemma OAI.TotientAsymptotic.totient_large_prime_product line 31
  3. theorem OAI.TotientAsymptotic.totient_ratio_loglog_bound line 66

    Source documentation

    Uniformity in b ≤ x is the form needed when summing shifted prime pairs.

    theorem totient_ratio_loglog_bound : ∃ C : ℝ, 0<C ∧ ∀ x : ℝ, Real.exp 2 ≤ x →
    ∀ b : ℕ, 0<b → (b:ℝ)≤x → (b:ℝ)/b.totient ≤ C*Real.log (Real.log x) := by
…