theorem G12SafeGridBudget.sum_cell_bounds {ι : Type u_1} (s : Finset ι) (output main : ι → ℝ) (fee : ℝ) (h : ∀ i ∈ s, output i ≤ main i + fee) : ∑ i ∈ s, output i ≤ ∑ i ∈ s, main i + ↑s.card * fee

A finite sum keeps the original main term and pays the fee once per cell.

theorem G12SafeGridBudget.outside_numerical (B : ℕ) {η : ℝ} (hη : 0 < η) (hηu : η < 1 / 8) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (Q : ℝ), ↑N ^ (1 / 3) ≤ Q → Q ≤ ↑N → 20 * ↑N * (4 / MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η ^ η ^ 2) * (1 + Real.log ↑⌊Q⌋₊) ^ 2 ≤ ↑N / Real.log ↑N ^ B

Numerical outside budget, not a bound on the signed error beneath it.

theorem G12SafeGridBudget.correction_numerical (B : ℕ) {η : ℝ} (hη : 0 < η) (hηu : η < 1 / 8) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (Q : ℝ), ↑N ^ (1 / 3) ≤ Q → Q ≤ ↑N → G12FlexibleWF.correctionBudget N Q η ≤ 2 * (↑N / Real.log ↑N ^ B)

Both displayed correction-budget summands are paid uniformly in the moving Q.