noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RSquareException (A : Finset ℕ) (v : GoldbachG11Label) : Finset ℕ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RSquareException A v = {n ∈ A | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelProd v ∣ n ∧ v.snd.snd.fst < v.snd.snd.snd ∧ v.snd.snd.fst ^ 2 ∣ n}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11NException (A : Finset ℕ) (N : ℕ) (v : GoldbachG11Label) : Finset ℕ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11NException A N v = {n ∈ A | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelProd v ∣ n ∧ ¬n.Coprime N}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RSquareCount (A : Finset ℕ) (v : GoldbachG11Label) : ℤ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RSquareCount A v = ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RSquareException A v).card

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11NCount (A : Finset ℕ) (N : ℕ) (v : GoldbachG11Label) : ℤ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11NCount A N v = ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11NException A N v).card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_rough_mul_survives {N r q s t m : ℕ} (hq : Nat.Prime q) (hs : Nat.Prime s) (ht : Nat.Prime t) (hqs : q ≤ s) (hst : s ≤ t) (hm : SurvivesSieve 1 (↑q) m) : SurvivesSieve (N * r) (↑q) (r * q * s * t * m)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_survives_or_exceptions {N r q s t n : ℕ} (hr : Nat.Prime r) (hd : r * q * s * t ∣ n) (hH : SurvivesSieve (N * r) (↑q) n) : SurvivesSieve 1 (↑q) (n / (r * q * s * t)) ∨ r < q ∧ r ^ 2 ∣ n ∨ ¬n.Coprime N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_cell_sandwich (N : ℕ) (ε : ℝ) (v : GoldbachG11Label) {z b : ℝ} (hε : 0 ≤ ε) (hv : v ∈ goldbachG11Labels N z b) : goldbachG11RoughCount N ε v ≤ literalH (goldbachDifferenceCarrier N ε) (N * v.snd.snd.fst) (goldbachG11LabelProd v) ↑v.snd.snd.snd ∧ literalH (goldbachDifferenceCarrier N ε) (N * v.snd.snd.fst) (goldbachG11LabelProd v) ↑v.snd.snd.snd ≤ goldbachG11RoughCount N ε v + goldbachG11RSquareCount (goldbachDifferenceCarrier N ε) v + goldbachG11NCount (goldbachDifferenceCarrier N ε) N v

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11_roughQuotient_sandwich (N : ℕ) (ε z b : ℝ) (hε : 0 ≤ ε) : ∑ v ∈ goldbachG11Labels N z b, goldbachG11RoughCount N ε v ≤ goldbachWeightG11 (goldbachDifferenceCarrier N ε) N z b ∧ goldbachWeightG11 (goldbachDifferenceCarrier N ε) N z b ≤ ∑ v ∈ goldbachG11Labels N z b, goldbachG11RoughCount N ε v + ∑ v ∈ goldbachG11Labels N z b, goldbachG11RSquareCount (goldbachDifferenceCarrier N ε) v + ∑ v ∈ goldbachG11Labels N z b, goldbachG11NCount (goldbachDifferenceCarrier N ε) N v