noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10MainWeight (N : ℕ) (ε : ℝ) (m : ℕ) : ℝ

The actual floor-endpoint Li interval weight, before the divisor coprimality gate.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10MainWeight N ε m = MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PanKappa0 (↑N / ↑m) - MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PanKappa0 (↑⌊ε * ↑N⌋₊ / ↑m)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10MainMass (N : ℕ) (ε b c : ℝ) : ℝ

Common main mass on the actual product support, with labels already accounted for by the proved injectivity of the ordered prime-pair product.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10MainMass N ε b c = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10ProductSupport N b c, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10MainWeight N ε m

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.b10_li_difference_nonneg_le (κ a b : ℝ) (ha : 2 ≤ a) (hab : a ≤ b) : 0 ≤ LiuWeight.liuLogarithmicIntegral κ b - LiuWeight.liuLogarithmicIntegral κ a ∧ LiuWeight.liuLogarithmicIntegral κ b - LiuWeight.liuLogarithmicIntegral κ a ≤ (b - a) / Real.log 2

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10MainWeight_bounds_eventually (ε γ : ℝ) (hε : 0 < ε) (hεlt : ε < 1) (hγ : γ < 1 / 3) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (β : ℝ), 1 / 18 < β → ∀ m ∈ goldbachC10ProductSupport N (↑N ^ β) (↑N ^ γ), 0 ≤ goldbachB10MainWeight N ε m ∧ |goldbachB10MainWeight N ε m| ≤ ↑N / Real.log 2 / ↑m

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10MainMass_nonneg_eventually (ε γ : ℝ) (hε : 0 < ε) (hεlt : ε < 1) (hγ : γ < 1 / 3) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (β : ℝ), 1 / 18 < β → 0 ≤ goldbachB10MainMass N ε (↑N ^ β) (↑N ^ γ)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PanMainPrefix_eq_support_sum {N Y A₁ A₂ d : ℕ} {b c : ℝ} (hsupp : ∀ ⦃m : ℕ⦄, m ∈ goldbachC10ProductSupport N b c → m ∈ Finset.Ioc A₁ A₂) : goldbachB10PanMainPrefix N Y A₁ A₂ d b c = ∑ m ∈ goldbachC10ProductSupport N b c, if m.Coprime d then LiuWeight.liuLogarithmicIntegral goldbachB10PanKappa0 (↑Y / ↑m) / ↑d.totient else 0

Exact support restriction of the already-defined Pan main prefix.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PanMainPrefix_sub_eq_gatedMainWeight {N A₁ A₂ d : ℕ} {ε b c : ℝ} (hsupp : ∀ ⦃m : ℕ⦄, m ∈ goldbachC10ProductSupport N b c → m ∈ Finset.Ioc A₁ A₂) : goldbachB10PanMainPrefix N N A₁ A₂ d b c - goldbachB10PanMainPrefix N ⌊ε * ↑N⌋₊ A₁ A₂ d b c = (∑ m ∈ goldbachC10ProductSupport N b c, if m.Coprime d then goldbachB10MainWeight N ε m else 0) / ↑d.totient

Same-source main-prefix subtraction, still retaining the divisor coprimality gate.