theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_scalar_base_integral {a b c : ℝ} (ha : 0 < a) (hab : a ≤ b) (hbc : b < c) : ∫ (s : ℝ) in a..b, 1 / (s * (c - s)) = (Real.log b - Real.log (c - b) - (Real.log a - Real.log (c - a))) / c

Exact base-kernel integration on the whole positive interval.