Square bound to Borel-Carathéodory II

LemmaSquare bound#

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

Lean

Formalized as lem_ineq_R_plus_r_sq.

Sources
Leanlem_ineq_R_plus_r_sq
Uses 2 · Used by 1
Proof usesSquare bound · Square identity
Used bySquare bound

LemmaSquare bound#

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

Lean

Formalized as lem_ineq_R_plus_r_sqM.

Sources
Leanlem_ineq_R_plus_r_sqM
Uses 1 · Used by 1
Proof usesSquare bound
Used byBound simplify

LemmaBound simplify#

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

Lean

Formalized as lem_simplify_final_bound.

Sources
Leanlem_simplify_final_bound
Uses 1 · Used by 1
Proof usesSquare bound
Used byFraction simplify

LemmaFraction simplify#

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

Lean

Formalized as lem_bound_after_substitution.

Sources
Leanlem_bound_after_substitution
Uses 2 · Used by 1
Proof usesFraction simplify · Bound simplify
Used byBorel-Carathéodory II

TheoremBorel-Carathéodory II#

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

Lean

Formalized as borel_caratheodory_II.

Sources
Leanborel_caratheodory_II
Uses 3 · Used by 1
Proof usesDerivative bound · Fraction simplify · Intermediate radius
Used byBC inequality

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.