theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9_positive_rectangle_cover (N : ℕ) (e : ℝ) {ρ : ℝ} (hρ : 1 < ρ) (F : ℕ → ℕ → ℝ) (hF : ∀ (n m : ℕ), 0 ≤ F n m) : ∑ a ∈ goldbachB9LowPositivePrefixAtoms N e, F a.fst.1 (a.fst.2 * a.snd) ≤ ∑ k ∈ fouvryG9GridUsed N e ρ, ∑ n ∈ fouvryG9LongShortLabels N ρ k, ∑ m ∈ fouvryG9LongProducts N ρ k, fouvryG9LongAlpha N ρ k m * F n m

A positive rectangular majorant for the entire actual labelled mother set. No subtraction of a principal term or signed-error inequality is asserted.