theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3base_log {a : ℝ} (ha : 0 < a) (haU : a ≤ 45 / 8) : 53 * ∫ (s : ℝ) in a..45 / 8, 1 / (s * (53 / 8 - s)) = 8 * Real.log (45 / 8 * (53 / 8 - a) / a)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3base4_bound : 53 * ∫ (s : ℝ) in 53 / 24..45 / 8, 1 / (s * (53 / 8 - s)) ≤ ↑s3Base4

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3base5_bound : 53 * ∫ (s : ℝ) in 265 / 88..45 / 8, 1 / (s * (53 / 8 - s)) ≤ ↑s3Base5