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

The original ordinary pi-centered main term on any selected actual cells.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryDensityMain N ε ρ δ θ S P z = ∑ k ∈ S, ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridLong N ε ρ k, ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m) * (Wu2004MeanValue.realPrimeCount (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridProfileHi ρ k) - Wu2004MeanValue.realPrimeCount (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridProfileLo N ρ k)) * MathlibNt.SieveTheory.LiLiuPrereqWF.externalDensity true (P k) (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryLevel N δ) θ) θ (z k) (MathlibNt.SieveTheory.LiLiuPrereqWF.progressionDensity m)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryGrid_sifted_paid (A : ℕ) {δ θ ρ : ℝ} (hδ : 0 < δ) (hδu : δ < 1 / 2) (hθ : 0 < θ) (hθu : θ < 1 / 8) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (ε : ℝ), ∀ S ⊆ goldbachG11GridUsed N ε ρ, ∀ (P : ℕ × ℕ → Finset ℕ) (z : ℕ × ℕ → ℝ), (∀ k ∈ S, ∀ p ∈ P k, Nat.Prime p) → (∀ k ∈ S, ∀ p ∈ P k, p.Coprime N) → (∀ k ∈ S, ∀ p ∈ P k, ↑p < z k) → ∑ k ∈ S, goldbachG11AllPrimeSiftedMass N (goldbachG11GridLong N ε ρ k) (goldbachG11GridShort N ρ k) (P k) ≤ goldbachG11OrdinaryDensityMain N ε ρ δ θ S P z + ↑N / Real.log ↑N ^ A

Fully paid ordinary sifted counts on any subset of occupied cells. The threshold precedes epsilon, the cell subset and all changing sieve data.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryGrid_prime_outputs_paid (A : ℕ) {δ θ ρ : ℝ} (hδ : 0 < δ) (hδu : δ < 1 / 2) (hθ : 0 < θ) (hθu : θ < 1 / 8) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (ε : ℝ), ∀ S ⊆ goldbachG11GridUsed N ε ρ, ∀ (z : ℝ), 0 ≤ z → z ≤ √↑N → ∑ k ∈ S, goldbachG11RectanglePrimeMass N (goldbachG11GridLong N ε ρ k) (goldbachG11GridShort N ρ k) ≤ (goldbachG11OrdinaryDensityMain N ε ρ δ θ S (fun (x : ℕ × ℕ) => fouvryG9SievePrimes N z) fun (x : ℕ × ℕ) => z) + 2 * ↑N / Real.log ↑N ^ A

Only the sifted part is enlarged to all primes. The original already-paid small-output budget is retained, so no new all-prime fibre estimate is needed.