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

Monotonicity of the actual logarithmic integrand gives the sharp left-endpoint denominator.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.b10_li_interval_relative_upper (ε η : ℝ) (hε : 0 < ε) (hεlt : ε < 1) (hη : 0 < η) : ∃ (x₀ : ℝ), 2 ≤ x₀ ∧ ∀ (x : ℝ), x₀ ≤ x → ∀ (κ : ℝ), LiuWeight.liuLogarithmicIntegral κ x - LiuWeight.liuLogarithmicIntegral κ (ε * x) ≤ (1 - ε + η) * x / Real.log x

Scalar relative upper comparison. This is an integral estimate, not a new prime-distribution input.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ContinuousMainWeight_relative_upper (ε η : ℝ) (hε : 0 < ε) (hεlt : ε < 1) (hη : 0 < η) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (m : ℕ), 0 < m → ↑m ≤ ↑N ^ (2 / 3) → goldbachB10ContinuousMainWeight N ε m ≤ (1 - ε + η) * (↑N / ↑m) / Real.log (↑N / ↑m)