theorem goldbachG11AuthorBuchstabIntegral_eq_literal : 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)

Definitional source-faithfulness check: the public object is the literal fourfold integral.