theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RemainderMajorant_discrepancy (U V : Finset ℕ) (α β : ℕ → ℝ) (N : ℕ) (hN : 1 ≤ N) (J : ℝ) (hJ : 0 ≤ J) (hw : ∀ p ∈ U ×ˢ V, 0 ≤ α p.1 * β p.2) (ha : ∀ p ∈ U ×ˢ V, (↑N - ↑p.1 * ↑p.2).natAbs ≤ 4 * N) (hf : ∀ r ≤ 4 * N, (∑ p ∈ U ×ˢ V, if (↑N - ↑p.1 * ↑p.2).natAbs = r then α p.1 * β p.2 else 0) ≤ J) (d : ℕ) (hd : 0 < d) (hdN : d ≤ N) : |AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.bilinearDiscrepancy U V α β (↑N) d| ≤ 10 * J * ↑N / ↑d.totient

A finite-fiber estimate for the literal coprime-centered discrepancy. Neither label injectivity nor a total-mass assumption is required.