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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ContinuousMainWeight 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.goldbachB10ContinuousMainMass (N : ℕ) (ε b c : ℝ) : ℝ

Equations

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10MainWeight_sub_continuous_nonneg_le {N m : ℕ} {ε : ℝ} (hε : 0 ≤ ε) (hm : 0 < m) (hlo : 2 ≤ ↑⌊ε * ↑N⌋₊ / ↑m) : 0 ≤ goldbachB10MainWeight N ε m - goldbachB10ContinuousMainWeight N ε m ∧ goldbachB10MainWeight N ε m - goldbachB10ContinuousMainWeight N ε m ≤ 1 / Real.log 2 * (1 / ↑m)

Flooring increases the main weight; the interval correction is charged with its sign.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10MainMass_sub_continuous_nonneg_le {N : ℕ} {ε b c : ℝ} (hε : 0 ≤ ε) (hlo : ∀ m ∈ goldbachC10ProductSupport N b c, 0 < m ∧ 2 ≤ ↑⌊ε * ↑N⌋₊ / ↑m) : 0 ≤ goldbachB10MainMass N ε b c - goldbachB10ContinuousMainMass N ε b c ∧ goldbachB10MainMass N ε b c - goldbachB10ContinuousMainMass N ε b c ≤ 1 / Real.log 2 * ∑ m ∈ goldbachC10ProductSupport N b c, 1 / ↑m

Same-support finite floor correction; no prime labels or endpoints are removed.

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

A uniform-in-beta floor payment. The coarse power bound suffices for the main scale.

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