Positive real to Real inverse

LemmaPositive real#

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

Lean

Formalized as lem_Re1deltatneq0.

Sources

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

Leanlem_Re1deltatneq0

Uses 1 · Used by 1

Proof usesReal delta

Used byInverse real

LemmaInverse real#

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

Lean

Formalized as lem_Re1deltatge0.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT4_ZeroFreeRegion.tex, line 209

Leanlem_Re1deltatge0

Uses 2 · Used by 2

Proof usesPositive real · Reciprocal real

Used byScaled real · Split bound

LemmaScaled real#

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

Lean

Formalized as lem_Re1deltatge0m.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT4_ZeroFreeRegion.tex, line 220

Leanlem_Re1deltatge0m

Uses 2 · Used by 1

Proof usesInverse real · Order is integer

Used byDouble real

LemmaDouble real#

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

Lean

Formalized as lem_Re1delta2tge0.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT4_ZeroFreeRegion.tex, line 230

Leanlem_Re1delta2tge0

Uses 1 · Used by 1

Proof usesScaled real

Used bySum nonneg

LemmaSum nonneg#

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

Lean

Formalized as lem_sumrho2ge.

Sources

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

Leanlem_sumrho2ge

Uses 1 · Used by 1

Proof usesDouble real

Used byReal nonneg

LemmaReal nonneg#

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

Lean

Formalized as lem_sumrho2ge02.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT4_ZeroFreeRegion.tex, line 252

Leanlem_sumrho2ge02

Uses 2 · Used by 1

Proof usesSum split · Sum nonneg

Used byDouble bound

LemmaDouble bound#

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

Lean

Formalized as lem_explicit2Real2.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT4_ZeroFreeRegion.tex, line 263

Leanlem_explicit2Real2

Uses 2 · Used by 1

Proof usesDouble real · Real nonneg

Used byShift bound

LemmaLog compare#

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

Lean

Formalized as lem_log2Olog.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT4_ZeroFreeRegion.tex, line 272

Leanlem_log2Olog

Uses 2 · Used by 1

Proof usesLog growth · Log compare

Used byLog compare

LemmaTrivial bound#

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

Lean

Formalized as lem_w2t.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT4_ZeroFreeRegion.tex, line 281

Leanlem_w2t

Used by 1

Used byLog compare

LemmaLog compare#

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

Lean

Formalized as lem_log2Olog2.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT4_ZeroFreeRegion.tex, line 288

Leanlem_log2Olog2

Uses 2 · Used by 1

Proof usesTrivial bound · Log compare

Used byShift bound

LemmaShift bound#

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

Lean

Formalized as lem_Z2bound.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT4_ZeroFreeRegion.tex, line 296

Leanlem_Z2bound

Uses 2 · Used by 1

Proof usesDouble bound · Log compare

Used byCombined bound

LemmaSplit sum#

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

Lean

Formalized as lem_Z1split.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT4_ZeroFreeRegion.tex, line 306

Leanlem_Z1split

Uses 1 · Used by 1

Proof usesIn set

Used bySplit bound

LemmaSplit bound#

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

Lean

Formalized as lem_Z1splitge.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT4_ZeroFreeRegion.tex, line 318

Leanlem_Z1splitge

Uses 2 · Used by 1

Proof usesSplit sum · Inverse real

Used bySum bound

LemmaDifference real#

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

Lean

Formalized as lem_1deltatrho0.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT4_ZeroFreeRegion.tex, line 331

Leanlem_1deltatrho0

Used by 1

Used byReal inverse

LemmaReal inverse#

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

Lean

Formalized as lem_1delsigReal.

Sources

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

Leanlem_1delsigReal

Uses 1 · Used by 1

Proof usesDifference real

Used byReal inverse

LemmaInverse real#

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

Lean

Formalized as lem_11delsiginR.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT4_ZeroFreeRegion.tex, line 354

Leanlem_11delsiginR

Used by 1

Used byInverse real

LemmaInverse real#

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

Lean

Formalized as lem_11delsiginR2.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT4_ZeroFreeRegion.tex, line 362

Leanlem_11delsiginR2

Uses 2 · Used by 1

Proof usesZero bound · Inverse real

Used byReal inverse

LemmaReal part#

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

Lean

Formalized as lem_ReReal.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT4_ZeroFreeRegion.tex, line 371

Leanlem_ReReal

Used by 1

Used byReal inverse

LemmaReal inverse#

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

Lean

Formalized as lem_1delsigReal2.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT4_ZeroFreeRegion.tex, line 378

Leanlem_1delsigReal2

Uses 2 · Used by 1

Proof usesInverse real · Real part

Used byReal inverse

LemmaReal inverse#

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

Lean

Formalized as lem_re_inv_one_plus_delta_minus_rho_real.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT4_ZeroFreeRegion.tex, line 389

Leanlem_re_inv_one_plus_delta_minus_rho_real

Uses 2 · Used by 1

Proof usesReal inverse · Real inverse

Used bySum bound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.