theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9FamilyCost_envelope {ι : Type u} [DecidableEq ι] (s : Finset ι) (f : ι → ℝ) {B H : ℝ} (hB : 0 < B) (hH : 0 ≤ H) (hcard : ↑s.card ≤ B) (hf : ∀ t ∈ s, |f t| ≤ H) : |(∑ t ∈ s, |f t|) / B| ≤ H

Normalize a finite family by a positive real cardinality budget. The tag set may be empty, and the budget need not be integral.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9FamilyCost_absorb (A : ℕ) {B n : ℝ} (hn : 0 ≤ n) (hl : 0 < Real.log n) (hB : B ≤ Real.log n) : B * (n / Real.log n ^ (A + 1)) ≤ n / Real.log n ^ A

A single spare logarithm absorbs any fixed positive real family budget.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectangleError_family_total {ι : Type u} [DecidableEq ι] (j A : ℕ) {B e ε δ ρ : ℝ} (hB : 0 < B) (he : 0 < e) (he1 : e ≤ 1) (hε : 0 < ε) (hεa : ε < 4 / 53) (hεδ : ε < δ) (hδ : δ ≤ 1 / 2) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → ∀ (S : ℕ × ℕ × ℕ → Finset ι) (c : ℕ × ℕ × ℕ → ι → ℕ → ℝ), (∀ k ∈ fouvryG9GridUsed N e ρ, ↑(S k).card ≤ B) → (∀ k ∈ fouvryG9GridUsed N e ρ, ∀ t ∈ S k, AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.SignedWellFactorable j (↑N ^ (5 / 9 - δ) / (2 / 3 * ρ ^ k.1) ^ (5 / 9)) (c k t)) → ∑ k ∈ fouvryG9GridUsed N e ρ, ∑ t ∈ S k, |fouvryG9RectangleError N ρ δ k (c k t)| ≤ ↑N / Real.log ↑N ^ A

Actual G9 rectangle errors for arbitrary finite tagged families. The common threshold precedes N, every tag set, and every coefficient family. Only individual original-level signed well-factorability is assumed; no well-factorability of an aggregate and no error estimate is a hypothesis.