theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PairLogKernel_le_mainIntegral_eventually (η : ℝ) (hη : 0 < η) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachB8PairLogKernel N ≤ goldbachB8MainIntegral + η

Select the mesh after the tolerance and the prime-size threshold after that mesh.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4_normalized_upper_integral (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hεu : ε < 2 / 15) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachS4 (goldbachDifferenceCarrier N ε) N (↑N ^ (3 / 11))) ≤ (8 * goldbachB8MainIntegral + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

The original S4 count has the genuine integral coefficient 8*I8. All sieve, Li, finite-transfer, grid and prime-size errors are paid.