noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12GoodCrossBodies (N : ℕ) (z b c : ℝ) : Finset GoldbachG11SwitchedBody

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12GoodCrossBodies N z b c = {u ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12CrossSwitchedBodies N z b c | (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodyProd u).Coprime N}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12GoodCrossTotal (N : ℕ) (ε z b c : ℝ) : ℤ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12GoodCrossTotal N ε z b c = ∑ u ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12GoodCrossBodies N z b c, ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11FirstPrimeFiber N ε z u).card

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12BadCrossTotal (N : ℕ) (ε z b c : ℝ) : ℤ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12BadCrossTotal N ε z b c = ∑ u ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12CrossSwitchedBodies N z b c with ¬(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodyProd u).Coprime N, ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11FirstPrimeFiber N ε z u).card

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductSupport (N : ℕ) (z b c : ℝ) : Finset ℕ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductSupport N z b c = Finset.image MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodyProd (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12GoodCrossBodies N z b c)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductCoefficient (N : ℕ) (z b c : ℝ) (m : ℕ) : ℕ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductCoefficient N z b c m = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11FilteredProductCoefficient N z c (fun (u : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11SwitchedBody) => ↑u.snd.fst ≤ b ∧ b ≤ ↑u.fst) m

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12GoodCrossBodies_eq_filter (N : ℕ) (z b c : ℝ) : goldbachG12GoodCrossBodies N z b c = {u ∈ goldbachG11GoodSwitchedBodies N z c | ↑u.snd.fst ≤ b ∧ b ≤ ↑u.fst}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12GoodCrossBodies_subset (N : ℕ) (z b c : ℝ) : goldbachG12GoodCrossBodies N z b c ⊆ goldbachG11GoodSwitchedBodies N z c

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductCoefficient_eq_card (N : ℕ) (z b c : ℝ) (m : ℕ) : goldbachG12ProductCoefficient N z b c m = {u ∈ goldbachG12GoodCrossBodies N z b c | goldbachG11SwitchedBodyProd u = m}.card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductCoefficient_le_four_hundred (N m : ℕ) (b c : ℝ) : goldbachG12ProductCoefficient N (↑N ^ (4 / 53)) b c m ≤ 400

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductSupport_data {N m : ℕ} {z b c : ℝ} (hm : m ∈ goldbachG12ProductSupport N z b c) : 0 < m ∧ m < N ∧ m.Coprime N ∧ z ≤ ↑m.minFac

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12RoughSum_eq_good_add_bad (N : ℕ) (ε z b c : ℝ) : ∑ v ∈ goldbachG12Labels N z b c, goldbachG11RoughCount N ε v = goldbachG12GoodCrossTotal N ε z b c + goldbachG12BadCrossTotal N ε z b c

The cross is split before any bound; no main-family enlargement occurs.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12BadCrossTotal_le_NCount_sum (N : ℕ) (ε z b c : ℝ) (hε : 0 ≤ ε) : goldbachG12BadCrossTotal N ε z b c ≤ ∑ v ∈ goldbachG11Labels N z c, goldbachG11NCount (goldbachDifferenceCarrier N ε) N v

Only the exceptional bad part is bounded by the broad exception family.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12GoodCross_sum_product (N : ℕ) (z b c : ℝ) (f : ℕ → ℤ) : ∑ u ∈ goldbachG12GoodCrossBodies N z b c, f (goldbachG11SwitchedBodyProd u) = ∑ m ∈ goldbachG12ProductSupport N z b c, ↑(goldbachG12ProductCoefficient N z b c m) * f m

Product grouping counts every body in its fibre; product injectivity is not assumed.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12GoodCrossTotal_eq_product_sum (N : ℕ) (ε z b c : ℝ) : goldbachG12GoodCrossTotal N ε z b c = ∑ m ∈ goldbachG12ProductSupport N z b c, ↑(goldbachG12ProductCoefficient N z b c m) * ↑(goldbachG11ProductFirstPrimeFiber N ε z m).card