OAI/NumberTheory/TotientAsymptotic/SmoothCofactorMoment.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A concrete Rankin moment for the smooth cofactor discarded in extraction.

  1. def OAI.TotientAsymptotic.powerReciprocal line 12
  2. lemma OAI.TotientAsymptotic.powerReciprocal_nonneg line 18
  3. lemma OAI.TotientAsymptotic.powerReciprocal_prime_norm line 22
  4. lemma OAI.TotientAsymptotic.powerReciprocal_euler_factor line 30
  5. lemma OAI.TotientAsymptotic.smooth_power_reciprocal_mass line 45
  6. lemma OAI.TotientAsymptotic.totient_ratio_le_eulerProduct_of_smooth line 84
  7. lemma OAI.TotientAsymptotic.quarter_log_power line 101
  8. lemma OAI.TotientAsymptotic.quarter_log_exponent_lt_one line 119
  9. theorem OAI.TotientAsymptotic.smooth_cofactor_power_mass line 127

    Source documentation

    A coarse fourth power of the Mertens product suffices for the tail; no asymptotic estimate for smooth integers is assumed.

    theorem smooth_cofactor_power_mass {N : ℕ} (hN : 2 ≤ N) (Q : Finset ℕ)
    (hQ : ∀ n ∈ Q, 0 < n ∧ largestPrimeFactor n ≤ N) :
    (∑ n ∈ Q, (n : ℝ)^(1/(4*Real.log N))/(n.totient : ℝ)) ≤ (primeEulerProduct N)^4 := by
…

    Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.largestPrimeFactor, OAI.TotientAsymptotic.primeEulerProduct