Order nat to Real diff

LemmaOrder nat#

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

Lean

Formalized as lem_m_rho_zeta_nat.

Sources

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

Leanlem_m_rho_zeta_nat

Uses 4 · Used by 1

Proof usesOrder shift · Order is integer · Disk analytic · Point nonzero

Used byTriangle

LemmaFinite set#

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

Lean

Formalized as lem_finiteKzeta.

Sources

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

Leanlem_finiteKzeta

Uses 4 · Used by 1

Proof usesZero shift · Finite zeros · Disk analytic · Point nonzero

Used byTriangle

LemmaTriangle#

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

Lean

Formalized as lem_triangle_ZFR.

Sources

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

Leanlem_triangle_ZFR

Uses 3 · Used by 1

Proof usesNonzero gap · Order nat · Finite set

Used byTriangle

LemmaTriangle#

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

Lean

Formalized as lem_Zeta_Triangle_ZFR.

Sources

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

Leanlem_Zeta_Triangle_ZFR

Uses 2 · Used by 1

Proof usesExpansion · Triangle

Used byLog bound

LemmaSum bound#

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

Lean

Formalized as lem_sumK1abs.

Sources

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

Leanlem_sumK1abs

Uses 1 · Used by 1

Proof usesInverse gap

Used bySum bound

LemmaOrder bound#

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

Lean

Formalized as lem_sum_m_rho_bound_c.

Sources

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

Leanlem_sum_m_rho_bound_c

Uses 6 · Used by 1

Proof usesZero shift · Order shift · Shift bound · Multiplicity bound · Disk analytic · Point nonzero

Used byOrder sum

LemmaOrder sum#

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

Lean

Formalized as lem_sum_m_rho_zeta.

Sources

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

Leanlem_sum_m_rho_zeta

Uses 3 · Used by 1

Proof usesOrder bound · Upper disk · Three exceeds e

Used bySum bound

LemmaSum bound#

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

Lean

Formalized as lem_sumKdeltatlogt.

Sources

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

Leanlem_sumKdeltatlogt

Uses 2 · Used by 1

Proof usesSum bound · Order sum

Used bySum bound

LemmaSum bound#

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

Lean

Formalized as lem_sumKlogt2.

Sources

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

Leanlem_sumKlogt2

Uses 2 · Used by 1

Proof usesSum bound · Delta def

Used byLog bound

LemmaLog bound#

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

Lean

Formalized as lem_logDerivZetalogt0.

Sources

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

Leanlem_logDerivZetalogt0

Uses 3 · Used by 1

Proof usesTriangle · Sum bound · Three exceeds e

Used byLog bound

LemmaLog bound#

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

Lean

Formalized as lem_logDerivZetalogt2.

Sources

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

Leanlem_logDerivZetalogt2

Uses 2 · Used by 1

Proof usesLog bound · Delta def

Used byBound on \(\zeta'/\zeta\)

LemmaReal bound#

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

Lean

Formalized as lem_rhoDRe4.

Sources

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

Leanlem_rhoDRe4

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 1153. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_DRez6dz.

Sources

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

Leanlem_DRez6dz

Uses 2

Proof usesReal bound · Delta compare

LemmaIn disk#

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

Lean

Formalized as lem_YinD.

Sources

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

Leanlem_YinD

Uses 1

Proof usesDelta zeros

LemmaZero set#

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

Lean

Formalized as lem_rhoYzero.

Sources

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

Leanlem_rhoYzero

Uses 1 · Used by 1

Proof usesDelta zeros

Used byEmpty set

LemmaReal abs#

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

Lean

Formalized as lem_absReabs.

Sources

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

Leanlem_absReabs

Used by 1

Used byReal diff

LemmaReal diff#

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

Lean

Formalized as lem_zRe.

Sources

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

Leanlem_zRe

Uses 1 · Used by 1

Proof usesReal abs

Used byReal diff

LemmaReal diff#

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

Lean

Formalized as lem_zRe2.

Sources

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

Leanlem_zRe2

Uses 1 · Used by 1

Proof usesReal diff

Used byReal diff

LemmaReal diff#

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

Lean

Formalized as lem_Rezit.

Sources

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

Leanlem_Rezit

Used by 1

Used byReal diff

LemmaReal diff#

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

Lean

Formalized as lem_zRe3.

Sources

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

Leanlem_zRe3

Uses 2 · Used by 1

Proof usesReal diff · Real diff

Used byReal bound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.