Zeta formula to Upper bound

LemmaZeta formula#

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

Lean

Formalized as lem_zetaFormula.

Sources

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

Leanlem_zetaFormula

Uses 4 · Used by 1

Proof usesFinal form · Series form · Limit term · Integral conv

Used byZeta extend

LemmaAnalytic off#

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

Lean

Formalized as lem_zetaanalS.

Sources

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

Leanlem_zetaanalS

Uses 1 · Used by 1

Proof usesAnalytic off

Used byZeta extend

LemmaS open#

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

Lean

Formalized as lem_S_isOpen.

Sources

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

Leanlem_S_isOpen

Used by 1

Used byT open

LemmaT open#

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

Lean

Formalized as lem_T_isOpen.

Sources

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

Leanlem_T_isOpen

Uses 1 · Used by 1

Proof usesS open

Used byZeta extend

LemmaT connected#

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

Lean

Formalized as lem_T_isPreconnected.

Sources

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

Leanlem_T_isPreconnected

Used by 1

Used byZeta extend

LemmaIntegral analytic#

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

Lean

Formalized as lem_integralAnalytic.

Sources

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

Leanlem_integralAnalytic

Used by 2

Used byZeta extend · Analytic ext

LemmaAnalytic ext#

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

Lean

Formalized as lem_zetaFormulaAC.

Sources

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

Leanlem_zetaFormulaAC

Uses 2 · Used by 1

Proof usesIntegral conv · Integral analytic

Used byZeta extend

LemmaDivide split#

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

Lean

Formalized as lem_div_eq_one_plus_one_div.

Sources

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

Leanlem_div_eq_one_plus_one_div

Used by 1

Used byZeta extend

LemmaZeta extend#

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

Lean

Formalized as lem_zetaAnalyticContinuation.

Sources

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

Leanlem_zetaAnalyticContinuation

Uses 7 · Used by 1

Proof usesZeta formula · Analytic ext · Analytic off · Integral analytic · Divide split · T open · T connected

Used byFirst bound

LemmaFirst bound#

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

Lean

Formalized as lem_zetaBound1.

Sources

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

Leanlem_zetaBound1

Uses 2 · Used by 1

Proof usesTriangle int · Zeta extend

Used bySecond bound

LemmaIntegral value#

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

Lean

Formalized as lem_integralBoundValue.

Sources

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

Leanlem_integralBoundValue

Used by 1

Used bySecond bound

LemmaSecond bound#

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

Lean

Formalized as lem_zetaBound2.

Sources

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

Leanlem_zetaBound2

Uses 3 · Used by 1

Proof usesFirst bound · Term bound · Integral value

Used byThird bound

LemmaInverse mod#

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

Lean

Formalized as lem_sOverSminus1Bound.

Sources

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

Leanlem_sOverSminus1Bound

Uses 1 · Used by 1

Proof usesTriangle int

Used byThird bound

LemmaThird bound#

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

Lean

Formalized as lem_zetaBound3.

Sources

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

Leanlem_zetaBound3

Uses 2 · Used by 1

Proof usesSecond bound · Inverse mod

Used byCombine bounds

Lemmas bound#

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

Lean

Formalized as lem_sBound.

Sources

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

Leanlem_sBound

Used by 1

Used byCombine bounds

LemmaReal inv#

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

Lean

Formalized as lem_invReSbound.

Sources

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

Leanlem_invReSbound

Used by 1

Used byCombine bounds

LemmaShift bound#

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

Lean

Formalized as lem_invSminus1bound.

Sources

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

Leanlem_invSminus1bound

Used by 1

Used byCombine bounds

LemmaCombine bounds#

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

Lean

Formalized as lem_finalBoundCombination.

Sources

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

Leanlem_finalBoundCombination

Uses 4 · Used by 1

Proof usesThird bound · Shift bound · s bound · Real inv

Used byUpper bound

LemmaAlgebra step#

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

Lean

Formalized as lem_finalAlgebra.

Sources

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

Leanlem_finalAlgebra

Used by 1

Used byUpper bound

LemmaUpper bound#

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

Lean

Formalized as lem_zetaUppBd.

Sources

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

Leanlem_zetaUppBd

Uses 2 · Used by 1

Proof usesCombine bounds · Algebra step

Used byGlobal bound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.