noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectangleError (N : ℕ) (ρ δ : ℝ) (k : ℕ × ℕ × ℕ) (c : ℕ → ℝ) : ℝ

The separated G9 rectangle error with the unchanged global weight and level. The interval endpoints are data, independent of any nonemptiness witness.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectangleError N ρ δ k c = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongProducts N ρ k) (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWInterval (↑⌈max (ρ ^ k.1) (↑N ^ (4 / 53))⌉ - 1) (↑⌈min (ρ ^ (k.1 + 1)) (↑N ^ (1 / 10))⌉ - 1)) (Finset.Ioc 0 ⌊↑N ^ (5 / 9 - δ) / (2 / 3 * ρ ^ k.1) ^ (5 / 9)⌋₊) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongAlpha N ρ k) (fun (n : ℕ) => if n.Coprime N then MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta n else 0) c ↑N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectangleError_uniform (j A : ℕ) {e ε δ : ℝ} (he : 0 < e) (he1 : e ≤ 1) (hε : 0 < ε) (hεa : ε < 4 / 53) (hεδ : ε < δ) (hδ : δ ≤ 1 / 2) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → ∀ (ρ : ℝ), 1 < ρ → ρ ≤ 5 / 4 → ∀ (k : ℕ × ℕ × ℕ), (fouvryG9GridCell N e ρ k).Nonempty → ∀ (c : ℕ → ℝ), AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.SignedWellFactorable j (↑N ^ (5 / 9 - δ) / (2 / 3 * ρ ^ k.1) ^ (5 / 9)) c → have x := 4 * ρ ^ (k.2.1 + k.2.2) * (2 / 3 * ρ ^ k.1); |fouvryG9RectangleError N ρ δ k c| ≤ x / Real.log x ^ A

Expanded C2 now pays the actual separated G9 rectangle. The threshold precedes the mesh ratio, occupied cell, and original global weight.