OAI/NumberTheory/TotientAsymptotic/OmegaReciprocal.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A concrete Euler-product moment for the remaining-factor exclusion. The exponent three is sufficient for the application.

  1. def OAI.TotientAsymptotic.omegaReciprocal line 13
  2. lemma OAI.TotientAsymptotic.omegaReciprocal_nonneg line 26
  3. lemma OAI.TotientAsymptotic.omegaReciprocal_prime line 30
  4. lemma OAI.TotientAsymptotic.omegaReciprocal_prime_norm line 33
  5. lemma OAI.TotientAsymptotic.omega_euler_factor_le line 38
  6. theorem OAI.TotientAsymptotic.omega_reciprocal_mass line 52

    Source documentation

    A finite moment over all positive integers below the endpoint; no sieve or distribution theorem is added to the published hypotheses.

    theorem omega_reciprocal_mass (N : ℕ) (Q : Finset ℕ)
    (hQ : ∀ n ∈ Q, 0 < n ∧ n ≤ N) :
    (∑ n ∈ Q, omegaReciprocal n) ≤ (primeEulerProduct N)^3 := by
…

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

  7. lemma OAI.TotientAsymptotic.omega_exceptional_mass line 89