theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegral_continuous_corner_error {u v x y m : ℝ} (hu : 0 ≤ u) (hv : 0 ≤ v) (hux : u ≤ x) (hvy : v ≤ y) (hx : x ≤ 1 / 3) (hy : y ≤ 1 / 2) (hm : 0 ≤ m) (hdx : x - u ≤ m) (hdy : y - v ≤ m) : 1 / ((1 - x - y) * (1 - x)) ≤ 1 / ((1 - u - v) * (1 - u)) + 243 * m

Quantitative oscillation of the continuous weighted kernel on the ambient box. The bound is independent of N and therefore usable before selecting N₀.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegral_selected_cell_geometry {n : ℕ} {h u v : ℝ} (q : Fin n × Fin n) (hq : q ∈ fouvryG9RelaxedIntegralCells n h) (hu : u ∈ Set.Ioc (goldbachB9AlphaGridPoint n ↑q.1) (goldbachB9AlphaGridPoint n (↑q.1 + 1))) (hv : v ∈ Set.Ioc (goldbachB9BetaGridPoint n ↑q.2) (goldbachB9BetaGridPoint n (↑q.2 + 1))) : 4 / 53 - goldbachB9AlphaGridStep n < u ∧ u < 1 / 10 + goldbachB9AlphaGridStep n ∧ 1 / 3 - goldbachB9BetaGridStep n < v ∧ u + 2 * v < 1 + h + goldbachB9AlphaGridStep n + 2 * goldbachB9BetaGridStep n

All cells selected by the finite cover lie in explicit thin enlargements of the four source boundaries. This isolates the remaining measure estimate.