@[instance_reducible]

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

Equations

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

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

Closed prime carrier z ≤ p ≤ y, keeping the actual conditions p.Prime and p ∤ N.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachClosedPrimes N z y = {p ∈ MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftingPrimes N (y + 1) | z ≤ ↑p ∧ ↑p ≤ y}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachHalfOpenPrimes_iff {N p : ℕ} {z y : ℝ} : p ∈ goldbachHalfOpenPrimes N z y ↔ Nat.Prime p ∧ ¬p ∣ N ∧ z ≤ ↑p ∧ ↑p < y

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachClosedPrimes_iff {N p : ℕ} {z y : ℝ} : p ∈ goldbachClosedPrimes N z y ↔ Nat.Prime p ∧ ¬p ∣ N ∧ z ≤ ↑p ∧ ↑p ≤ y

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH_nonneg (A : Finset ℕ) (M d : ℕ) (x : ℝ) : 0 ≤ literalH A M d x

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

Actual weakly ordered half-open triple sum S6h, with t < y but r = s, s = t, and r = s = t all retained.

Equations

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

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

Actual repeat mass R, counting exactly the weakly ordered half-open triples with r = s or s = t.

Equations

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

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

Actual weakly ordered closed triple sum S6closed, with t ≤ y.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS6Closed A N z y = ∑ t ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachClosedPrimes N z y, ∑ r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachClosedPrimes N z ↑t, ∑ s ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachClosedPrimes N ↑r ↑t, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH A (N * r) (r * s * t) ↑s

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

Actual endpoint mass B6, i.e. the part of S6closed with t = y when such a prime exists, and zero otherwise.

Equations

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachR_nonneg (A : Finset ℕ) (N : ℕ) (z y : ℝ) : 0 ≤ goldbachR A N z y

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB6_nonneg (A : Finset ℕ) (N : ℕ) (z y : ℝ) : 0 ≤ goldbachB6 A N z y

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS6HalfOpen_eq_goldbachWStrict_add_goldbachR (A : Finset ℕ) (N : ℕ) (z y : ℝ) : goldbachS6HalfOpen A N z y = goldbachWStrict A N z y + goldbachR A N z y

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS6Closed_eq_goldbachS6HalfOpen_add_goldbachB6 (A : Finset ℕ) (N : ℕ) (z y : ℝ) : goldbachS6Closed A N z y = goldbachS6HalfOpen A N z y + goldbachB6 A N z y

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWStrict_eq_goldbachS6Closed_sub_goldbachR_sub_goldbachB6 (A : Finset ℕ) (N : ℕ) (z y : ℝ) : goldbachWStrict A N z y = goldbachS6Closed A N z y - goldbachR A N z y - goldbachB6 A N z y

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

Closed S3, keeping the literal endpoint p = y when it exists.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3Closed A N z y = ∑ s ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachClosedPrimes N z y, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH A N s z

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

Closed S5, keeping the literal endpoint r = y in the first prime.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5Closed 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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3HalfOpen_le_goldbachS3Closed (A : Finset ℕ) (N : ℕ) (z y : ℝ) : goldbachS3HalfOpen A N z y ≤ goldbachS3Closed A N z y

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5HalfOpen_le_goldbachS5Closed (A : Finset ℕ) (N : ℕ) (z y : ℝ) : goldbachS5HalfOpen A N z y ≤ goldbachS5Closed A N z y