noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryGridError (N : ℕ) (ε ρ δ : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryGridError N ε ρ δ = ∑ k ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridUsed N ε ρ, ∑ d ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedModuli N ⌊MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryLevel N δ⌋₊, |MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryRectangleResidual N ε ρ k d N|

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryGrid_error_total (A : ℕ) (F : ℝ) (hF : 0 ≤ F) {δ ρ : ℝ} (hδ : 0 < δ) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (ε : ℝ), F * goldbachG11OrdinaryGridError N ε ρ δ ≤ ↑N / Real.log ↑N ^ A

All actual ordinary-grid errors are paid at the original half-minus-delta level. Any fixed external-family cardinality is also paid; epsilon is after N0.