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

The exact low-grid main term, before arithmetic density/Euler normalization.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LowGridDensityMain N ε δ θ ρ P z = ∑ k ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LowGridUsed N ε ρ, ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridLong N ε ρ k, ∑ p ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridShort N ρ k, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectangleWeight N (m, p) * MathlibNt.SieveTheory.LiLiuPrereqWF.externalDensity true (P k) (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridLowLevel N δ ρ k) θ) θ (z k) (MathlibNt.SieveTheory.LiLiuPrereqWF.progressionDensity (m * p))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LowGrid_sifted_paid (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 : ℕ × ℕ → ℝ), (∀ k ∈ goldbachG11LowGridUsed N ε ρ, ∀ p ∈ P k, Nat.Prime p) → (∀ k ∈ goldbachG11LowGridUsed N ε ρ, ∀ p ∈ P k, p.Coprime N) → (∀ k ∈ goldbachG11LowGridUsed N ε ρ, ∀ p ∈ P k, ↑p < z k) → ∑ k ∈ goldbachG11LowGridUsed N ε ρ, goldbachG11RectangleSiftedMass N (goldbachG11GridLong N ε ρ k) (goldbachG11GridShort N ρ k) (P k) ≤ goldbachG11LowGridDensityMain N ε δ θ ρ P z + 2 * ↑N / Real.log ↑N ^ A

Actual low-grid sifted counts with all distribution and primorial/full transport errors paid. Only structural conditions on the changing sieve remain.