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

The actual cross support retains the upper bound on its least prime factor.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12_nonempty_productFiber_upper {N m : ℕ} {ε : ℝ} (hN : 2 ≤ N) (hf : (goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m).Nonempty) : ↑m < ↑N ^ (49 / 53)

Any nonempty physical first-prime fibre already lies in the balanced range.

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport (N : ℕ) : Finset ℕ

Independent of epsilon and of the output sieve modulus.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N = {m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)) | ↑m ≤ ↑N ^ (49 / 53)}

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N m = ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)) m) / 400

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient_bounds (N m : ℕ) : goldbachG12NormalizedCoefficient N m ∈ Set.Icc 0 1

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport_data {N m : ℕ} (hm : m ∈ goldbachG12ActiveProductSupport N) : 0 < m ∧ m < N ∧ m.Coprime N ∧ ↑N ^ (4 / 53) ≤ ↑m ∧ ↑m ≤ ↑N ^ (49 / 53) ∧ ↑N ^ (4 / 53) ≤ ↑m.minFac ∧ ↑m.minFac ≤ ↑N ^ (4 / 33)

Exact support facts for the existing balanced prime-centered distribution theorem.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductPrimeTotal_eq_active (N : ℕ) (ε : ℝ) (hN : 2 ≤ N) : ↑(goldbachG12ProductPrimeTotal N ε (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11))) = 400 * ∑ m ∈ goldbachG12ActiveProductSupport N, goldbachG12NormalizedCoefficient N m * ↑(goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m).card

Restricting to the balanced support deletes only empty first-prime fibres. The factor 400 restores the literal integer coefficient, including every representation.