OAI/NumberTheory/TotientAsymptotic/CofactorMass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Reciprocal totient majorants, including repeated primes in the cofactor.

  1. lemma OAI.TotientAsymptotic.totient_prime_product_lower line 12
  2. theorem OAI.TotientAsymptotic.reciprocal_totient_prime_product line 30

    Source documentation

    No coprimality or distinctness assumption is needed for this majorant.

    theorem reciprocal_totient_prime_product {ι : Type*} (I : Finset ι) (p : ι → ℕ)
    (a : ℕ) (ha : 0 < a) (hp : ∀ i ∈ I, (p i).Prime) :
    ((a*∏ i ∈ I, p i).totient : ℝ)⁻¹ ≤
      (a.totient : ℝ)⁻¹ * ∏ i ∈ I, (p i-1 : ℝ)⁻¹ := by
…

    Mentions: OAI.TotientAsymptotic.a

  3. lemma OAI.TotientAsymptotic.tail_reciprocal_majorant line 56