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

Exact inner evaluation, including the degenerate interval at u = 1/3.

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8MainIntegral_eq_singleIntegral : goldbachB8MainIntegral = ∫ (u : ℝ) in 3 / 11..1 / 3, Real.log (1 / u - 2) / (u * (1 - u))

This is the production double integral itself, with no factor eight.

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

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8SingleIntegrand_nonneg {u : ℝ} (hu : u ∈ Set.Icc (3 / 11) (1 / 3)) : 0 ≤ Real.log (1 / u - 2) / (u * (1 - u))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.continuousOn_goldbachB8TransformedIntegrand : ContinuousOn (fun (t : ℝ) => Real.log (t - 1) / t) (Set.Icc 2 (8 / 3))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.intervalIntegrable_goldbachB8TransformedIntegrand : IntervalIntegrable (fun (t : ℝ) => Real.log (t - 1) / t) MeasureTheory.volume 2 (8 / 3)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8TransformedIntegrand_nonneg {t : ℝ} (ht : t ∈ Set.Icc 2 (8 / 3)) : 0 ≤ Real.log (t - 1) / t

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8ReductionChange_endpoints : 1 / (2 + 1) = 1 / 3 ∧ 1 / (8 / 3 + 1) = 3 / 11

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8ReductionChange_mapsTo : Set.MapsTo (fun (t : ℝ) => 1 / (t + 1)) (Set.Icc 2 (8 / 3)) (Set.Icc (3 / 11) (1 / 3))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.hasDerivAt_goldbachB8ReductionChange {t : ℝ} (ht : t ∈ Set.Icc 2 (8 / 3)) : HasDerivAt (fun (t : ℝ) => 1 / (t + 1)) (-1 / (t + 1) ^ 2) t

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.continuousOn_goldbachB8ReductionChange : ContinuousOn (fun (t : ℝ) => 1 / (t + 1)) (Set.Icc 2 (8 / 3))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.continuousOn_goldbachB8ReductionJacobian : ContinuousOn (fun (t : ℝ) => -1 / (t + 1) ^ 2) (Set.Icc 2 (8 / 3))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8ReductionChange_integrand {t : ℝ} (ht : t ∈ Set.Icc 2 (8 / 3)) : Real.log (1 / (1 / (t + 1)) - 2) / (1 / (t + 1) * (1 - 1 / (t + 1))) * (-1 / (t + 1) ^ 2) = -(Real.log (t - 1) / t)

The negative sign is the Jacobian, before reversal of the integration limits.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8ReductionChange_oriented : ∫ (t : ℝ) in 2..8 / 3, Real.log (1 / (1 / (t + 1)) - 2) / (1 / (t + 1) * (1 - 1 / (t + 1))) * (-1 / (t + 1) ^ 2) = ∫ (u : ℝ) in 1 / 3..3 / 11, Real.log (1 / u - 2) / (u * (1 - u))

Directed substitution: g(2) = 1/3 and g(8/3) = 3/11.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8MainIntegral_eq_transformedIntegral : goldbachB8MainIntegral = ∫ (t : ℝ) in 2..8 / 3, Real.log (t - 1) / t

Exact reduction of actual I8; the reversed limits cancel the negative Jacobian.