theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSW_uniform_eventually (B : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (u v : ℝ), u ≤ v → ⌊u⌋₊ ∈ Finset.Icc 2 N → ⌊v⌋₊ ∈ Finset.Icc 2 N → ∀ (d h : ℕ), 0 < d → 0 < h → ∀ (b : ℕ), b.Coprime d → |betaCoprimeAPDiscrepancy (primeSWInterval u v) primeSWBeta d h b| ≤ C * ↑N * ↑((fouvryTau 2) h) / Real.log ↑N ^ B

A uniform natural-scale estimate for all moduli and all moving prime intervals. The constants and the scale threshold precede both endpoints and every arithmetic parameter.