Square expand to Scaled triangle

LemmaSquare expand#

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

Lean

Formalized as lem_casq.

Sources

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

Leanlem_casq

Used by 1

Used bySquare diff

LemmaSquare diff#

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

Lean

Formalized as lem_casq2.

Sources

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

Leanlem_casq2

Uses 1 · Used by 1

Proof usesSquare expand

Used byMod diff

LemmaMod diff#

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

Lean

Formalized as lem_diffmods2.

Sources

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

Leanlem_diffmods2

Uses 2 · Used by 1

Proof usesMod diff · Square diff

Used byModulus diff

LemmaModulus diff#

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

Lean

Formalized as lem_modulus_sq_ReImw.

Sources

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

Leanlem_modulus_sq_ReImw

Uses 1 · Used by 1

Proof usesMod diff

Used byModulus identity

LemmaModulus identity#

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

Lean

Formalized as lem_modulus_sq_identity.

Sources

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

Leanlem_modulus_sq_identity

Uses 2 · Used by 1

Proof usesModulus diff · Real imaginary

Used byModulus compare

LemmaNonneg product#

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

Lean

Formalized as lem_nonnegative_product.

Sources

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

Leanlem_nonnegative_product

Used by 1

Used byNonneg product

LemmaNonneg product#

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

Lean

Formalized as lem_nonnegative_product2.

Sources

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

Leanlem_nonnegative_product2

Uses 1 · Used by 1

Proof usesNonneg product

Used byModulus compare

LemmaModulus compare#

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

Lean

Formalized as lem_nonnegative_product3.

Sources

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

Leanlem_nonnegative_product3

Uses 2 · Used by 1

Proof usesModulus identity · Nonneg product

Used byModulus bound

LemmaModulus bound#

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

Lean

Formalized as lem_nonnegative_product4.

Sources

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

Leanlem_nonnegative_product4

Uses 1 · Used by 1

Proof usesModulus compare

Used byModulus bound

LemmaModulus bound#

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

Lean

Formalized as lem_nonnegative_product5.

Sources

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

Leanlem_nonnegative_product5

Uses 1 · Used by 1

Proof usesModulus bound

Used byModulus order

LemmaModulus order#

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

Lean

Formalized as lem_nonnegative_product6.

Sources

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

Leanlem_nonnegative_product6

Uses 1 · Used by 2

Proof usesModulus bound

Used byRatio bound · Ratio bound

LemmaDivide inequality#

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

Lean

Formalized as lem_ineqmultr.

Sources

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

Leanlem_ineqmultr

Used by 3

Used byRatio bound · Scaled triangle · Divide bound

LemmaRatio bound#

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

Lean

Formalized as lem_ineqmultrbb.

Sources

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

Leanlem_ineqmultrbb

Uses 1 · Used by 1

Proof usesDivide inequality

Used byRatio bound

LemmaRatio bound#

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

Lean

Formalized as lem_nonnegative_product7.

Sources

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

Leanlem_nonnegative_product7

Uses 3 · Used by 1

Proof uses2M minus mod · Modulus order · Ratio bound

Used byRatio bound

LemmaRatio bound#

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

Lean

Formalized as lem_nonnegative_product8.

Sources

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

Leanlem_nonnegative_product8

Uses 2 · Used by 1

Proof uses2M minus mod · Ratio bound

Used byRatio bound

LemmaRatio bound#

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

Lean

Formalized as lem_nonnegative_product9.

Sources

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

Leanlem_nonnegative_product9

Uses 2 · Used by 1

Proof usesModulus order · Ratio bound

Used byRatio bound

LemmaTriangle inequality#

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

Lean

Formalized as lem_triangle_ineq.

Sources

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

Leanlem_triangle_ineq

Used by 2

Used byScaled triangle · Triangle minus

LemmaTriangle minus#

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

Lean

Formalized as lem_triangleineqminus.

Sources

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

Leanlem_triangleineqminus

Uses 1

Proof usesTriangle inequality

LemmaScaled triangle#

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

Lean

Formalized as lem_rtriangle.

Sources

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

Leanlem_rtriangle

Uses 2 · Used by 1

Proof usesTriangle inequality · Divide inequality

Used byScaled triangle

LemmaScaled triangle#

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

Lean

Formalized as rtriangle2.

Sources

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

Leanrtriangle2

Uses 1 · Used by 1

Proof usesScaled triangle

Used byIneq step

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.