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

Exact evaluation of the inner v-integral in Liu's printed I10 over the actual closed u-interval [β, γ].

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10MainIntegral_eq_singleIntegral : goldbachB10MainIntegral = ∫ (u : ℝ) in goldbachB10Beta..goldbachB10Gamma, Real.log ((1 - u - goldbachB10Gamma) / goldbachB10Gamma) / (u * (1 - u))

Liu's exact double integral goldbachB10MainIntegral reduces to a single closed-form interval integral.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10I10_eq_singleIntegral : goldbachB10I10 = ∫ (u : ℝ) in goldbachB10Beta..goldbachB10Gamma, Real.log ((1 - u - goldbachB10Gamma) / goldbachB10Gamma) / (u * (1 - u))

The production alias goldbachB10I10 is exactly the reduced one-dimensional integral.