MathlibNt.SieveTheory.LiLiuGoldbachG11AuthorIntegralScalar

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11Author_log53_bounds :

473784352085 / 1000000000000 ≤ Real.log (53 / 33) ∧ Real.log (53 / 33) ≤ 473784352086 / 1000000000000

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11Author_log40_bounds :

192371892647 / 1000000000000 ≤ Real.log (40 / 33) ∧ Real.log (40 / 33) ≤ 192371892648 / 1000000000000

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11Author_primitives_scalar_bound :

561522 / 1000000 * (36 / 5 * (g11AuthorMajorantPrimitive (1 / 10) - g11AuthorMajorantPrimitive (4 / 53)) + 8 * (g11AuthorPrimitive0 (4 / 33) - g11AuthorPrimitive0 (1 / 10))) ≤ 10191 / 100000

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeIntegral_author_scalar_le_10191 :

561522 / 1000000 * goldbachG11PrimeIntegral goldbachG11AuthorWeight ≤ 10191 / 100000

Scalar certification of the author integral only; not an actual G11 bound.

Inspect dependencies

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