OAI/NumberTheory/TotientAsymptotic/SquarefreeCollisionMass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A finite Euler-product bound for the squarefree interval factors in Ford's sieve.

  1. lemma OAI.TotientAsymptotic.squarefree_primeFactors_card line 11
  2. lemma OAI.TotientAsymptotic.squarefree_reciprocal_moment line 15
  3. lemma OAI.TotientAsymptotic.squarefree_collision_mass line 52

    Source documentation

    The elementary tilt giving Ford's (e*i)^I interval bound.

    lemma squarefree_collision_mass (S Q : Finset ℕ) {c I H : ℝ} (hc : 1 ≤ c)
    (hQ : ∀ n ∈ Q,Squarefree n ∧ n.primeFactors ⊆ S ∧
      (n.primeFactors.card:ℝ) ≤ I)
    (hH : (∑ p ∈ S,(p:ℝ)⁻¹) ≤ H) (hIH : c*H ≤ I) :
    (∑ n ∈ Q,c^(2*n.primeFactors.card)/(n:ℝ)) ≤
      Real.exp (I*(Real.log c+1)) := by
…