theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_buchstabParameter_bounds {u v w x : ℝ} (hu : u ∈ Set.Icc (4 / 53) (4 / 33)) (hv : v ∈ Set.Icc (4 / 53) (4 / 33)) (hw : w ∈ Set.Icc (4 / 53) (4 / 33)) (hx : x ∈ Set.Icc (4 / 53) (4 / 33)) : (1 - u - v - w - x) / v ∈ Set.Icc (17 / 4) (37 / 4)

A domain estimate for the literal Buchstab argument; no estimate for the Buchstab function.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_logPrimeExponent_mem {N p : ℕ} (hN : 2 ≤ N) (hp : Nat.Prime p) (hlo : ↑N ^ (4 / 53) ≤ ↑p) (hhi : ↑p ≤ ↑N ^ (4 / 33)) : Real.log ↑p / Real.log ↑N ∈ Set.Icc (4 / 53) (4 / 33)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_canonical_logQuotient_bounds {N r q s t : ℕ} (hN : 2 ≤ N) (ht : t ∈ goldbachClosedPrimes N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) (hs : s ∈ goldbachClosedPrimes N (↑N ^ (4 / 53)) ↑t) (hr : r ∈ goldbachClosedPrimes N (↑N ^ (4 / 53)) ↑s) (hq : q ∈ goldbachClosedPrimes N ↑r ↑s) : Real.log (↑N / ↑(r * q * s * t)) / Real.log ↑q ∈ Set.Icc (17 / 4) (37 / 4)

Actual closed G11 labels give the same compact Buchstab window, including repeated primes.