noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectanglePrimeSupport (N : ℕ) (ρ : ℝ) (k : ℕ × ℕ × ℕ) : Finset ℕ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectanglePrimeSupport N ρ k = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWInterval (↑⌈max (ρ ^ k.1) (↑N ^ (4 / 53))⌉ - 1) (↑⌈min (ρ ^ (k.1 + 1)) (↑N ^ (1 / 10))⌉ - 1)

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectangleBeta (N n : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectangleBeta N n = if n.Coprime N then MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta n else 0

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectangleSifted (N : ℕ) (ρ : ℝ) (k : ℕ × ℕ × ℕ) (P : Finset ℕ) : ℝ

Sift the actual separated rectangle, retaining the long-label weights.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectangleSifted N ρ k P = MathlibNt.SieveTheory.LiLiuPrereqWF.weightedSequenceSifted (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongProducts N ρ k ×ˢ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectanglePrimeSupport N ρ k) (fun (p : ℕ × ℕ) => (↑N - ↑p.1 * ↑p.2).natAbs) (fun (p : ℕ × ℕ) => MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongAlpha N ρ k p.1 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectangleBeta N p.2) P

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Rectangle_weighted_upper (N : ℕ) (ρ : ℝ) (k : ℕ × ℕ × ℕ) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D η z : ℝ} (hD : 2 ≤ D) (hη : 0 < η) (hηu : η < 1 / 8) (hcut : ∀ p ∈ P, ↑p < z) : have U := fouvryG9LongProducts N ρ k; have V := fouvryG9RectanglePrimeSupport N ρ k; have α := fouvryG9LongAlpha N ρ k; have β := fouvryG9RectangleBeta N; fouvryG9RectangleSifted N ρ k P ≤ ∑ t ∈ LiLiuPrereqWF.externalTags true P D η z, ∑ d ∈ (P.prod id).divisors, (LiLiuPrereqWF.externalTerm true P D η z t) d * AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9IntegerFibreCenter U V α β d + ∑ t ∈ LiLiuPrereqWF.externalTags true P D η z, ∑ d ∈ (P.prod id).divisors, (LiLiuPrereqWF.externalTerm true P D η z t) d * AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.bilinearDiscrepancy U V α β (↑N) d

Actual upper sieve with the exact C2 center. Divisor sums here still have the primorial carrier; transporting them is a separate obligation.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Rectangle_full_error_eq (N : ℕ) (ρ δ : ℝ) (k : ℕ × ℕ × ℕ) (c : ℕ → ℝ) : AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError (fouvryG9LongProducts N ρ k) (fouvryG9RectanglePrimeSupport N ρ k) (Finset.Ioc 0 ⌊↑N ^ (5 / 9 - δ) / (2 / 3 * ρ ^ k.1) ^ (5 / 9)⌋₊) (fouvryG9LongAlpha N ρ k) (fouvryG9RectangleBeta N) c ↑N = fouvryG9RectangleError N ρ δ k c

The full reduced sum on this very same rectangle is the previously proved actual G9 error, not a substitute discrepancy.