OAI/NumberTheory/Ostmann/ZeroDensity/SmoothPrincipalPNTBridge.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative PNT for the fixed smooth principal test

Only the classical quantitative Chebyshev estimate is used here. The smoothing bounds are proved for the concrete test retained in the main proof.

  1. theorem OAI.Ostmann.smoothPrincipalError_rough_bound line 16
  2. theorem OAI.Ostmann.smoothPrincipalError_of_psi_bound line 42
  3. theorem OAI.Ostmann.publishedSmoothPrincipalPNT_of_chebyshev line 106

    Source documentation

    The fixed-test PNT follows from the classical quantitative Chebyshev PNT.

    theorem publishedSmoothPrincipalPNT_of_chebyshev
    (hPNT : ∃ c > 0,
      (Chebyshev.psi - id) =O[atTop]
        (fun x : ℝ => x * Real.exp (-c * (Real.log x) ^ ((1 : ℝ) / 2)))) :
    PublishedSmoothPrincipalPNT := by
…

    Mentions: OAI.Ostmann.PublishedSmoothPrincipalPNT