theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_product_active_bounds {N m r : ℕ} {ε : ℝ} (hN : 2 ≤ N) (hm : m ∈ goldbachG11ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) (hr : r ∈ goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m) : ε * ↑N ^ (29 / 33) < ↑m ∧ ↑m < ↑N ^ (49 / 53)

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

A purely geometric envelope; no output-prime condition is inserted into coefficients.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EffectiveProductSupport N ε = {m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) | ε * ↑N ^ (29 / 33) < ↑m ∧ ↑m < ↑N ^ (49 / 53)}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductFirstPrimeFiber_eq_empty_of_inactive {N m : ℕ} {ε : ℝ} (hN : 2 ≤ N) (hm : m ∈ goldbachG11ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) (hi : ¬(ε * ↑N ^ (29 / 33) < ↑m ∧ ↑m < ↑N ^ (49 / 53))) : goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m = ∅

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodSwitchedTotal_eq_effective_product_sum {N : ℕ} (ε : ℝ) (hN : 2 ≤ N) : goldbachG11GoodSwitchedTotal N ε (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) = ∑ m ∈ goldbachG11EffectiveProductSupport N ε, ↑(goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m) * ↑(goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m).card

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EffectiveProductCoefficient (N : ℕ) (ε : ℝ) (m : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EffectiveProductCoefficient N ε m = if m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EffectiveProductSupport N ε then MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11NormalizedProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m else 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EffectiveProductCoefficient_bounds (N m : ℕ) (ε : ℝ) : 0 ≤ goldbachG11EffectiveProductCoefficient N ε m ∧ goldbachG11EffectiveProductCoefficient N ε m ≤ 1

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EffectiveProductCoefficient_support {N m : ℕ} {ε : ℝ} (ha : goldbachG11EffectiveProductCoefficient N ε m ≠ 0) : m ∈ goldbachG11ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) ∧ ε * ↑N ^ (29 / 33) < ↑m ∧ ↑m < ↑N ^ (49 / 53)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodSwitchedTotal_eq_effective_normalized_sum {N : ℕ} (ε : ℝ) (hN : 2 ≤ N) : ↑(goldbachG11GoodSwitchedTotal N ε (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) = 400 * ∑ m ∈ goldbachG11EffectiveProductSupport N ε, goldbachG11EffectiveProductCoefficient N ε m * ↑(goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m).card