MathlibNt.SieveTheory.LiLiuGoldbachS3IntegralScalarEnvelopeBounds

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_fullEnvelope_continuousOn :

ContinuousOn goldbachS3_fullEnvelope (Set.Icc (53 / 24) (45 / 8))

The explicit rational envelope is continuous on the full original integration interval.

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_fullEnvelope_continuousOn · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_oneThird_integral_le_fullEnvelope :

goldbachS3_oneThirdExpFreeIntegral ≤ ∫ (s : ℝ) in 53 / 24..45 / 8, goldbachS3_fullEnvelope s

A genuine integral comparison for the first named endpoint, with no bound hypothesis.

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_oneThird_integral_le_fullEnvelope · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_threeElevenths_integral_le_fullEnvelope :

goldbachS3_threeEleventhsExpFreeIntegral ≤ ∫ (s : ℝ) in 265 / 88..45 / 8, goldbachS3_fullEnvelope s

A genuine integral comparison for the second named endpoint, on its unchanged interval.

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_threeElevenths_integral_le_fullEnvelope · compiled type and proof/definition references.