noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectangleEulerMass (N : ℕ) (ρ : ℝ) (k : ℕ × ℕ × ℕ) (P : Finset ℕ) : ℝ

Actual weighted Euler mass, retaining all product-dependent exclusions.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectangleEulerMass N ρ k P = ∑ 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 * ∏ p ∈ P, (1 - (MathlibNt.SieveTheory.LiLiuPrereqWF.progressionDensity (m * n)) p)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9UpperFactor (N : ℕ) (Q C K η : ℝ) : ℝ

The genuine extended upper-sieve factor at the original level and sqrt(N).

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9UpperFactor N Q C K η = MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965F (Real.log Q / Real.log √↑N) + C * (η + (η ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log Q ^ (-(1 / 3)))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectangleMain_upper : ∃ (C : ℝ), 0 < C ∧ ∃ (K : ℝ), 1 < K ∧ ∀ (δ η : ℝ), 0 ≤ δ → δ < 1 / 4 → 0 < η → η < 1 / 8 → ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → Even N → ∀ (e ρ : ℝ), 0 < e → 1 < ρ → ρ ≤ 5 / 4 → ∀ (k : ℕ × ℕ × ℕ), (fouvryG9GridCell N e ρ k).Nonempty → have Q := ↑N ^ (5 / 9 - δ) / (2 / 3 * ρ ^ k.1) ^ (5 / 9); have P := fouvryG9SievePrimes N √↑N; 0 ≤ fouvryG9UpperFactor N Q C K η ∧ fouvryG9RectangleMain N ρ δ η k P √↑N ≤ fouvryG9UpperFactor N Q C K η * fouvryG9RectangleEulerMass N ρ k P

Uniform analytic evaluation of every actual rectangle density. The fixed constants and common threshold precede all cells, products and grids. The positive Euler correction and the prime-box mass have not been suppressed.