@[instance_reducible]

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidable_mathlibNt_2 (P : Prop) : Decidable P

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidable_mathlibNt_2 P = Classical.propDecidable P

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachV (A : Finset ℕ) (N : ℕ) (z y : ℝ) : ℤ

Weakly ordered double sum, with the diagonal retained.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachV A N z y = ∑ s ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachHalfOpenPrimes N z y, ∑ r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachHalfOpenPrimes N z y with r ≤ s, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH A (N * r) (r * s) ↑s

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachQ (A : Finset ℕ) (N : ℕ) (z y : ℝ) : ℤ

Actual diagonal square contribution, not an assumed error bound.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachQ A N z y = ∑ r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachHalfOpenPrimes N z y, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH A N (r ^ 2) ↑r

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWStrict (A : Finset ℕ) (N : ℕ) (z y : ℝ) : ℤ

Strict triples r<s<t. The sieve cutoff is the middle prime s.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWStrict A N z y = ∑ t ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachHalfOpenPrimes N z y, ∑ r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachHalfOpenPrimes N z ↑t, ∑ s ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachHalfOpenPrimes N ↑r ↑t with r < s, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH A (N * r) (r * s * t) ↑s

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5HalfOpen (A : Finset ℕ) (N : ℕ) (z y : ℝ) : ℤ

Middle part of S4: the smaller prime is strictly below y.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5HalfOpen A N z y = ∑ rs ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Pairs N z with ↑rs.1 < y ∧ y ≤ ↑rs.2, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH A (N * rs.1) (rs.1 * rs.2) ↑rs.2