Shift calc to Global bound

LemmaShift calc#

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

Lean

Formalized as lem_zfroms_calc.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 769

Leanlem_zfroms_calc

Used by 1

Used byShift cond

LemmaShift cond#

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

Lean

Formalized as lem_zfroms_conditions.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 778

Leanlem_zfroms_conditions

Uses 1 · Used by 1

Proof usesShift calc

Used byGlobal bound

LemmaGlobal bound#

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

Lean

Formalized as lem_zetaUppBound.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 788

Leanlem_zetaUppBound

Uses 2 · Used by 1

Proof usesUpper bound · Shift cond

Used byUpper pre

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.