@[instance_reducible]

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

Equations

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Pairs_low_eq {N : ℕ} {z y : ℝ} (hy : 2 ≤ y) (hyN : y ^ 3 ≤ ↑N) : {rs ∈ goldbachS4Pairs N z | ↑rs.2 < y} = {rs ∈ goldbachHalfOpenPrimes N z y ×ˢ goldbachHalfOpenPrimes N z y | rs.1 ≤ rs.2}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4_low_sum_eq_V (A : Finset ℕ) (N : ℕ) {z y : ℝ} (hy : 2 ≤ y) (hyN : y ^ 3 ≤ ↑N) : ∑ rs ∈ goldbachS4Pairs N z with ↑rs.2 < y, literalH A (N * rs.1) (rs.1 * rs.2) ↑rs.2 = goldbachV A N z y

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4_split_exact (A : Finset ℕ) (N : ℕ) {z y : ℝ} (hzy : z ≤ y) (hy : 2 ≤ y) (hyN : y ^ 3 ≤ ↑N) : goldbachS4 A N z = goldbachV A N z y + goldbachS5HalfOpen A N z y + goldbachS4 A N y

Exact three-region split, retaining the s=y boundary in the middle part. The cubic condition makes the old root restriction automatic in the low block.