theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectangleMass_le_kernel {e ρ δ ζ : ℝ} (he : 0 < e) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (hδ : δ < 1 / 4) (hζ : 0 < ζ) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → ∑ k ∈ fouvryG9GridUsed N e ρ, fouvryG9RectangleMass N ρ k / Real.log (↑N ^ (5 / 9 - δ) / (2 / 3 * ρ ^ k.1) ^ (5 / 9)) ≤ (1 + ζ) * ρ ^ 3 * ↑N / Real.log ↑N ^ 2 * fouvryG9RelaxedPairKernel N ρ δ

Complete actual occupied weighted-mass bound, with the original Qk and one prime prefix per pair. All finite and analytic weight inputs are supplied.