Term bound to Fixed lower

LemmaTerm bound#

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

Lean

Formalized as abs_term_bound.

Sources
Leanabs_term_bound
Uses 2 · Used by 1
Proof usesTriangle abs · Prime power
Used byInverse bound

LemmaInv order#

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

Lean

Formalized as inv_inequality.

Sources
Leaninv_inequality
Used by 1
Used byInverse bound

LemmaNonzero term#

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

Lean

Formalized as condp32.

Sources
Leancondp32
Uses 1 · Used by 1
Proof usesPrime decay
Used byInverse bound

LemmaInverse bound#

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

Lean

Formalized as abs_term_inv_bound.

Sources
Leanabs_term_inv_bound
Uses 3 · Used by 1
Proof usesTerm bound · Inv order · Nonzero term
Used byZeta compare

LemmaProd order#

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

Lean

Formalized as prod_inequality.

Sources
Leanprod_inequality
Used by 1
Used byZeta compare

LemmaZeta compare#

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

Lean

Formalized as abs_zeta_inequality.

Sources
Leanabs_zeta_inequality
Uses 3 · Used by 1
Proof usesInverse bound · Prod order · Euler product
Used byZeta lower

TheoremZeta lower#

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

Lean

Formalized as zeta_lower_bound.

Sources
Leanzeta_lower_bound
Uses 3 · Used by 1
Proof usesAbs product · Three halves · Zeta compare
Used byFixed lower

LemmaZeta positive#

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

Lean

Formalized as zetapos.

Sources
Leanzetapos
Used by 1
Used byRatio positive

LemmaRatio positive#

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

Lean

Formalized as zeta332pos.

Sources
Leanzeta332pos
Uses 1 · Used by 1
Proof usesZeta positive
Used byFixed lower

LemmaFixed lower#

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

Lean

Formalized as zeta_low_332.

Sources
Leanzeta_low_332
Uses 2 · Used by 1
Proof usesZeta lower · Ratio positive
Used byLower shift

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.