Reverse triangle to Integral inequality

LemmaReverse triangle#

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

Lean

Formalized as lem_reverse_triangle3.

Sources

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

Leanlem_reverse_triangle3

Uses 2 · Used by 2

Proof usesReverse triangle · Scaled modulus

Used byReverse triangle · Radius relation

LemmaRadius relation#

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

Lean

Formalized as lem_zrr1.

Sources

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

Leanlem_zrr1

Used by 1

Used byReverse triangle

LemmaRadius relation#

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

Lean

Formalized as lem_zrr2.

Sources

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

Leanlem_zrr2

Uses 1 · Used by 1

Proof usesReverse triangle

Used byRadius relation

LemmaRadius relation#

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

Lean

Formalized as lem_rr11.

Sources

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

Leanlem_rr11

Used by 1

Used byRadius relation

LemmaRadius relation#

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

Lean

Formalized as lem_rr12.

Sources

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

Leanlem_rr12

Uses 1 · Used by 1

Proof usesRadius relation

Used byRadius relation

LemmaRadius relation#

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

Lean

Formalized as lem_zrr3.

Sources

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

Leanlem_zrr3

Uses 2 · Used by 1

Proof usesRadius relation · Radius relation

Used byProduct modulus

LemmaRadius relation#

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

Lean

Formalized as lem_zrr4.

Sources

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

Leanlem_zrr4

Uses 1 · Used by 1

Proof usesSquare modulus

Used byProduct modulus

LemmaReverse triangle#

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

Lean

Formalized as lem_reverse_triangle4.

Sources

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

Leanlem_reverse_triangle4

Uses 2 · Used by 1

Proof usesReverse triangle · Radius relation

Used byReverse triangle

LemmaPositive nonzero#

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

Lean

Formalized as lem_wposneq0.

Sources

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

Leanlem_wposneq0

Used by 1

Used byReverse triangle

LemmaReverse triangle#

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

Lean

Formalized as lem_reverse_triangle5.

Sources

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

Leanlem_reverse_triangle5

Uses 2 · Used by 1

Proof usesReverse triangle · Positive nonzero

Used byReverse triangle

LemmaReverse triangle#

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

Lean

Formalized as lem_reverse_triangle6.

Sources

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

Leanlem_reverse_triangle6

Uses 1 · Used by 1

Proof usesReverse triangle

Used byIntegrand modulus

LemmaDivision bound#

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

Lean

Formalized as lem_absdiv.

Sources

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

Leanlem_absdiv

Used by 1

Used byIntegrand modulus

LemmaIntegrand modulus#

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

Lean

Formalized as lem_modulus_of_integrand_product.

Sources

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

Leanlem_modulus_of_integrand_product

Uses 3 · Used by 1

Proof usesDivision bound · Reverse triangle · Shifted modulus

Used byProduct modulus

LemmaProduct modulus#

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

Lean

Formalized as lem_modulus_of_product.

Sources

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

Leanlem_modulus_of_product

Uses 2 · Used by 1

Proof usesIntegrand modulus · Integrand modulus

Used byProduct modulus

LemmaProduct modulus#

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

Lean

Formalized as lem_modulus_of_product2.

Sources

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

Leanlem_modulus_of_product2

Uses 2 · Used by 1

Proof usesProduct modulus · Radius relation

Used byProduct modulus

LemmaProduct modulus#

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

Lean

Formalized as lem_modulus_of_product3.

Sources

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

Leanlem_modulus_of_product3

Uses 1 · Used by 1

Proof usesRadius relation

Used byProduct modulus

LemmaProduct modulus#

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

Lean

Formalized as lem_modulus_of_product4.

Sources

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

Leanlem_modulus_of_product4

Uses 2 · Used by 1

Proof usesProduct modulus · Product modulus

Used byIntegrand bound

LemmaPoint bound#

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

Lean

Formalized as lem_bound_on_f_at_r_prime.

Sources

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

Leanlem_bound_on_f_at_r_prime

Uses 2 · Used by 1

Proof usesScaled modulus · BC bound

Used byIntegrand bound

LemmaIntegrand bound#

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

Lean

Formalized as lem_bound_on_integrand_modulus.

Sources

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

Leanlem_bound_on_integrand_modulus

Uses 2 · Used by 1

Proof usesProduct modulus · Point bound

Used byDerivative bound

LemmaIntegral inequality#

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

Lean

Formalized as lem_integral_inequality.

Sources

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

Leanlem_integral_inequality

Used by 1

Used byDerivative bound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.