Documentation

MathlibNt.SieveTheory.LiLiuGoldbachB10IntegralScalar

source
theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10I10_eight_mul_le_540996 :
8 * goldbachB10I10 ≤ 540996 / 100000

Unconditional purely analytic bound for the unchanged production integral I10.

Inspect dependencies

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