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

Exact inner integral with the additional low-first-prime factor from Eq. (5.45). This is a scalar identity, not an estimate for the actual low counting function.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9SubintervalIntegral_eq_single {a b : ℝ} (ha : 4 / 53 ≤ a) (hab : a ≤ b) (hb : b ≤ 1 / 3) : ∫ (u : ℝ) in a..b, ∫ (v : ℝ) in 1 / 3..(1 - u) / 2, 1 / (u * v * (1 - u - v)) = ∫ (u : ℝ) in a..b, Real.log (2 - 3 * u) / (u * (1 - u))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9WeightedSubintervalIntegral_eq_single {a b : ℝ} (ha : 4 / 53 ≤ a) (hab : a ≤ b) (hb : b ≤ 1 / 3) : ∫ (u : ℝ) in a..b, ∫ (v : ℝ) in 1 / 3..(1 - u) / 2, 1 / (u * v * (1 - u - v) * (1 - u)) = ∫ (u : ℝ) in a..b, Real.log (2 - 3 * u) / (u * (1 - u) ^ 2)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PaperSplitIntegral : ℝ

The literal scalar expression in the paper, without any assertion that it bounds S5.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PaperSplitIntegral = (36 / 5 * ∫ (u : ℝ) in 4 / 53..1 / 10, ∫ (v : ℝ) in 1 / 3..(1 - u) / 2, 1 / (u * v * (1 - u - v) * (1 - u))) + 8 * ∫ (u : ℝ) in 1 / 10..1 / 3, ∫ (v : ℝ) in 1 / 3..(1 - u) / 2, 1 / (u * v * (1 - u - v))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PaperSplitIntegral_eq_singleIntegrals : goldbachB9PaperSplitIntegral = (36 / 5 * ∫ (u : ℝ) in 4 / 53..1 / 10, Real.log (2 - 3 * u) / (u * (1 - u) ^ 2)) + 8 * ∫ (u : ℝ) in 1 / 10..1 / 3, Real.log (2 - 3 * u) / (u * (1 - u))

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

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.intervalIntegrable_goldbachB9WeightedInner {u : ℝ} (hu : u ∈ Set.Icc (4 / 53) (1 / 3)) : IntervalIntegrable (fun (v : ℝ) => 1 / (u * v * (1 - u - v) * (1 - u))) MeasureTheory.volume (1 / 3) ((1 - u) / 2)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.intervalIntegrable_goldbachB9WeightedOuter : IntervalIntegrable (fun (u : ℝ) => ∫ (v : ℝ) in 1 / 3..(1 - u) / 2, 1 / (u * v * (1 - u - v) * (1 - u))) MeasureTheory.volume (4 / 53) (1 / 3)

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

Continuous interval splitting is justified by integrability; it does not alter how the finite first-prime boundary is assigned to the high counting family.