Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

PntShortContour

Abstract

The short horizontal contour admits a uniform logarithmic-power estimate.

Theorem 1.1 (I4Bound).

Lean statement: D5/S3/Weil/PrimeNumberTheorem/PntShortContour.I4Bound

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

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

Commentary.

For a once continuously differentiable kernel supported in [1/2, 2], a small-strip holomorphic logarithmic derivative, a lower real part strictly between zero and one, and A strictly positive and at most one half, there are a nonnegative bound constant and a T threshold greater than three. Above that threshold the short horizontal piece satisfies the stated logarithmic-power bound for X greater than three and epsilon strictly between zero and one.

References