noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectangleMain (N : ℕ) (ρ δ η : ℝ) (k : ℕ × ℕ × ℕ) (P : Finset ℕ) (z : ℝ) : ℝ

The literal normalized external-density main term for one occupied rectangle.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectangleMain N ρ δ η k P z = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongProducts N ρ k, ∑ n ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectanglePrimeSupport N ρ k, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongAlpha N ρ k m * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectangleBeta N n * MathlibNt.SieveTheory.LiLiuPrereqWF.externalDensity true P (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel (↑N ^ (5 / 9 - δ) / (2 / 3 * ρ ^ k.1) ^ (5 / 9)) η) η z (MathlibNt.SieveTheory.LiLiuPrereqWF.progressionDensity (m * n))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Sieve_total (A : ℕ) {e ε δ η ρ : ℝ} (he : 0 < e) (he1 : e ≤ 1) (hε : 0 < ε) (hεa : ε < 4 / 53) (hεδ : ε < δ) (hδ : δ < 1 / 2) (hη : 0 < η) (hηu : η < 1 / 8) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → ∀ (P : ℕ × ℕ × ℕ → Finset ℕ) (z : ℕ × ℕ × ℕ → ℝ), (∀ k ∈ fouvryG9GridUsed N e ρ, ∀ p ∈ P k, Nat.Prime p) → (∀ k ∈ fouvryG9GridUsed N e ρ, ∀ p ∈ P k, p.Coprime N) → (∀ k ∈ fouvryG9GridUsed N e ρ, ∀ p ∈ P k, ↑p < z k) → ∑ k ∈ fouvryG9GridUsed N e ρ, fouvryG9RectangleSifted N ρ k (P k) ≤ ∑ k ∈ fouvryG9GridUsed N e ρ, fouvryG9RectangleMain N ρ δ η k (P k) (z k) + ↑N / Real.log ↑N ^ A

Actual upper sieving on the entire occupied grid, with all distribution and exceptional-transport costs paid. No weight, discrepancy, or mass bound is an input. The displayed main term is an exact density expression, not yet its analytic asymptotic evaluation. Prime carriers and cutoffs follow the threshold.