Square nonneg to Mod diff

LemmaSquare nonneg#

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

Lean

Formalized as lem_SquarePos.

Sources

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

Leanlem_SquarePos

Used by 1

Used byDouble square

LemmaDouble square#

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

Lean

Formalized as lem_SquarePos2.

Sources

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

Leanlem_SquarePos2

Uses 1 · Used by 1

Proof usesSquare nonneg

Used byCos square

LemmaCos square#

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

Lean

Formalized as lem_SquarePoscos.

Sources

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

Leanlem_SquarePoscos

Uses 1 · Used by 1

Proof usesDouble square

Used byTrig positive

LemmaTrig positive#

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

Lean

Formalized as lem_postrig.

Sources

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

Leanlem_postrig

Uses 2 · Used by 1

Proof usesTrig identity · Cos square

Used byTrig positive

LemmaTrig positive#

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

Lean

Formalized as lem_postriglogn.

Sources

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

Leanlem_postriglogn

Uses 1 · Used by 2

Proof usesTrig positive

Used byTerm nonneg · Series nonneg

LemmaSeries positive#

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

Lean

Formalized as lem_seriesPos.

Sources

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

Leanlem_seriesPos

Used by 1

Used bySeries nonneg

LemmaReal part diff#

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

Lean

Formalized as real_part_of_diff.

Sources

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

Leanreal_part_of_diff

Used by 1

Used byReal part 2M

LemmaReal part 2M#

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

Lean

Formalized as real_part_of_diffz.

Sources

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

Leanreal_part_of_diffz

Uses 1 · Used by 2

Proof usesReal part diff

Used byReal part bound · Real part >0

LemmaInequality reversal#

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

Lean

Formalized as inequality_reversal.

Sources

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

Leaninequality_reversal

Used by 1

Used byReal part lower bound

LemmaReal part lower bound#

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

Lean

Formalized as real_part_lower_bound.

Sources

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

Leanreal_part_lower_bound

Uses 1 · Used by 2

Proof usesInequality reversal

Used byReal part bound · Real part >0

LemmaReal part bound#

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

Lean

Formalized as real_part_lower_bound2.

Sources

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

Leanreal_part_lower_bound2

Uses 2

Proof usesReal part 2M · Real part lower bound

LemmaReal part >0#

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

Lean

Formalized as real_part_lower_bound3.

Sources

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

Leanreal_part_lower_bound3

Uses 2 · Used by 1

Proof usesReal part 2M · Real part lower bound

Used by2M minus nonzero

LemmaPos real nonzero#

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

Lean

Formalized as nonzero_if_real_part_positive.

Sources

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

Leannonzero_if_real_part_positive

Used by 1

Used by2M minus nonzero

Lemma2M minus nonzero#

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

Lean

Formalized as lem_real_part_lower_bound4.

Sources

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

Leanlem_real_part_lower_bound4

Uses 2 · Used by 2

Proof usesReal part >0 · Pos real nonzero

Used by2M minus mod · Denom nonzero

LemmaAbsolute value positive#

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

Lean

Formalized as lem_abspos.

Sources

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

Leanlem_abspos

Used by 2

Used by2M minus mod · Mod positive

Lemma2M minus mod#

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

Lean

Formalized as lem_real_part_lower_bound5.

Sources

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

Leanlem_real_part_lower_bound5

Uses 2 · Used by 2

Proof uses2M minus nonzero · Absolute value positive

Used byRatio bound · Ratio bound

LemmaReal imaginary#

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

Lean

Formalized as lem_wReIm.

Sources

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

Leanlem_wReIm

Used by 1

Used byModulus identity

LemmaMod square#

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

Lean

Formalized as lem_modaib.

Sources

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

Leanlem_modaib

Used by 1

Used byMod diff

LemmaShifted mod#

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

Lean

Formalized as lem_modcaib.

Sources

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

Leanlem_modcaib

Used by 1

Used byMod diff

LemmaMod diff#

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

Lean

Formalized as lem_diffmods.

Sources

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

Leanlem_diffmods

Uses 2 · Used by 1

Proof usesShifted mod · Mod square

Used byMod diff

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.