Cauchy's Integral Formula for… to Reverse triangle

LemmaCauchy's Integral Formula for \(f'\)#

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

Lean

Formalized as cauchy_formula_deriv.

Sources

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

Leancauchy_formula_deriv

Used by 1

Used byCIF for \(f'\), Parameterized

LemmaDifferential of \(w(t)\)#

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

Lean

Formalized as lem_dw_dt.

Sources

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

Leanlem_dw_dt

Used by 1

Used byCIF for \(f'\), Parameterized

LemmaCIF for \(f'\), Parameterized#

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

Lean

Formalized as lem_CIF_deriv_param.

Sources

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

Leanlem_CIF_deriv_param

Uses 2 · Used by 1

Proof usesCauchy's Integral Formula for \(f'\) · Differential of \(w(t)\)

Used byCIF for \(f'\), Simplified

LemmaCIF for \(f'\), Simplified#

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

Lean

Formalized as lem_CIF_deriv_simplified.

Sources

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

Leanlem_CIF_deriv_simplified

Uses 1 · Used by 1

Proof usesCIF for \(f'\), Parameterized

Used byDerivative modulus

LemmaDerivative modulus#

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

Lean

Formalized as lem_modulus_of_f_prime0.

Sources

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

Leanlem_modulus_of_f_prime0

Uses 1 · Used by 1

Proof usesCIF for \(f'\), Simplified

Used byModulus of \(f'\)

LemmaIntegral bound#

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

Lean

Formalized as lem_integral_modulus_inequality.

Sources

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

Leanlem_integral_modulus_inequality

Used by 1

Used byModulus of \(f'\)

LemmaModulus of \(f'\)#

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

Lean

Formalized as lem_modulus_of_f_prime.

Sources

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

Leanlem_modulus_of_f_prime

Uses 2 · Used by 1

Proof usesDerivative modulus · Integral bound

Used byDerivative bound

LemmaIntegrand modulus#

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

Lean

Formalized as lem_modulus_of_integrand_product2.

Sources

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

Leanlem_modulus_of_integrand_product2

Used by 1

Used byIntegrand modulus

LemmaModulus one#

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

Lean

Formalized as lem_modeit.

Sources

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

Leanlem_modeit

Used by 1

Used byUnit modulus

LemmaCosine part#

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

Lean

Formalized as lem_Reit0.

Sources

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

Leanlem_Reit0

Used by 1

Used byEuler part

LemmaEuler part#

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

Lean

Formalized as lem_eReite0.

Sources

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

Leanlem_eReite0

Uses 1 · Used by 1

Proof usesCosine part

Used byCosine relation

LemmaExp zero one#

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

Lean

Formalized as lem_e01.

Sources

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

Leanlem_e01

Used by 1

Used byCosine relation

LemmaCosine relation#

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

Lean

Formalized as lem_eReit1.

Sources

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

Leanlem_eReit1

Uses 2 · Used by 1

Proof usesEuler part · Exp zero one

Used byUnit modulus

LemmaUnit modulus#

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

Lean

Formalized as lem_modulus_of_e_it_is_one.

Sources

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

Leanlem_modulus_of_e_it_is_one

Uses 2 · Used by 1

Proof usesModulus one · Cosine relation

Used byScaled modulus

LemmaScaled modulus#

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

Lean

Formalized as lem_modulus_of_ae_it.

Sources

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

Leanlem_modulus_of_ae_it

Uses 1 · Used by 3

Proof usesUnit modulus

Used byIntegrand modulus · Point bound · Reverse triangle

LemmaIntegrand modulus#

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

Lean

Formalized as lem_modulus_of_integrand_product3.

Sources

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

Leanlem_modulus_of_integrand_product3

Uses 2 · Used by 1

Proof usesIntegrand modulus · Scaled modulus

Used byProduct modulus

LemmaSquare modulus#

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

Lean

Formalized as lem_modulus_of_square.

Sources

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

Leanlem_modulus_of_square

Used by 2

Used byShifted modulus · Radius relation

LemmaShifted modulus#

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

Lean

Formalized as lem_modulus_wz.

Sources

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

Leanlem_modulus_wz

Uses 1 · Used by 1

Proof usesSquare modulus

Used byIntegrand modulus

LemmaReverse triangle#

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

Lean

Formalized as lem_reverse_triangle.

Sources

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

Leanlem_reverse_triangle

Used by 1

Used byReverse triangle

LemmaReverse triangle#

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

Lean

Formalized as lem_reverse_triangle2.

Sources

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

Leanlem_reverse_triangle2

Uses 1 · Used by 1

Proof usesReverse triangle

Used byReverse triangle

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.