Open disk to Boundary max

DefinitionOpen disk#

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

Lean

Formalized as ballDR.

Sources

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

LeanballDR

Used by 2

Used byOutside disk bound · Positive radius belongs to its closed disk

LemmaDisk closure#

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

Lean

Formalized as lem_ballDR.

Sources

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

Leanlem_ballDR

Used by 2

Used byIn disk bound · Interior max

LemmaIn disk bound#

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

Lean

Formalized as lem_inDR.

Sources

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

Leanlem_inDR

Uses 1 · Used by 2

Proof usesDisk closure

Used byBoundary modulus · Boundary point

LemmaOutside disk bound#

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

Lean

Formalized as lem_notinDR.

Sources

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

Leanlem_notinDR

Uses 1 · Used by 1

Proof usesOpen disk

Used byBoundary modulus

LemmaModulus equal#

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

Lean

Formalized as lem_legeR.

Sources

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

Leanlem_legeR

Used by 1

Used byBoundary modulus

LemmaBoundary modulus#

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

Lean

Formalized as lem_circleDR.

Sources

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

Leanlem_circleDR

Uses 3 · Used by 1

Proof usesIn disk bound · Outside disk bound · Modulus equal

Used byBoundary point

LemmaPositive modulus#

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

Lean

Formalized as lem_Rself.

Sources

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

Leanlem_Rself

Used by 1

Used byModulus bound

LemmaModulus bound#

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

Lean

Formalized as lem_Rself2.

Sources

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

Leanlem_Rself2

Uses 1 · Used by 1

Proof usesPositive modulus

Used byPositive radius belongs to its closed disk

LemmaPositive radius belongs to its closed disk#

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

Lean

Formalized as lem_Rself3.

Sources

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

Leanlem_Rself3

Uses 2 · Used by 1

Proof usesModulus bound · Open disk

Used byBoundary value

LemmaCompactness#

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

Lean

Formalized as lem_DRcompact.

Sources

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

Leanlem_DRcompact

Used by 2

Used byDisk Boundary · Zeros accumulate

LemmaExtrValThm#

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

Lean

Formalized as lem_ExtrValThm.

Sources

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

Leanlem_ExtrValThm

Used by 1

Used byDisk Boundary

LemmaDisk Boundary#

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

Lean

Formalized as lem_ExtrValThmDR.

Sources

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

Leanlem_ExtrValThmDR

Uses 2 · Used by 1

Proof usesCompactness · ExtrValThm

Used byMax modulus

LemmaAnalytic Continuation#

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

Lean

Formalized as lem_AnalCont.

Sources

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

Leanlem_AnalCont

Used by 1

Used byMax modulus

LemmaMax modulus#

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

Lean

Formalized as lem_ExtrValThmh.

Sources

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

Leanlem_ExtrValThmh

Uses 2 · Used by 1

Proof usesDisk Boundary · Analytic Continuation

Used byBoundary point

LemmaInterior max#

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

Lean

Formalized as lem_MaxModP.

Sources

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

Leanlem_MaxModP

Uses 1 · Used by 2

Proof usesDisk closure

Used byBoundary value · Boundary bound

LemmaBoundary value#

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

Lean

Formalized as lem_MaxModR.

Sources

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

Leanlem_MaxModR

Uses 2 · Used by 1

Proof usesInterior max · Positive radius belongs to its closed disk

Used byBoundary bound

LemmaBoundary bound#

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

Lean

Formalized as lem_MaxModRR.

Sources

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

Leanlem_MaxModRR

Uses 2 · Used by 1

Proof usesInterior max · Boundary value

Used byBoundary point

LemmaBoundary point#

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

Lean

Formalized as lem_MaxModv2.

Sources

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

Leanlem_MaxModv2

Uses 3 · Used by 1

Proof usesMax modulus · Boundary bound · Boundary modulus

Used byBoundary point

LemmaBoundary point#

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

Lean

Formalized as lem_MaxModv3.

Sources

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

Leanlem_MaxModv3

Uses 2 · Used by 1

Proof usesBoundary point · In disk bound

Used byBoundary max

LemmaBoundary max#

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

Lean

Formalized as lem_MaxModv4.

Sources

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

Leanlem_MaxModv4

Uses 1 · Used by 1

Proof usesBoundary point

Used byMax principle

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.