Sum bound to Real sum

LemmaSum bound#

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

Lean

Formalized as lem_Z1splitge2.

Sources

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

Leanlem_Z1splitge2

Uses 2 · Used by 1

Proof usesSplit bound · Real inverse

Used byReal bound

LemmaReal bound#

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

Lean

Formalized as lem_Z1splitge3.

Sources

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

Leanlem_Z1splitge3

Uses 2 · Used by 1

Proof usesSum split · Sum bound

Used byZeta bound

LemmaIn set#

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

Lean

Formalized as lem_rho_in_Zt.

Sources

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

Leanlem_rho_in_Zt

Used by 2

Used bySplit sum · Zeta bound

LemmaZeta bound#

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

Lean

Formalized as Z1bound.

Sources

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

LeanZ1bound

Uses 3 · Used by 1

Proof usesSplit real · Real bound · In set

Used byCombined bound

LemmaAt one#

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

Lean

Formalized as Z0bound.

Sources

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

LeanZ0bound

Used by 2

Used byOne bound · Real one

LemmaReal one#

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

Lean

Formalized as Z0boundRe.

Sources

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

LeanZ0boundRe

Uses 1

Proof usesAt one

LemmaOne bound#

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

Lean

Formalized as Z0bound_const.

Sources

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

LeanZ0bound_const

Uses 1 · Used by 2

Proof usesAt one

Used byReal bound · Log bound

LemmaReal bound#

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

Lean

Formalized as Z0boundRe_const.

Sources

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

LeanZ0boundRe_const

Uses 1 · Used by 1

Proof usesOne bound

Used byReal sum

LemmaReal sum#

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

Lean

Formalized as Z0boundRe_const2.

Sources

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

LeanZ0boundRe_const2

Uses 1 · Used by 1

Proof usesReal bound

Used byReal diff

LemmaReal diff#

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

Lean

Formalized as Z0boundRe_const3.

Sources

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

LeanZ0boundRe_const3

Uses 1 · Used by 1

Proof usesReal sum

Used byCombined bound

LemmaCombined bound#

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

Lean

Formalized as Z341bounds_const.

Sources

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

LeanZ341bounds_const

Uses 4 · Used by 1

Proof usesReal diff · Zeta bound · Shift bound · Three exceeds e

Used byInequality

LemmaSeries form#

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

Lean

Formalized as zeta1zetaseries.

Sources

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

Leanzeta1zetaseries

Uses 1 · Used by 1

Proof usesLog derivative

Used bySeries form

LemmaSeries form#

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

Lean

Formalized as zeta1zetaseriesxy.

Sources

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

Leanzeta1zetaseriesxy

Uses 1 · Used by 1

Proof usesSeries form

Used bySeries split

LemmaConverges#

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

Lean

Formalized as Zconverges1.

Sources

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

LeanZconverges1

Uses 1 · Used by 2

Proof usesLog derivative

Used byReal converges · Series converges

LemmaReal converges#

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

Lean

Formalized as ReZconverges1.

Sources

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

LeanReZconverges1

Uses 1 · Used by 1

Proof usesConverges

Used byCos series

LemmaExponent split#

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

Lean

Formalized as lem_nxy.

Sources

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

Leanlem_nxy

Uses 1 · Used by 1

Proof usesExp rule

Used bySeries split

LemmaSeries split#

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

Lean

Formalized as lem_zeta1zetaseriesxy2.

Sources

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

Leanlem_zeta1zetaseriesxy2

Uses 2 · Used by 2

Proof usesSeries form · Exponent split

Used bySeries converges · Series real

LemmaSeries converges#

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

Lean

Formalized as Zseriesconverges1.

Sources

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

LeanZseriesconverges1

Uses 2 · Used by 1

Proof usesConverges · Series split

Used byReal sum

LemmaReal terms#

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

Lean

Formalized as lem_realnx.

Sources

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

Leanlem_realnx

Used by 2

Used byTerm nonneg · Real factor

LemmaReal sum#

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

Lean

Formalized as sumRealLambda.

Sources

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

LeansumRealLambda

Uses 2 · Used by 1

Proof usesSeries converges · Real series

Used bySeries real

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.