theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Grid_low_high_sum (N : ℕ) (ε ρ : ℝ) (f : ℕ × ℕ → ℝ) : ∑ k ∈ goldbachG11LowGridUsed N ε ρ, f k + ∑ k ∈ goldbachG11HighGridUsed N ε ρ, f k = ∑ k ∈ goldbachG11GridUsed N ε ρ, f k

Exact complementary split: equality at the short-cell boundary is low.

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MixedDensityMain (N : ℕ) (ε ρ δ θ z : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MixedDensityMain N ε ρ δ θ z = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LowGridDensityMain N ε δ θ ρ (fun (x : ℕ × ℕ) => MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9SievePrimes N z) fun (x : ℕ × ℕ) => z) + MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryDensityMain N ε ρ δ θ (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11HighGridUsed N ε ρ) (fun (x : ℕ × ℕ) => MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9SievePrimes N z) fun (x : ℕ × ℕ) => z

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodSwitchedTotal_le_mixedDensity (A : ℕ) {ε ρ δ θ : ℝ} (hε : 0 < ε) (hεu : ε ≤ 1) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (hδ : 0 < δ) (hδu : δ < 1 / 2) (hθ : 0 < θ) (hθu : θ < 1 / 8) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (z : ℝ), 0 ≤ z → z ≤ √↑N → ↑(goldbachG11GoodSwitchedTotal N ε (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ goldbachG11MixedDensityMain N ε ρ δ θ z + 5 * ↑N / Real.log ↑N ^ A

The original good G11 count, with both actual distribution routes and all small-output/transport errors paid. Only the explicit arithmetic main term remains.