Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

MediumPNT

Abstract

The Chebyshev psi error decays by an exponential power of logarithm.

Theorem 1.1 (MediumPNT).

Lean statement: D5/S3/Weil/PrimeNumberTheorem/MediumPNT.MediumPNT

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

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

Commentary.

There exists a positive real c such that the second Chebyshev function minus the identity is bounded asymptotically by a constant times x times exp of minus c times the one-tenth power of log x. Neither c nor the eventual multiplicative bound is asserted to be explicit.

References