Log derivative to Real delta

DefinitionLog derivative#

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

Lean

Formalized as logDerivZeta.

Sources

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

LeanlogDerivZeta

Used by 2

Used byConverges · Series form

DefinitionZero set#

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

Lean

Formalized as zeroZ.

Sources

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

LeanzeroZ

Used by 2

Used byWindow zeros · Zero free

DefinitionWindow zeros#

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

Lean

Formalized as ZetaZerosNearPoint.

Sources

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

LeanZetaZerosNearPoint

Uses 1 · Used by 2

Statement usesZero set

Used byZero bound · Finite set

LemmaFinite set#

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

Lean

Formalized as ZetaZerosNearPoint_finite.

Sources

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

LeanZetaZerosNearPoint_finite

Uses 2 · Used by 1

Statement usesWindow zeros

Proof usesFinite zeros

Used bySum split

LemmaReciprocal real#

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

Lean

Formalized as lem_Re1zge0.

Sources

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

Leanlem_Re1zge0

Used by 1

Used byInverse real

LemmaZero free#

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

Lean

Formalized as lem_sigmage1.

Sources

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

Leanlem_sigmage1

Used by 2

Used byOutside zeros · Zero bound

LemmaZero bound#

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

Lean

Formalized as lem_sigmale1.

Sources

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

Leanlem_sigmale1

Uses 1 · Used by 2

Proof usesZero free

Used byZero bound · Inverse real

LemmaZero bound#

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

Lean

Formalized as lem_sigmale1Zt.

Sources

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

Leanlem_sigmale1Zt

Uses 2 · Used by 1

Proof usesWindow zeros · Zero bound

Used byDelta bound

LemmaOutside zeros#

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

Lean

Formalized as lem_s_notin_Zt.

Sources

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

Leanlem_s_notin_Zt

Uses 1 · Used by 1

Proof usesZero free

Used bySum bound

LemmaHalf disk#

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

Lean

Formalized as s_in_D12.

Sources

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

Leans_in_D12

Used by 1

Used bySum bound

LemmaSum bound#

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

Lean

Formalized as lem_explicit1deltat.

Sources

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

Leanlem_explicit1deltat

Uses 3

Proof usesFinal expansion · Outside zeros · Half disk

LemmaSplit real#

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

Lean

Formalized as lem_explicit1RealReal.

Sources

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

Leanlem_explicit1RealReal

Used by 1

Used byZeta bound

LemmaDouble real#

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

Lean

Formalized as lem_explicit2Real.

Sources

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

Leanlem_explicit2Real

Used by 1

Used byDouble bound

LemmaReal sum#

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

Lean

Formalized as lem_Realsum.

Sources

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

Leanlem_Realsum

Used by 1

Used bySum split

LemmaSum split#

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

Lean

Formalized as lem_sumrho1.

Sources

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

Leanlem_sumrho1

Uses 2 · Used by 2

Proof usesFinite set · Real sum

Used bySum split · Real bound

LemmaSum split#

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

Lean

Formalized as lem_sumrho2.

Sources

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

Leanlem_sumrho2

Uses 1 · Used by 1

Proof usesSum split

Used byReal nonneg

LemmaDifference form#

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

Lean

Formalized as lem_1deltatrho1.

Sources

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

Leanlem_1deltatrho1

Used by 1

Used byReal part

LemmaReal part#

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

Lean

Formalized as lem_Re1deltatrho1.

Sources

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

Leanlem_Re1deltatrho1

Uses 1 · Used by 1

Proof usesDifference form

Used byReal delta

LemmaDelta bound#

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

Lean

Formalized as lem_Re1delta1.

Sources

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

Leanlem_Re1delta1

Uses 1 · Used by 1

Proof usesZero bound

Used byReal delta

LemmaReal delta#

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

Lean

Formalized as lem_Re1deltatge.

Sources

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

Leanlem_Re1deltatge

Uses 2 · Used by 1

Proof usesReal part · Delta bound

Used byPositive real

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.