Derivative bound to Square identity

LemmaDerivative bound#

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

Lean

Formalized as lem_f_prime_bound_by_integral_of_constant.

Sources
Leanlem_f_prime_bound_by_integral_of_constant
Uses 3 · Used by 1
Proof usesModulus of \(f'\) · Integrand bound · Integral inequality
Used byDerivative bound

LemmaIntegrate one#

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

Lean

Formalized as lem_integral_of_1.

Sources
Leanlem_integral_of_1
Used by 1
Used byExponential integral

LemmaExponential integral#

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

Lean

Formalized as lem_integral_2.

Sources
Leanlem_integral_2
Uses 1 · Used by 1
Proof usesIntegrate one
Used byDerivative bound

LemmaDerivative bound#

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

Lean

Formalized as lem_f_prime_bound.

Sources
Leanlem_f_prime_bound
Uses 2 · Used by 1
Proof usesDerivative bound · Exponential integral
Used byBorel-Carathéodory II

LemmaRadius compare#

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

Lean

Formalized as lem_r_prime_gt_r.

Sources
Leanlem_r_prime_gt_r
Used by 1
Used byIntermediate radius

LemmaRadius compare#

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

Lean

Formalized as lem_r_prime_lt_R.

Sources
Leanlem_r_prime_lt_R
Used by 1
Used byIntermediate radius

LemmaIntermediate radius#

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

Lean

Formalized as lem_r_prime_is_intermediate.

Sources
Leanlem_r_prime_is_intermediate
Uses 2 · Used by 1
Proof usesRadius compare · Radius compare
Used byBorel-Carathéodory II

LemmaRadius formula#

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

Lean

Formalized as lem_calc_R_minus_r_prime.

Sources
Leanlem_calc_R_minus_r_prime
Used by 1
Used byDenominator form

LemmaRadius formula#

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

Lean

Formalized as lem_calc_r_prime_minus_r.

Sources
Leanlem_calc_r_prime_minus_r
Used by 1
Used byDenominator form

LemmaDenominator form#

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

Lean

Formalized as lem_calc_denominator_specific.

Sources
Leanlem_calc_denominator_specific
Uses 2 · Used by 1
Proof usesRadius formula · Radius formula
Used byFraction simplify

LemmaNumerator form#

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

Lean

Formalized as lem_calc_numerator_specific.

Sources
Leanlem_calc_numerator_specific
Used by 1
Used byFraction simplify

LemmaFraction simplify#

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

Lean

Formalized as lem_frac_simplify.

Sources
Leanlem_frac_simplify
Uses 2 · Used by 1
Proof usesNumerator form · Denominator form
Used byFraction simplify

LemmaFraction simplify#

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

Lean

Formalized as lem_frac_simplify2.

Sources
Leanlem_frac_simplify2
Used by 1
Used byFraction simplify

LemmaFraction simplify#

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

Lean

Formalized as lem_frac_simplify3.

Sources
Leanlem_frac_simplify3
Uses 2 · Used by 1
Proof usesFraction simplify · Fraction simplify
Used byFraction simplify

LemmaInequality fact#

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

Lean

Formalized as lem_ineq_R_plus_r_lt_2R.

Sources
Leanlem_ineq_R_plus_r_lt_2R
Used by 1
Used bySquare bound

LemmaSum positive#

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

Lean

Formalized as lem_R_plus_r_is_positive.

Sources
Leanlem_R_plus_r_is_positive
Used by 1
Used bySquare bound

LemmaDouble positive#

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

Lean

Formalized as lem_2R_is_positive.

Sources
Leanlem_2R_is_positive
Used by 1
Used bySquare bound

LemmaSquare fact#

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

Lean

Formalized as lem_square_inequality_strict.

Sources
Leanlem_square_inequality_strict
Used by 1
Used bySquare bound

LemmaSquare bound#

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

Lean

Formalized as lem_ineq_R_plus_r_sq_lt_2R_sq.

Sources
Leanlem_ineq_R_plus_r_sq_lt_2R_sq
Uses 4 · Used by 1
Proof usesSum positive · Double positive · Inequality fact · Square fact
Used bySquare bound

LemmaSquare identity#

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

Lean

Formalized as lem_2R_sq_is_4R_sq.

Sources
Leanlem_2R_sq_is_4R_sq
Used by 1
Used bySquare bound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.