theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeIntegral_logTriangle {b q : ℝ} (hq : 0 < q) (hqb : q ≤ b) : ∫ (s : ℝ) in q..b, ∫ (t : ℝ) in s..b, 1 / (s * t) = Real.log (b / q) ^ 2 / 2

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeIntegral_eq_double (h : ℝ → ℝ) : goldbachG11PrimeIntegral h = ∫ (r : ℝ) in 4 / 53..4 / 33, ∫ (q : ℝ) in r..4 / 33, h r / (r * q ^ 2) * (Real.log (4 / 33 / q) ^ 2 / 2)

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

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeIntegral_eq_single (h : ℝ → ℝ) : goldbachG11PrimeIntegral h = ∫ (r : ℝ) in 4 / 53..4 / 33, h r / r * ((Real.log (4 / 33 / r) ^ 2 - 2 * Real.log (4 / 33 / r) + 2) / r - 2 / (4 / 33)) / 2

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeIntegral_one_eq_single : (goldbachG11PrimeIntegral fun (x : ℝ) => 1) = ∫ (r : ℝ) in 4 / 53..4 / 33, ((Real.log (4 / 33 / r) ^ 2 - 2 * Real.log (4 / 33 / r) + 2) / r - 2 / (4 / 33)) / (2 * r)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeIntegral_author_eq_single : goldbachG11PrimeIntegral goldbachG11AuthorWeight = ∫ (r : ℝ) in 4 / 53..4 / 33, goldbachG11AuthorWeight r / r * ((Real.log (4 / 33 / r) ^ 2 - 2 * Real.log (4 / 33 / r) + 2) / r - 2 / (4 / 33)) / 2

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeIntegral_nonneg (h : ℝ → ℝ) (hh : ∀ r ∈ Set.Icc (4 / 53) (4 / 33), 0 ≤ h r) : 0 ≤ goldbachG11PrimeIntegral h

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeIntegral_const (c : ℝ) : (goldbachG11PrimeIntegral fun (x : ℝ) => c) = c * goldbachG11PrimeIntegral fun (x : ℝ) => 1

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