RoughPrimeMass.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Sharp reciprocal-prime mass and square-error bounds above a large cutoff.

lemma OAI.TotientAsymptotic.prime_interval_reciprocal_eq line 10
lemma OAI.TotientAsymptotic.prime_interval_reciprocal_sharp line 30
lemma OAI.TotientAsymptotic.prime_interval_square_tail line 54

theorem OAI.TotientAsymptotic.rough_interval_allocation_bound line 70

Source documentation

The full allocation estimate, allowing all multiplicities in the common product.

theorem rough_interval_allocation_bound : ∃ U₀ : ℝ,2 ≤ U₀ ∧ ∀ (c U V I : ℝ),
    1 ≤ c → U₀ ≤ U → 4*c^2 ≤ U → U ≤ V →
    c*(B V-B U+1) ≤ I → ∀ Q : Finset ℕ,
    (∀ n ∈ Q,0 < n ∧ (n.primeFactorsList.length:ℝ) ≤ I ∧
      ∀ p ∈ n.primeFactorsList,U < (p:ℝ) ∧ (p:ℝ) ≤ V) →
    (∑ n ∈ Q,c^(2*n.primeFactorsList.length)/(n:ℝ)) ≤ Real.exp (I*(Real.log c+1)+1) := by
…

Mentions: OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.B