Ineq step to Product analytic

LemmaIneq step#

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

Lean

Formalized as lem_rtriangle3.

Sources

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

Leanlem_rtriangle3

Uses 1 · Used by 1

Proof usesScaled triangle

Used byRearranged bound

LemmaRearranged bound#

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

Lean

Formalized as lem_rtriangle4.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT1_ComplexAnalysis.tex, line 455

Leanlem_rtriangle4

Uses 1 · Used by 1

Proof usesIneq step

Used byKey bound

LemmaAbs positive#

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

Lean

Formalized as lem_absposeq.

Sources

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

Leanlem_absposeq

Used by 1

Used byScaled abs

LemmaDouble positive#

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

Lean

Formalized as lem_a2a.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT1_ComplexAnalysis.tex, line 468

Leanlem_a2a

Used by 1

Used byScaled abs

LemmaScaled abs#

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

Lean

Formalized as lem_absposeq2.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT1_ComplexAnalysis.tex, line 474

Leanlem_absposeq2

Uses 2 · Used by 1

Proof usesAbs positive · Double positive

Used byKey bound

LemmaKey bound#

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

Lean

Formalized as lem_rtriangle5.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT1_ComplexAnalysis.tex, line 481

Leanlem_rtriangle5

Uses 2 · Used by 1

Proof usesRearranged bound · Scaled abs

Used byFinal bound

LemmaNonneg factor#

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

Lean

Formalized as lem_RrFpos.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT1_ComplexAnalysis.tex, line 488

Leanlem_RrFpos

Used by 1

Used byDivide bound

LemmaDivide bound#

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

Lean

Formalized as lem_rtriangle6.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT1_ComplexAnalysis.tex, line 494

Leanlem_rtriangle6

Uses 2 · Used by 1

Proof usesDivide inequality · Nonneg factor

Used byFinal bound

LemmaFinal bound#

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

Lean

Formalized as lem_rtriangle7.

Sources

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

Leanlem_rtriangle7

Uses 2 · Used by 1

Proof usesKey bound · Divide bound

Used byCircle bound

LemmaOrder nonzero#

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

Lean

Formalized as lem_orderne0.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT1_ComplexAnalysis.tex, line 509

Leanlem_orderne0

Used by 1

Used byDivide zero

LemmaOrder natural#

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

Lean

Formalized as lem_ordernetop.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT1_ComplexAnalysis.tex, line 519

Leanlem_ordernetop

Used by 1

Used byDivide zero

LemmaFactor power#

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

Lean

Formalized as lem_ordernatcast.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT1_ComplexAnalysis.tex, line 530

Leanlem_ordernatcast

Used by 1

Used byFactor linear

LemmaFactor linear#

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

Lean

Formalized as lem_ordernatcast1.

Sources

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

Leanlem_ordernatcast1

Uses 1 · Used by 1

Proof usesFactor power

Used byDivide zero

LemmaDivide zero#

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

Lean

Formalized as lem_ordernatcast2.

Sources

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

Leanlem_ordernatcast2

Uses 3 · Used by 1

Proof usesOrder natural · Factor linear · Order nonzero

Used byRemovable zero

LemmaAnalytic mono#

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

Lean

Formalized as lem_analmono.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT1_ComplexAnalysis.tex, line 577

Leanlem_analmono

Used by 2

Used byInverse analytic · Product analytic

LemmaNonzero subset#

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

Lean

Formalized as lem_not0mono.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT1_ComplexAnalysis.tex, line 587

Leanlem_not0mono

Used by 1

Used byInverse analytic

LemmaInverse analytic#

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

Lean

Formalized as lem_1zanalDR.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT1_ComplexAnalysis.tex, line 597

Leanlem_1zanalDR

Uses 2 · Used by 1

Proof usesNonzero subset · Analytic mono

Used byQuotient analytic

LemmaProduct analytic#

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

Lean

Formalized as lem_analprod.

Sources

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

Leanlem_analprod

Used by 1

Used byProduct analytic

LemmaProduct analytic#

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

Lean

Formalized as lem_analprodST.

Sources

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

Leanlem_analprodST

Uses 2 · Used by 1

Proof usesProduct analytic · Analytic mono

Used byProduct analytic

LemmaProduct analytic#

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

Lean

Formalized as lem_analprodTDR.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT1_ComplexAnalysis.tex, line 632

Leanlem_analprodTDR

Uses 1 · Used by 1

Proof usesProduct analytic

Used byQuotient analytic

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.