Series real to Inequality

LemmaSeries real#

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

Lean

Formalized as lem_sumRealZ.

Sources

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

Leanlem_sumRealZ

Uses 2 · Used by 1

Proof usesSeries split · Real sum

Used byReal series

LemmaReal factor#

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

Lean

Formalized as RealLambdaxy.

Sources

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

LeanRealLambdaxy

Uses 2 · Used by 1

Proof usesReal terms · Real scale

Used byReal series

LemmaReal series#

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

Lean

Formalized as ReZseriesRen.

Sources

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

LeanReZseriesRen

Uses 2 · Used by 1

Proof usesSeries real · Real factor

Used byCos form

LemmaCos form#

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

Lean

Formalized as Rezeta1zetaseries.

Sources

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

LeanRezeta1zetaseries

Uses 2 · Used by 4

Proof usesReal series · Real cosine

Used byDelta zero · Delta series · Delta double · Cos series

LemmaCos series#

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

Lean

Formalized as Rezetaseries_convergence.

Sources

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

LeanRezetaseries_convergence

Uses 2 · Used by 4

Proof usesReal converges · Cos form

Used byFactor form · Sum converges · Zero series · Double cos

LemmaDouble cos#

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

Lean

Formalized as Rezetaseries2t.

Sources

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

LeanRezetaseries2t

Uses 1 · Used by 2

Proof usesCos series

Used byFactor form · Sum converges

LemmaZero cos#

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

Lean

Formalized as lem_cost0.

Sources

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

Leanlem_cost0

Used by 2

Used byDelta zero · Zero series

LemmaZero series#

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

Lean

Formalized as Rezetaseries0.

Sources

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

LeanRezetaseries0

Uses 2 · Used by 2

Proof usesCos series · Zero cos

Used byFactor form · Sum converges

LemmaDelta series#

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

Lean

Formalized as Rezeta1zetaseries1.

Sources

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

LeanRezeta1zetaseries1

Uses 1 · Used by 1

Proof usesCos form

Used by341 series

LemmaDelta double#

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

Lean

Formalized as Rezeta1zetaseries2.

Sources

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

LeanRezeta1zetaseries2

Uses 1 · Used by 1

Proof usesCos form

Used by341 series

LemmaDelta zero#

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

Lean

Formalized as Rezeta1zetaseries0.

Sources

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

LeanRezeta1zetaseries0

Uses 2 · Used by 1

Proof usesCos form · Zero cos

Used by341 series

Lemma341 series#

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

Lean

Formalized as Z341series.

Sources

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

LeanZ341series

Uses 3 · Used by 1

Proof usesDelta zero · Delta series · Delta double

Used bySeries equal

LemmaSum converges#

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

Lean

Formalized as lem341seriesConv.

Sources

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

Leanlem341seriesConv

Uses 3 · Used by 1

Proof usesZero series · Cos series · Double cos

Used byFactor conv

LemmaFactor form#

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

Lean

Formalized as lem341series.

Sources

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

Leanlem341series

Uses 3 · Used by 2

Proof usesZero series · Cos series · Double cos

Used bySeries equal · Factor conv

LemmaFactor conv#

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

Lean

Formalized as lem_341seriesConverge.

Sources

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

Leanlem_341seriesConverge

Uses 2 · Used by 1

Proof usesSum converges · Factor form

Used bySeries nonneg

LemmaSeries equal#

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

Lean

Formalized as lem_341series2.

Sources

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

Leanlem_341series2

Uses 2 · Used by 1

Proof uses341 series · Factor form

Used byPositive sum

LemmaTerm nonneg#

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

Lean

Formalized as lem_Lambda_pos_trig_sum.

Sources

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

Leanlem_Lambda_pos_trig_sum

Uses 2 · Used by 1

Proof usesTrig positive · Real terms

Used bySeries nonneg

LemmaSeries nonneg#

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

Lean

Formalized as lem_seriespos.

Sources

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

Leanlem_seriespos

Uses 4 · Used by 1

Proof usesFactor conv · Trig positive · Series positive · Term nonneg

Used byPositive sum

LemmaPositive sum#

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

Lean

Formalized as Z341pos.

Sources

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

LeanZ341pos

Uses 2 · Used by 1

Proof usesSeries equal · Series nonneg

Used byInequality

LemmaInequality#

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

Lean

Formalized as lem341tsC.

Sources

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

Leanlem341tsC

Uses 3 · Used by 1

Proof usesCombined bound · Positive sum · Three exceeds e

Used byRearranged

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.