Neg bound to Uniform bound on the…

LemmaNeg bound#

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

Lean

Formalized as lem_negleabs.

Sources
Leanlem_negleabs
Used by 1
Used byReal bound

LemmaReal bound#

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

Lean

Formalized as lem_absrez1d.

Sources
Leanlem_absrez1d
Uses 1 · Used by 1
Proof usesNeg bound
Used byReal bound

LemmaReal bound#

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

Lean

Formalized as lem_absrez1d2.

Sources
Leanlem_absrez1d2
Uses 1 · Used by 1
Proof usesReal bound
Used byReal bound

LemmaReal bound#

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

Lean

Formalized as lem_absrez1d3.

Sources
Leanlem_absrez1d3
Uses 1 · Used by 1
Proof usesReal bound
Used byReal bound

LemmaReal bound#

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

Lean

Formalized as lem_zRe4.

Sources
Leanlem_zRe4
Uses 2 · Used by 1
Proof usesReal diff · Real bound
Used byReal bound

LemmaEmpty set#

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

Lean

Formalized as lem_Kzetaempty.

Sources
Leanlem_Kzetaempty
Uses 2 · Used by 1
Proof usesZero set · Delta def
Used byZero sum

LemmaEmpty sum#

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

Lean

Formalized as lem_sumempty.

Sources
Leanlem_sumempty
Used by 1
Used byZero sum

LemmaZero sum#

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

Lean

Formalized as lem_Ksumempty.

Sources
Leanlem_Ksumempty
Uses 2
Proof usesEmpty set · Empty sum

LemmaCenter bound#

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

Lean

Formalized as lem_zetacenterbd.

Sources
Leanlem_zetacenterbd
Used by 1
Used byLog bound

LemmaLog bound#

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

Lean

Formalized as lem_logDerivZetalogt32.

Sources
Leanlem_logDerivZetalogt32
Uses 2 · Used by 1
Proof usesCenter bound · One bound
Used byBound on \(\zeta'/\zeta\)

TheoremBound on \(\zeta'/\zeta\)#

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

Lean

Formalized as thm_final_result.

Sources
Leanthm_final_result
Uses 3 · Used by 1
Proof usesLog bound · Log bound · Three exceeds e
Used byUniform bound on the logarithmic derivative of \(\zeta\)

LemmaZero-free region near 1#

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

Lean

Formalized as ZetaZeroFree_p.

Sources
LeanZetaZeroFree_p
Uses 1 · Used by 1
Proof usesZero free
Used byStrong PNT

LemmaUniform bound on the logarithmic derivative of \(\zeta\)#

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

Lean

Formalized as LogDerivZetaBndUnif2.

Sources
LeanLogDerivZetaBndUnif2
Uses 1 · Used by 1
Proof usesBound on \(\zeta'/\zeta\)
Used byStrong PNT

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.