Documentation

MathlibNt.SieveTheory.LiLiuGoldbachG12BuchstabMajorantPolynomials

source
theorem LiLiuGoldbachG12BuchstabMajorant.polynomial1_broad {x : ℝ} (hx : 0 ≤ x) (hx' : x ≤ 1 / 1) :
Polynomial.eval x LiLiuBuchstabSharp.closureP1 ≤ 56438299999 / 100000000000

Exact positive-coefficient identity on a whole real interval.

Inspect dependencies

LiLiuGoldbachG12BuchstabMajorant.polynomial1_broad · compiled type and proof/definition references.

source
theorem LiLiuGoldbachG12BuchstabMajorant.polynomial1_sharp {x : ℝ} (hx : 0 ≤ x) (hx' : x ≤ 21 / 25) :
Polynomial.eval x LiLiuBuchstabSharp.closureP1 ≤ 56198999999 / 100000000000

Exact positive-coefficient identity on a whole real interval.

Inspect dependencies

LiLiuGoldbachG12BuchstabMajorant.polynomial1_sharp · compiled type and proof/definition references.

source
theorem LiLiuGoldbachG12BuchstabMajorant.polynomial2_sharp {x : ℝ} (hx : 0 ≤ x) (hx' : x ≤ 1 / 1) :
Polynomial.eval x LiLiuBuchstabSharp.closureP2 ≤ 56198999999 / 100000000000

Exact positive-coefficient identity on a whole real interval.

Inspect dependencies

LiLiuGoldbachG12BuchstabMajorant.polynomial2_sharp · compiled type and proof/definition references.