theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectangleWeight_of_firstPrimeFiber {N m p : ℕ} {ε : ℝ} (hp : p ∈ goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m) : goldbachG11RectangleWeight N (m, p) = ↑(goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeProductAtoms (N : ℕ) (ε : ℝ) : Finset (ℕ × ℕ)

Actual first-prime/product pairs; the coefficient continues to carry the body fibres.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeProductAtoms N ε = {v ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) ×ˢ Finset.range N | v.2 ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) v.1}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodSwitchedTotal_eq_weighted_atoms (N : ℕ) (ε : ℝ) : ↑(goldbachG11GoodSwitchedTotal N ε (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) = ∑ v ∈ goldbachG11PrimeProductAtoms N ε, goldbachG11RectangleWeight N v

Literal equality with the accepted good switched count, including all multiplicities.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_finite_positive_cover {ι : Type u_1} {κ : Type u_2} (S : Finset ι) (K : Finset κ) (R : κ → Finset ι) (f : ι → ℝ) (hf : ∀ (v : ι), 0 ≤ f v) (hc : ∀ v ∈ S, ∃ k ∈ K, v ∈ R k) : ∑ v ∈ S, f v ≤ ∑ k ∈ K, ∑ v ∈ R k, f v

A positive cover may overlap; no output or body-product injectivity is asserted.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodSwitchedTotal_le_rectanglePrimeMass_cover {κ : Type u_1} (N : ℕ) (ε : ℝ) (K : Finset κ) (U V : κ → Finset ℕ) (hc : ∀ m ∈ goldbachG11ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), ∀ p ∈ goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m, ∃ k ∈ K, m ∈ U k ∧ p ∈ V k) : ↑(goldbachG11GoodSwitchedTotal N ε (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ ∑ k ∈ K, goldbachG11RectanglePrimeMass N (U k) (V k)

The true G11 good count is bounded by the positive rectangular prime masses once the actual finite prime/product atoms are covered. No geometric cover is assumed proved.