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

The literal author-weighted Buchstab integral; no counting interpretation is asserted.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorBuchstabIntegral = ∫ (r : ℝ) in 4 / 53..4 / 33, ∫ (q : ℝ) in r..4 / 33, ∫ (s : ℝ) in q..4 / 33, ∫ (t : ℝ) in s..4 / 33, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorWeight r * LiLiuPrereqBuchstab.buchstab ((1 - r - q - s - t) / q) / (r * q ^ 2 * s * t)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorBuchstab_argument {r q s t : ℝ} (hr : 4 / 53 ≤ r) (hrq : r ≤ q) (hqs : q ≤ s) (hst : s ≤ t) (ht : t ≤ 4 / 33) : 17 / 4 ≤ (1 - r - q - s - t) / q

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorBuchstab_t_intervalIntegrable {r q s : ℝ} (hr : r ∈ Set.Icc (4 / 53) (4 / 33)) (hq : q ∈ Set.Icc r (4 / 33)) (hs : s ∈ Set.Icc q (4 / 33)) : IntervalIntegrable (fun (t : ℝ) => goldbachG11AuthorWeight r * LiLiuPrereqBuchstab.buchstab ((1 - r - q - s - t) / q) / (r * q ^ 2 * s * t)) MeasureTheory.volume s (4 / 33)

Every literal inner slice is genuinely interval-integrable.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorBuchstab_s_intervalIntegrable {r q : ℝ} (hr : r ∈ Set.Icc (4 / 53) (4 / 33)) (hq : q ∈ Set.Icc r (4 / 33)) : IntervalIntegrable (fun (s : ℝ) => ∫ (t : ℝ) in s..4 / 33, goldbachG11AuthorWeight r * LiLiuPrereqBuchstab.buchstab ((1 - r - q - s - t) / q) / (r * q ^ 2 * s * t)) MeasureTheory.volume q (4 / 33)

The actual once-integrated kernel is integrable in the next variable.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorBuchstab_q_intervalIntegrable {r : ℝ} (hr : r ∈ Set.Icc (4 / 53) (4 / 33)) : IntervalIntegrable (fun (q : ℝ) => ∫ (s : ℝ) in q..4 / 33, ∫ (t : ℝ) in s..4 / 33, goldbachG11AuthorWeight r * LiLiuPrereqBuchstab.buchstab ((1 - r - q - s - t) / q) / (r * q ^ 2 * s * t)) MeasureTheory.volume r (4 / 33)

The actual twice-integrated kernel is integrable in q.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorBuchstab_r_intervalIntegrable : IntervalIntegrable (fun (r : ℝ) => ∫ (q : ℝ) in r..4 / 33, ∫ (s : ℝ) in q..4 / 33, ∫ (t : ℝ) in s..4 / 33, goldbachG11AuthorWeight r * LiLiuPrereqBuchstab.buchstab ((1 - r - q - s - t) / q) / (r * q ^ 2 * s * t)) MeasureTheory.volume (4 / 53) (4 / 33)

The outermost literal integrand is integrable, not a totalized undefined integral.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorBuchstabIntegral_le_scalar : goldbachG11AuthorBuchstabIntegral ≤ 561522 / 1000000 * goldbachG11PrimeIntegral goldbachG11AuthorWeight

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorBuchstabIntegral_le_10191 : goldbachG11AuthorBuchstabIntegral ≤ 10191 / 100000