OAI/NumberTheory/JointDickman/Arithmetic/PrimeReciprocalSquareMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Reciprocal-square mass of a dyadic prime interval

  1. theorem OAI.JointDickman.prime_reciprocal_square_mass line 11

    Source documentation

    Chebyshev's proved prime bound supplies the second logarithmic saving when sparse sampling is applied to a reciprocal prime polynomial.

    theorem prime_reciprocal_square_mass : ∃ D : ℝ, 0 < D ∧
    ∀ (N : ℝ), 2 ≤ N → ∀ Q : Finset ℕ,
      (∀ p ∈ Q, p.Prime ∧ N ≤ (p:ℝ) ∧ (p:ℝ) ≤ 2*N) →
      (∑ p ∈ Q, 1/(p:ℝ)^2) ≤ D/(N*Real.log N) := by
…