theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeInterval_mass {L U : ℝ} (hLU : L ≤ U) : ∑ p ∈ AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWInterval L U, AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta p = Wu2004MeanValue.realPrimeCount U - Wu2004MeanValue.realPrimeCount L

Exact conversion, with the same half-open natural endpoints and no PNT error.

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridPlainMass N ε ρ k = ∑ v ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridLong N ε ρ k ×ˢ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridShort N ρ k, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AllPrimeWeight N v

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryDensityMain_eq_pairs {N : ℕ} {ε ρ δ θ : ℝ} (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (hbig : 4 ≤ ↑N ^ (4 / 53)) (S : Finset (ℕ × ℕ)) (hS : S ⊆ goldbachG11GridUsed N ε ρ) (P : ℕ × ℕ → Finset ℕ) (z : ℕ × ℕ → ℝ) : goldbachG11OrdinaryDensityMain N ε ρ δ θ S P z = ∑ k ∈ S, ∑ v ∈ goldbachG11GridLong N ε ρ k ×ˢ goldbachG11GridShort N ρ k, goldbachG11AllPrimeWeight N v * LiLiuPrereqWF.externalDensity true (P k) (LiLiuPrereqWF.externalInternalLevel (goldbachG11OrdinaryLevel N δ) θ) θ (z k) (LiLiuPrereqWF.progressionDensity v.1)

The ordinary pi-center is precisely a finite all-prime rectangle main term with progression argument m (not m*p).