Delta zeros to Inverse gap

DefinitionDelta zeros#

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

Lean

Formalized as Yt.

Sources

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

LeanYt

Used by 2

Used byZero set · In disk

DefinitionDelta def#

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

Lean

Formalized as deltaz, deltaz_t.

Sources

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

Leandeltaz · deltaz_t

Used by 9

Used byDelta compare · Delta range · Delta bound · Zero free · Disk inclusion · Not zero · Log bound · Sum bound · Empty set

LemmaDelta range#

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

Lean

Formalized as lem_delta19.

Sources

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

Leanlem_delta19

Uses 2 · Used by 3

Proof usesDelta def · Three exceeds e

Used byInverse gap · Nonzero gap · Disk inclusion

LemmaZero free#

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

Lean

Formalized as lem_ZFRdelta.

Sources

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

Leanlem_ZFRdelta

Uses 2 · Used by 2

Proof usesDelta def · Zero free

Used byReal bound · Not zero

LemmaDisk inclusion#

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

Lean

Formalized as lem_ZFRinD.

Sources

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

Leanlem_ZFRinD

Uses 2 · Used by 2

Proof usesDelta def · Delta range

Used byExpansion · Not zero

LemmaNot zero#

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

Lean

Formalized as lem_ZFRnotK.

Sources

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

Leanlem_ZFRnotK

Uses 3 · Used by 1

Proof usesDelta def · Disk inclusion · Zero free

Used byExpansion

LemmaExpansion#

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

Lean

Formalized as lem_Zeta_Expansion_ZFR.

Sources

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

Leanlem_Zeta_Expansion_ZFR

Uses 3 · Used by 1

Proof usesFinal expansion · Disk inclusion · Not zero

Used byTriangle

LemmaDistance real#

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

Lean

Formalized as lem_abszrhoReRe.

Sources

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

Leanlem_abszrhoReRe

Used by 1

Used byGap size

LemmaReal bound#

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

Lean

Formalized as lem_Rerhotodeltarho.

Sources

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

Leanlem_Rerhotodeltarho

Uses 1 · Used by 1

Proof usesZero free

Used byReal bound

LemmaImag bound#

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

Lean

Formalized as lem_DImt2d.

Sources

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

Leanlem_DImt2d

Used by 1

Used byImag growth

LemmaImag growth#

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

Lean

Formalized as lem_DIMt2.

Sources

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

Leanlem_DIMt2

Uses 1 · Used by 1

Proof usesImag bound

Used byLog bound

LemmaLog bound#

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

Lean

Formalized as lem_DlogImlog.

Sources

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

Leanlem_DlogImlog

Uses 1 · Used by 1

Proof usesImag growth

Used byLog compare

LemmaLog compare#

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

Lean

Formalized as lem_D1logtlog.

Sources

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

Leanlem_D1logtlog

Uses 1 · Used by 1

Proof usesLog bound

Used byDelta compare

LemmaDelta compare#

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

Lean

Formalized as lem_Ddt2dz.

Sources

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

Leanlem_Ddt2dz

Uses 2 · Used by 2

Proof usesDelta def · Log compare

Used byDelta bound · Real bound

LemmaDelta bound#

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

Lean

Formalized as lem_deltarhotodeltat.

Sources

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

Leanlem_deltarhotodeltat

Uses 2 · Used by 1

Proof usesDelta def · Delta compare

Used byReal bound

LemmaReal bound#

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

Lean

Formalized as lem_Rerhotodeltat.

Sources

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

Leanlem_Rerhotodeltat

Uses 2 · Used by 1

Proof usesReal bound · Delta bound

Used byGap bound

LemmaGap bound#

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

Lean

Formalized as lem_RezRerho.

Sources

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

Leanlem_RezRerho

Uses 1 · Used by 1

Proof usesReal bound

Used byGap size

LemmaGap size#

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

Lean

Formalized as lem_abszrhodelta.

Sources

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

Leanlem_abszrhodelta

Uses 2 · Used by 2

Proof usesDistance real · Gap bound

Used byInverse gap · Nonzero gap

LemmaNonzero gap#

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

Lean

Formalized as lem_abszrhodeltanot0.

Sources

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

Leanlem_abszrhodeltanot0

Uses 2 · Used by 1

Proof usesGap size · Delta range

Used byTriangle

LemmaInverse gap#

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

Lean

Formalized as lem_1abszrho.

Sources

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

Leanlem_1abszrho

Uses 2 · Used by 1

Proof usesGap size · Delta range

Used bySum bound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.