Rearranged to Bound on \(\zeta'/\zeta\)

LemmaRearranged#

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

Lean

Formalized as lem341tsC2.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT4_ZeroFreeRegion.tex, line 814

Leanlem341tsC2

Uses 1 · Used by 1

Proof usesInequality

Used byFinal bound

LemmaFinal bound#

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

Lean

Formalized as lem341tsC3.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT4_ZeroFreeRegion.tex, line 825

Leanlem341tsC3

Uses 1 · Used by 1

Proof usesRearranged

Used byZero free

LemmaZero free#

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

Lean

Formalized as zerofree.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT4_ZeroFreeRegion.tex, line 837

Leanzerofree

Uses 2 · Used by 2

Proof usesFinal bound · Zero set

Used byZero free · Zero-free region near 1

• Bound on \(\zeta'/\zeta\)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.