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

The actual finite prime-pair kernel; no integral limit is asserted.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PairLogKernel N = ∑ rs ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Pairs N (↑N ^ (3 / 11)), 1 / (↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8Prod rs) * (1 - Real.log ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8Prod rs) / Real.log ↑N))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusMainMass_eq_pair_sum (N : ℕ) : goldbachB8PlusMainMass N = ∑ rs ∈ goldbachS4Pairs N (↑N ^ (3 / 11)), LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) (↑N / ↑(goldbachC8Prod rs))

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

Uniform relative Li payment on the real C8 support, followed by exact product-to-pair reindexing. The moving triangular prime-sum limit remains separate.