theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9_prime_copN_beta_bounds (N n : ℕ) : (0 ≤ if n.Coprime N then AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta n else 0) ∧ (if n.Coprime N then AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta n else 0) ≤ ↑((AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau 1) n)

The literal short prime/coprimality coefficient obeys the one-fold divisor bound.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Long_prime_product_fibre_le (N : ℕ) (ρ : ℝ) (k : ℕ × ℕ × ℕ) (U V : Finset ℕ) (v : ℕ) : (∑ p ∈ U ×ˢ V, if p.1 * p.2 = v then fouvryG9LongAlpha N ρ k p.1 * if p.2.Coprime N then AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta p.2 else 0 else 0) ≤ ↑((AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau 3) v)

The actual long multiplicity and literal prime/copN short coefficient, with an arbitrary finite rectangle and no additional geometric assumptions.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Long_prime_natAbs_fibre_le (N : ℕ) (ρ : ℝ) (k : ℕ × ℕ × ℕ) (U V : Finset ℕ) (r : ℕ) : (∑ p ∈ U ×ˢ V, if (↑N - ↑p.1 * ↑p.2).natAbs = r then fouvryG9LongAlpha N ρ k p.1 * if p.2.Coprime N then AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta p.2 else 0 else 0) ≤ ↑((AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau 3) (N + r)) + ↑((AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau 3) (N - r))

The genuine absolute-difference bound for the same source coefficients.