MRTRieszPrimeGram.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The exact sparse-prime input follows from the quadratic Riesz-Mangoldt kernel. This finite bridge retains the published error and arbitrary Y.

def OAI.TwoPointCorrelations.mrtRieszPrimeWeight line 14
def OAI.TwoPointCorrelations.mrtRieszPrimeSupport line 17
lemma OAI.TwoPointCorrelations.mrt_riesz_prime_weight_nonneg line 19
lemma OAI.TwoPointCorrelations.mrt_riesz_prime_support line 23
lemma OAI.TwoPointCorrelations.mrt_riesz_prime_weight_ge_one line 29

theorem OAI.TwoPointCorrelations.mrt_sparse_prime_of_riesz_kernel line 42

Source documentation

Only the smoothed arithmetic kernel is left by the finite duality step. The small-logY range has already been proved from Chebyshev.

theorem mrt_sparse_prime_of_riesz_kernel
    (hkernel : ∃ C L₀ : ℝ, 0 < C ∧ ∀ L Y : ℝ, L₀ ≤ L → 1 ≤ L → 2 ≤ Y →
      2 * L ^ (3 / 4 : ℝ) * Real.log L < Real.log Y →
      ∀ u : ℝ, |u| ≤ 2 * Real.exp L →
      ‖mrtExponentialPolynomial (mrtRieszPrimeSupport Y)
        (fun n => (mrtRieszPrimeWeight Y n * ArithmeticFunction.vonMangoldt n : ℝ))
        (fun n => -Real.log (n : ℝ)) u‖ ≤
          C * Y / (1 + u ^ 2) + C * Y * Real.exp (-Real.log Y / L ^ (3 / 4 : ℝ)) * L ^ 2) :
    HalaszPrimeSparseInput := by
…

Mentions: OAI.TwoPointCorrelations.mrtExponentialPolynomial, OAI.TwoPointCorrelations.mrtRieszPrimeSupport, OAI.TwoPointCorrelations.mrtRieszPrimeWeight, OAI.TwoPointCorrelations.HalaszPrimeSparseInput