Weak PNT

TheoremWeakPNT#

We have

\[ \sum_{n \leq x} \Lambda(n) = x + o(x). \]

Proof

Already done by Stoll, assuming Wiener-Ikehara.

Lean

Formalized as WeakPNT.

Sources

• PNT+ blueprint: PrimeNumberTheoremAnd/Wiener.lean

LeanWeakPNT

Uses 1 · Used by 3

Proof usesWiener-Ikehara Theorem (1)

Used bychebyshev-asymptotic · lambda-pnt · Möbius form of prime number theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.