noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LowGridFamilyError (N : ℕ) (ε δ θ ρ : ℝ) (P : ℕ × ℕ → Finset ℕ) (z : ℕ × ℕ → ℝ) : ℝ

The full same-member signed errors over actual low cells and actual external tags.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LowGridFamilyError N ε δ θ ρ P z = ∑ k ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LowGridUsed N ε ρ, ∑ t ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags true (P k) (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridLowLevel N δ ρ k) θ) θ (z k), |MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridLong N ε ρ k) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridShort N ρ k) (Finset.Ioc 0 ⌊MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridLowLevel N δ ρ k⌋₊) (fun (m : ℕ) => ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m)) (fun (p : ℕ) => if p.Coprime N then MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta p else 0) (fun (d : ℕ) => (MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm true (P k) (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridLowLevel N δ ρ k) θ) θ (z k) t) d) ↑N|

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LowGrid_externalFamily_error_total (A : ℕ) {ε δ θ ρ : ℝ} (hε : 0 < ε) (hεu : ε ≤ 1) (hδ : 0 < δ) (hδu : δ < 1 / 2) (hθ : 0 < θ) (hθu : θ < 1 / 8) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → ∀ (P : ℕ × ℕ → Finset ℕ) (z : ℕ × ℕ → ℝ), goldbachG11LowGridFamilyError N ε δ θ ρ P z ≤ ↑N / Real.log ↑N ^ A

Fully paid low-grid distribution error. The threshold precedes all changing sieve carriers, cutoffs, cells and members. No SW, WF, cardinality, mass or per-cell-error hypothesis remains; fixed rho and epsilon dependence is retained.