PntContourBound
Abstract
Contour deformation controls the smoothed Chebyshev reading.
Theorem 1.1 (SmoothedChebyshevContourBound).
Lean statement: D5/S3/Weil/PrimeNumberTheorem/PntContourBound.SmoothedChebyshevContourBound
Proof. Machine-checked in Lean as D5/S3/Weil/PrimeNumberTheorem/PntContourBound.SmoothedChebyshevContourBound (✓ std3). ∎
Citation. PrimeNumberTheoremAnd contributors (2026). PrimeNumberTheoremAnd – Medium prime number theorem. URL: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/tree/6a380f0c4658c04a420a9eb00b1ed62a1e3fde01.
Commentary.
For a nonnegative once continuously differentiable kernel supported in [1/2, 2] with unit multiplicative Haar mass and a small-strip holomorphic logarithmic derivative, there is a positive constant for the central vertical piece. Under both explicit punctured-rectangle holomorphy assumptions and the stated strict parameter ordering, the error from the Mellin mass term is at most the sum of the eight remaining contour norms and that central bound.