Prime decay to Prime power

LemmaPrime decay#

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

Lean

Formalized as p_s_abs_1.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 9

Leanp_s_abs_1

Uses 1 · Used by 3

Proof usesPrime power

Used byNonzero factor · Ratio identity · Nonzero term

LemmaEuler product#

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

Lean

Formalized as zetaEulerprod.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 23

LeanzetaEulerprod

Used by 5

Used byAbs primes · Abs zeta · Ratio split · Zeta ratio · Zeta compare

LemmaAbs product#

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

Lean

Formalized as abs_of_tprod.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 34

Leanabs_of_tprod

Used by 1

Used byAbs primes

LemmaAbs primes#

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

Lean

Formalized as abs_P_prod.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 43

Leanabs_P_prod

Uses 2 · Used by 1

Proof usesEuler product · Abs product

Used byAbs zeta

LemmaAbs zeta#

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

Lean

Formalized as abs_zeta_prod.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 55

Leanabs_zeta_prod

Uses 2 · Used by 1

Proof usesEuler product · Abs primes

Used byAbs product

LemmaAbs inverse#

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

Lean

Formalized as abs_of_inv.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 66

Leanabs_of_inv

Used by 1

Used byAbs product

LemmaNonzero factor#

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

Lean

Formalized as one_minus_p_s_neq_0.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 76

Leanone_minus_p_s_neq_0

Uses 1 · Used by 1

Proof usesPrime decay

Used byAbs product

LemmaAbs product#

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

Lean

Formalized as abs_zeta_prod_prime.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 87

Leanabs_zeta_prod_prime

Uses 3 · Used by 1

Proof usesAbs zeta · Abs inverse · Nonzero factor

Used byZeta lower

LemmaReal double#

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

Lean

Formalized as Re2s.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 98

LeanRe2s

Used by 1

Used byReal bound

LemmaReal bound#

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

Lean

Formalized as Re2sge1.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 106

LeanRe2sge1

Uses 1 · Used by 2

Proof usesReal double

Used byRatio split · Zeta ratio

LemmaZeta ratio#

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

Lean

Formalized as zeta_ratio_prod.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 116

Leanzeta_ratio_prod

Uses 2 · Used by 1

Proof usesEuler product · Real bound

Used byRatio form

LemmaRatio product#

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

Lean

Formalized as prod_of_ratios.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 127

Leanprod_of_ratios

Used by 1

Used byRatio split

LemmaRatio split#

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

Lean

Formalized as simplify_prod_ratio.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 186

Leansimplify_prod_ratio

Uses 3 · Used by 1

Proof usesRatio product · Euler product · Real bound

Used byRatio form

LemmaRatio form#

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

Lean

Formalized as zeta_ratios.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 196

Leanzeta_ratios

Uses 2 · Used by 1

Proof usesRatio split · Zeta ratio

Used byRatio identity

LemmaDiff squares#

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

Lean

Formalized as diff_of_squares.

Sources

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

Leandiff_of_squares

Used by 1

Used byInverse ratio

LemmaInverse ratio#

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

Lean

Formalized as ratio_invs.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 216

Leanratio_invs

Uses 1 · Used by 1

Proof usesDiff squares

Used byRatio identity

TheoremRatio identity#

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

Lean

Formalized as zeta_ratio_identity.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 227

Leanzeta_ratio_identity

Uses 3 · Used by 1

Proof usesRatio form · Inverse ratio · Prime decay

Used byThree halves

LemmaThree halves#

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

Lean

Formalized as zeta_ratio_at_3_2.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 238

Leanzeta_ratio_at_3_2

Uses 1 · Used by 1

Proof usesRatio identity

Used byZeta lower

LemmaTriangle abs#

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

Lean

Formalized as triangle_inequality_specific.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 249

Leantriangle_inequality_specific

Used by 1

Used byTerm bound

LemmaPrime power#

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

Lean

Formalized as abs_p_pow_s.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 258

Leanabs_p_pow_s

Used by 2

Used byPrime decay · Term bound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.