theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9InnerIntegral_eq {u : ℝ} (hu : u ∈ Set.Icc (4 / 53) (1 / 3)) : ∫ (v : ℝ) in 1 / 3..(1 - u) / 2, 1 / (u * v * (1 - u - v)) = Real.log ((1 - u - 1 / 3) / (1 / 3)) / (u * (1 - u))

Exact evaluation of the inner v-integral in the actual B9 kernel over the actual closed u-interval [4/53, 1/3].

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9InnerIntegral_eq_logTwoSubThree {u : ℝ} (hu : u ∈ Set.Icc (4 / 53) (1 / 3)) : ∫ (v : ℝ) in 1 / 3..(1 - u) / 2, 1 / (u * v * (1 - u - v)) = Real.log (2 - 3 * u) / (u * (1 - u))

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.continuousOn_goldbachB9SingleIntegrand : ContinuousOn (fun (u : ℝ) => Real.log (2 - 3 * u) / (u * (1 - u))) (Set.Icc (4 / 53) (1 / 3))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.intervalIntegrable_goldbachB9SingleIntegrand : IntervalIntegrable (fun (u : ℝ) => Real.log (2 - 3 * u) / (u * (1 - u))) MeasureTheory.volume (4 / 53) (1 / 3)