theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodSwitchedBodies_sum_product_real (N : ℕ) (z b : ℝ) (f : ℕ → ℝ) : ∑ u ∈ goldbachG11GoodSwitchedBodies N z b, f (goldbachG11SwitchedBodyProd u) = ∑ m ∈ goldbachG11ProductSupport N z b, ↑(goldbachG11ProductCoefficient N z b m) * f m

The finite product-fibre identity for genuinely real weights, not an invalid cast of the integer-valued grouping theorem.

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ExpandedPrimeWindow (N : ℕ) (ρ : ℝ) (m : ℕ) : Finset ℕ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ExpandedPrimeWindow N ρ m = {p ∈ Finset.range (2 * N + 1) | Nat.Prime p ∧ ↑N ^ (4 / 53) ≤ ↑p ∧ ↑p < ρ * ↑m.minFac ∧ ↑m * ↑p < ρ ^ 2 * ↑N}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ExpandedMotherMass (N : ℕ) (ρ : ℝ) (h : ℝ → ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ExpandedMotherMass N ρ h = ∑ u ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodSwitchedBodies N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), ∑ p ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ExpandedPrimeWindow N ρ (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodyProd u), h (Real.log ↑p / Real.log ↑N)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11WeightedGridMass_le_expandedMother {N : ℕ} {ε ρ : ℝ} (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (hbig : 4 ≤ ↑N ^ (4 / 53)) (h : ℝ → ℝ) (hh : ∀ (r : ℝ), 0 ≤ h r) : goldbachG11WeightedGridMass N ε ρ h ≤ goldbachG11ExpandedMotherMass N ρ h

Reconstruct every retained body label from the raw coefficient, without any injectivity assumption on the product map. The product and ordering extensions, and the absent p-coprimality filter, remain explicit in the window.