Strong PNT

TheoremStrong PNT#

The blueprint of Strong PNT (Math Inc) states this theorem at PNT/PNT5_Strong.tex, line 3. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as Strong_PNT.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT5_Strong.tex, line 3

LeanStrong_PNT

Uses 2

Proof usesZero-free region near 1 · Uniform bound on the logarithmic derivative of \(\zeta\)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.