Circle bound to Borel-Carathéodory I

LemmaCircle bound#

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

Lean

Formalized as lem_final_bound_on_circle0.

Sources

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

Leanlem_final_bound_on_circle0

Uses 2 · Used by 1

Proof usesRearranged bound · Final bound

Used byCircle bound

LemmaCircle bound#

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

Lean

Formalized as lem_final_bound_on_circle.

Sources

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

Leanlem_final_bound_on_circle

Uses 1 · Used by 1

Proof usesCircle bound

Used byBC bound

LemmaBC bound#

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

Lean

Formalized as lem_BCI.

Sources

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

Leanlem_BCI

Uses 2 · Used by 2

Proof usesCircle bound · Maximum modulus principle

Used byBorel-Carathéodory I · Point bound

TheoremBorel-Carathéodory I#

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

Lean

Formalized as thm_BorelCaratheodoryI.

Sources

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

Leanthm_BorelCaratheodoryI

Uses 1

Proof usesBC bound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.