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

The original S5Closed count has the coarse integral coefficient 8*I9; not the improved low-r coefficient. All sieve, Li, finite-transfer, grid and prime-size errors are paid.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9MainIntegral_eq_singleIntegral : goldbachB9MainIntegral = ∫ (u : ℝ) in 4 / 53..1 / 3, Real.log (2 - 3 * u) / (u * (1 - u))