Series form to Integral conv

LemmaSeries form#

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

Lean

Formalized as lem_zetaLimit.

Sources

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

Leanlem_zetaLimit

Used by 1

Used byZeta formula

DefinitionPartial sum#

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

Lean

Formalized as zetaPartialSum.

Sources

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

LeanzetaPartialSum

Used by 5

Used byApply Abel · Sum identity · Final form · First form · Second form

LemmaAbel sum#

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

Lean

Formalized as lem_abelSummation.

Sources

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

Leanlem_abelSummation

Used by 1

Used byApply Abel

LemmaSum identity#

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

Lean

Formalized as lem_partialSumIsZetaN.

Sources

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

Leanlem_partialSumIsZetaN

Uses 1 · Used by 1

Statement usesPartial sum

Used byApply Abel

LemmaCount sum#

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

Lean

Formalized as lem_sumOfAn.

Sources

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

Leanlem_sumOfAn

Used by 1

Used byApply Abel

LemmaPower deriv#

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

Lean

Formalized as lem_fDeriv.

Sources

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

Leanlem_fDeriv

Used by 1

Used byApply Abel

LemmaApply Abel#

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

Lean

Formalized as lem_applyAbel.

Sources

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

Leanlem_applyAbel

Uses 5 · Used by 1

Statement usesPartial sum

Proof usesAbel sum · Sum identity · Count sum · Power deriv

Used byFirst form

LemmaFloor int#

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

Lean

Formalized as lem_floorNisN.

Sources

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

Leanlem_floorNisN

Used by 1

Used byFirst form

LemmaFirst form#

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

Lean

Formalized as lem_zetaNsimplified1.

Sources

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

Leanlem_zetaNsimplified1

Uses 3 · Used by 1

Statement usesPartial sum

Proof usesApply Abel · Floor int

Used bySecond form

LemmaFloor split#

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

Lean

Formalized as lem_floorUdecomp.

Sources

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

Leanlem_floorUdecomp

Used by 1

Used byIntegral split

LemmaIntegral split#

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

Lean

Formalized as lem_integralSplit.

Sources

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

Leanlem_integralSplit

Uses 1 · Used by 1

Proof usesFloor split

Used bySecond form

LemmaSecond form#

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

Lean

Formalized as lem_zetaNsimplified2.

Sources

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

Leanlem_zetaNsimplified2

Uses 3 · Used by 1

Statement usesPartial sum

Proof usesFirst form · Integral split

Used byFinal form

LemmaMain integral#

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

Lean

Formalized as lem_evalMainIntegral.

Sources

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

Leanlem_evalMainIntegral

Used by 1

Used byFinal form

LemmaFinal form#

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

Lean

Formalized as lem_zetaNfinal.

Sources

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

Leanlem_zetaNfinal

Uses 3 · Used by 1

Statement usesPartial sum

Proof usesSecond form · Main integral

Used byZeta formula

LemmaLimit term#

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

Lean

Formalized as lem_limitTerm1.

Sources

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

Leanlem_limitTerm1

Used by 1

Used byZeta formula

LemmaFrac bound#

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

Lean

Formalized as lem_fracPartBound.

Sources

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

Leanlem_fracPartBound

Used by 1

Used byTerm bound

LemmaTerm bound#

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

Lean

Formalized as lem_integrandBound.

Sources

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

Leanlem_integrandBound

Uses 1 · Used by 2

Proof usesFrac bound

Used byEps bound · Second bound

LemmaEps bound#

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

Lean

Formalized as lem_integrandBoundeps.

Sources

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

Leanlem_integrandBoundeps

Uses 1 · Used by 1

Proof usesTerm bound

Used byIntegral conv

LemmaTriangle int#

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

Lean

Formalized as lem_triangleInequality_add.

Sources

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

Leanlem_triangleInequality_add

Used by 3

Used byIntegral conv · Inverse mod · First bound

LemmaIntegral conv#

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

Lean

Formalized as lem_integralConvergence.

Sources

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

Leanlem_integralConvergence

Uses 2 · Used by 2

Proof usesTriangle int · Eps bound

Used byZeta formula · Analytic ext

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.