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

Actual closed C10 kernel for S5, not the former C8 triangle.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PairLogKernel N = ∑ rs ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Pairs N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)), 1 / (↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Prod rs) * (1 - Real.log ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Prod rs) / Real.log ↑N))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusMainMass_le_pair_kernel (η : ℝ) (hη : 0 < η) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachB9PlusMainMass N ≤ (1 + η) * (↑N / Real.log ↑N) * goldbachB9PairLogKernel N

Relative full-prefix Li bound summed on the actual pair support. The prime-sum integral limit and low-first-prime improved coefficient are separate.