noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiCenterMass (κ : ℝ) (N : ℕ) (ε : ℝ) (D : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiCenterMass κ N ε D = ∑ d ∈ Finset.Icc 1 D, |∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EffectiveProductSupport N ε with m.Coprime d, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EffectiveProductCoefficient N ε m * (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiEndpointError κ N ε m / ↑d.totient)|

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiCenterMass_zero (κ : ℝ) (N : ℕ) (ε : ℝ) : goldbachG11PiLiCenterMass κ N ε 0 = 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiCenterMass_eps_one (κ : ℝ) (N D : ℕ) : goldbachG11PiLiCenterMass κ N 1 D = 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLi_reciprocal_product_mass (N d : ℕ) (ε : ℝ) : ∑ m ∈ goldbachG11EffectiveProductSupport N ε with m.Coprime d, (↑m)⁻¹ ≤ 1 + Real.log ↑N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLi_center_mass_bound (κ U : ℝ) (hU : 0 < U) : ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ε : ℝ), ∀ D ≤ N, goldbachG11PiLiCenterMass κ N ε D ≤ C * ↑N / Real.log ↑N ^ U

Only the centering difference is triangularized; this is not an AP distribution bound.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLi_center_change (κ U : ℝ) (hU : 0 < U) : ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ε : ℝ), ∀ D ≤ N, ∑ d ∈ Finset.Icc 1 D, |∑ m ∈ goldbachG11EffectiveProductSupport N ε with m.Coprime d, goldbachG11EffectiveProductCoefficient N ε m * ((AnalyticNumberTheory.LargeSieve.PanPrincipal.primeCount ⌊goldbachG11PiLiHi N m⌋₊ - AnalyticNumberTheory.LargeSieve.PanPrincipal.primeCount ⌊goldbachG11PiLiLo N ε m⌋₊ - (LiuWeight.liuLogarithmicIntegral κ (goldbachG11PiLiHi N m) - LiuWeight.liuLogarithmicIntegral κ (goldbachG11PiLiLo N ε m))) / ↑d.totient)| ≤ C * ↑N / Real.log ↑N ^ U