Max principle to Rearranged bound

LemmaMax principle#

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

Lean

Formalized as lem_HardMMP.

Sources
Leanlem_HardMMP
Uses 1 · Used by 2
Proof usesBoundary max
Used byMaximum modulus principle · Max modulus

LemmaEasy maximum principle#

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

Lean

Formalized as lem_EasyMMP.

Sources
Leanlem_EasyMMP
Used by 1
Used byMaximum modulus principle

LemmaMaximum modulus principle#

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

Lean

Formalized as lem_MMP.

Sources
Leanlem_MMP
Uses 2 · Used by 2
Proof usesMax principle · Easy maximum principle
Used byInterior bound · BC bound

LemmaDenom nonzero#

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

Lean

Formalized as lem_denominator_nonzero.

Sources
Leanlem_denominator_nonzero
Uses 1 · Used by 2
Proof uses2M minus nonzero
Used byg analytic · g modulus

LemmaRatio bound#

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

Lean

Formalized as lem_f_vs_2M_minus_f.

Sources
Leanlem_f_vs_2M_minus_f
Uses 1 · Used by 1
Proof usesRatio bound
Used byScaled ratio

LemmaRemovable zero#

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

Lean

Formalized as lem_removable_singularity.

Sources
Leanlem_removable_singularity
Uses 3 · Used by 1
Proof usesDivide zero · Local to global · Quotient analytic
Used byg analytic

LemmaQuotient analytic#

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

Lean

Formalized as lem_quotient_analytic.

Sources
Leanlem_quotient_analytic
Used by 1
Used byg analytic

DefinitionModified function#

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

Lean

Formalized as f_M.

Sources
Leanf_M
Used by 2
Used byg analytic · g modulus

Lemmag analytic#

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

Lean

Formalized as lem_g_analytic.

Sources
Leanlem_g_analytic
Uses 4 · Used by 1
Proof usesModified function · Quotient analytic · Removable zero · Denom nonzero
Used byInterior bound

LemmaQuotient modulus#

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

Lean

Formalized as lem_absab.

Sources
Leanlem_absab
Used by 1
Used byg modulus

Lemmag modulus#

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

Lean

Formalized as lem_g_on_boundaryz.

Sources
Leanlem_g_on_boundaryz
Uses 3 · Used by 2
Proof usesModified function · Quotient modulus · Denom nonzero
Used byg at r · Boundary g

LemmaQuotient radius#

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

Lean

Formalized as lem_fzzR.

Sources
Leanlem_fzzR
Used by 2
Used byg at r · Boundary g

LemmaBoundary g#

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

Lean

Formalized as lem_g_on_boundary.

Sources
Leanlem_g_on_boundary
Uses 2 · Used by 1
Proof usesg modulus · Quotient radius
Used byBoundary bound

LemmaScaled ratio#

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

Lean

Formalized as lem_f_vs_2M_minus_fR.

Sources
Leanlem_f_vs_2M_minus_fR
Uses 1 · Used by 1
Proof usesRatio bound
Used byBoundary bound

LemmaBoundary bound#

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

Lean

Formalized as lem_g_boundary_bound0.

Sources
Leanlem_g_boundary_bound0
Uses 2 · Used by 1
Proof usesBoundary g · Scaled ratio
Used byInterior bound

LemmaInterior bound#

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

Lean

Formalized as lem_g_interior_bound.

Sources
Leanlem_g_interior_bound
Uses 3 · Used by 1
Proof usesBoundary bound · Maximum modulus principle · g analytic
Used byg bound r

Lemmag at r#

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

Lean

Formalized as lem_g_at_r.

Sources
Leanlem_g_at_r
Uses 2 · Used by 1
Proof usesg modulus · Quotient radius
Used byg bound r

Lemmag bound r#

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

Lean

Formalized as lem_g_at_rR.

Sources
Leanlem_g_at_rR
Uses 2 · Used by 1
Proof usesInterior bound · g at r
Used byRearranged bound

LemmaFraction swap#

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

Lean

Formalized as lem_fracs.

Sources
Leanlem_fracs
Used by 1
Used byRearranged bound

LemmaRearranged bound#

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

Lean

Formalized as lem_f_bound_rearranged.

Sources
Leanlem_f_bound_rearranged
Uses 2 · Used by 1
Proof usesg bound r · Fraction swap
Used byCircle bound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.