@[instance_reducible]

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableS2MainMassUpper (P : Prop) : Decidable P

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableS2MainMassUpper P = Classical.propDecidable P

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2MainMassUpperSum (N : ℕ) (τ : ℝ) : ℝ

The literal S2 main-mass sum at the genuine single-endpoint carrier r ∈ R(N,N^τ).

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2MainMassUpperSum N τ = ∑ r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2Primes N (↑N ^ τ), MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) (↑N / ↑r)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2MainMassUpper (τ η : ℝ) (hτ : 1 / 3 < τ) (hτu : τ < 1 / 2) (hη : 0 < η) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachS2MainMassUpperSum N τ ≤ (Real.log ((1 - τ) / τ) + η) * (↑N / Real.log ↑N)

For every fixed 1/3 < τ < 1/2, the literal single-endpoint S2 main-mass sum is eventually bounded by the exact logarithmic kernel log ((1-τ)/τ). The finite carrier is the actual goldbachS2Primes carrier, with no switched source predicate.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2MainMassUpper_nine_nineteen_sub (η ε : ℝ) (hη : 0 < η) (hε : 0 < ε) (hεu : ε < 2 / 15) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachS2MainMassUpperSum N (9 / 19 - ε) ≤ (Real.log ((1 - (9 / 19 - ε)) / (9 / 19 - ε)) + η) * (↑N / Real.log ↑N)

Specialization of goldbachS2MainMassUpper to τ = 9 / 19 - ε under the task-local constraint 0 < ε < 2 / 15.