PntLongVertical

Abstract

The long vertical contour admits a uniform logarithmic-power estimate.

Theorem 1.1 (I3Bound).

Lean statement: D5/S3/Weil/PrimeNumberTheorem/PntLongVertical.I3Bound

Proof. Machine-checked in Lean as D5/S3/Weil/PrimeNumberTheorem/PntLongVertical.I3Bound (✓ std3). ∎

Citation. PrimeNumberTheoremAnd contributors (2026). PrimeNumberTheoremAnd – Medium prime number theorem. URL: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/tree/6a380f0c4658c04a420a9eb00b1ed62a1e3fde01.

Commentary.

Let the real smoothing kernel be continuously differentiable and supported in [1/2, 2]. Assume LogDerivZetaHasBound A Cζ, with Cζ positive and 0 < A ≤ 1/2. There is a positive constant C such that, for every X > 3, T > 3 and 0 < epsilon < 1, setting sigma₁ = 1 − A/(log T)^9 gives the bound ‖I₃‖ ≤ C times X times X to the power −A/(log T)^9, divided by epsilon.

References

• Truth anchor: D5/S3/Weil/PrimeNumberTheorem/PntLongVertical.I3Bound
• Dependency: D5/S3/Weil/PrimeNumberTheorem/PntTail