theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_expanded_rough_uniform (η : ℝ) (hη : 0 < η) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (q y : ℝ), ↑N ^ (4 / 53) ≤ q → q ≤ ↑N ^ (4 / 33) → ↑N ^ (1 / 2) ≤ y → y ≤ ↑N ^ 2 → 1 < y ∧ 1 < q ∧ Real.log y / Real.log q ∈ Set.Icc 4 100 ∧ |↑(LiLiuPrereqBuchstab.roughCount y q) - goldbachG11BuchstabMass y q| ≤ η * y / Real.log q

One frozen uniform Buchstab source, with a moving output size. All q and all y in the expanded coarse window share one threshold. No numerical bound on omega is hypothesized.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_expanded_rough_coarse (η : ℝ) (hη : 0 < η) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (q y : ℝ), ↑N ^ (4 / 53) ≤ q → q ≤ ↑N ^ (4 / 33) → ↑N ^ (1 / 2) ≤ y → y ≤ ↑N ^ 2 → ↑(LiLiuPrereqBuchstab.roughCount y q) ≤ (1 + η) * y / Real.log q

The coarse collar uses the already proved omega<=1, not the sharper ordered-domain constant outside its domain.