Lower shift to Final expansion

LemmaLower shift#

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

Lean

Formalized as zeta32lower.

Sources

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

Leanzeta32lower

Uses 1 · Used by 1

Proof usesFixed lower

Used byLog lower

LemmaLog lower#

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

Lean

Formalized as zeta32lower_log.

Sources

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

Leanzeta32lower_log

Uses 1 · Used by 1

Proof usesLower shift

Used byExpand bound

LemmaUpper pre#

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

Lean

Formalized as zeta32upper_pre.

Sources

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

Leanzeta32upper_pre

Uses 1 · Used by 1

Proof usesGlobal bound

Used byUpper disk

LemmaUpper disk#

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

Lean

Formalized as zeta32upper.

Sources

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

Leanzeta32upper

Uses 1 · Used by 2

Proof usesUpper pre

Used byExpand bound · Order sum

LemmaExpand bound#

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

Lean

Formalized as Zeta1_Zeta_Expand.

Sources

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

LeanZeta1_Zeta_Expand

Uses 3 · Used by 1

Proof usesLog expansion · Upper disk · Log lower

Used byFinal expansion

LemmaFinal expansion#

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

Lean

Formalized as Zeta1_Zeta_Expansion.

Sources

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

LeanZeta1_Zeta_Expansion

Uses 1 · Used by 2

Proof usesExpand bound

Used bySum bound · Expansion

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.