theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeIntegral_t_eq (h : ℝ → ℝ) (r q s : ℝ) {b c : ℝ} (hb : 0 < b) (hc : 0 < c) : ∫ (t : ℝ) in b..c, h r / (r * q ^ 2 * s * t) = h r / (r * q ^ 2 * s) * Real.log (c / b)

Integration over the independent cross interval.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeIntegral_inner_eq (h : ℝ → ℝ) (r : ℝ) {b c q : ℝ} (hq : 0 < q) (hqb : q ≤ b) (hc : 0 < c) : ∫ (s : ℝ) in q..b, ∫ (t : ℝ) in b..c, h r / (r * q ^ 2 * s * t) = h r / (r * q ^ 2) * Real.log (c / b) * Real.log (b / q)

The last two variables give a product of logarithms, not a log square.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeIntegral_qPrimitive_deriv {b q : ℝ} (hb : 0 < b) (hq : 0 < q) : HasDerivAt (fun (x : ℝ) => (1 - Real.log (b / x)) / x) (Real.log (b / q) / q ^ 2) q

Primitive for the remaining inner variable.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeIntegral_qIntegral {b r : ℝ} (hr : 0 < r) (hrb : r ≤ b) : ∫ (q : ℝ) in r..b, Real.log (b / q) / q ^ 2 = 1 / b + (Real.log (b / r) - 1) / r

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeIntegral_eq_single (h : ℝ → ℝ) : goldbachG12PrimeIntegral h = Real.log (3 / 11 / (4 / 33)) * ∫ (r : ℝ) in 4 / 53..4 / 33, h r / r * (1 / (4 / 33) + (Real.log (4 / 33 / r) - 1) / r)

Exact reduction of the original cross integral. Continuity is not needed for the identity.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.intervalIntegrable_goldbachG12PrimeSingleIntegrand (h : ℝ → ℝ) (hh : ContinuousOn h (Set.Icc (4 / 53) (4 / 33))) : IntervalIntegrable (fun (r : ℝ) => h r / r * (1 / (4 / 33) + (Real.log (4 / 33 / r) - 1) / r)) MeasureTheory.volume (4 / 53) (4 / 33)

Continuous weights give a genuinely integrable one-dimensional integrand.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeIntegral_onePrimitive_deriv {b r : ℝ} (hb : 0 < b) (hr : 0 < r) : HasDerivAt (fun (x : ℝ) => -Real.log (b / x) / b + (2 - Real.log (b / x)) / x) (1 / r * (1 / b + (Real.log (b / r) - 1) / r)) r

Primitive of the constant-weight reduced kernel.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeIntegral_one_closed : (goldbachG12PrimeIntegral fun (x : ℝ) => 1) = Real.log (9 / 4) * (43 / 2 * Real.log (53 / 33) - 10)

Closed form for the constant weight on the original cross domain.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeIntegral_t_intervalIntegrable (h : ℝ → ℝ) {r q s : ℝ} (hr : 0 < r) (hq : 0 < q) (hs : 0 < s) : IntervalIntegrable (fun (t : ℝ) => h r / (r * q ^ 2 * s * t)) MeasureTheory.volume (4 / 33) (3 / 11)

Every literal innermost cross slice is integrable.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeIntegral_s_intervalIntegrable (h : ℝ → ℝ) {r q : ℝ} (hq : 0 < q) (hqb : q ≤ 4 / 33) : IntervalIntegrable (fun (s : ℝ) => ∫ (t : ℝ) in 4 / 33..3 / 11, h r / (r * q ^ 2 * s * t)) MeasureTheory.volume q (4 / 33)

The once-integrated literal cross kernel is integrable.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeIntegral_q_intervalIntegrable (h : ℝ → ℝ) {r : ℝ} (hr : 0 < r) (hrb : r ≤ 4 / 33) : IntervalIntegrable (fun (q : ℝ) => ∫ (s : ℝ) in q..4 / 33, ∫ (t : ℝ) in 4 / 33..3 / 11, h r / (r * q ^ 2 * s * t)) MeasureTheory.volume r (4 / 33)

The twice-integrated literal cross kernel is integrable.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeIntegral_rSlice_eq (h : ℝ → ℝ) {r : ℝ} (hr : 0 < r) (hrb : r ≤ 4 / 33) : ∫ (q : ℝ) in r..4 / 33, ∫ (s : ℝ) in q..4 / 33, ∫ (t : ℝ) in 4 / 33..3 / 11, h r / (r * q ^ 2 * s * t) = Real.log (3 / 11 / (4 / 33)) * (h r / r * (1 / (4 / 33) + (Real.log (4 / 33 / r) - 1) / r))

The outer literal slice has the same pointwise reduction.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeIntegral_r_intervalIntegrable (h : ℝ → ℝ) (hh : ContinuousOn h (Set.Icc (4 / 53) (4 / 33))) : IntervalIntegrable (fun (r : ℝ) => ∫ (q : ℝ) in r..4 / 33, ∫ (s : ℝ) in q..4 / 33, ∫ (t : ℝ) in 4 / 33..3 / 11, h r / (r * q ^ 2 * s * t)) MeasureTheory.volume (4 / 53) (4 / 33)

Continuous weights also make the original outer literal slice integrable.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeIntegral_author_split : goldbachG12PrimeIntegral goldbachG11AuthorWeight = Real.log (9 / 4) * ((36 / 5 * ∫ (r : ℝ) in 4 / 53..1 / 10, (1 / (4 / 33) + (Real.log (4 / 33 / r) - 1) / r) / (r * (1 - r))) + 8 * ∫ (r : ℝ) in 1 / 10..4 / 33, (1 / (4 / 33) + (Real.log (4 / 33 / r) - 1) / r) / r)

Exact piecewise one-dimensional formula for the author's weight.