theorem LiLiuBuchstabSharp.closure_polynomial2_sharp {x : ℝ} (hx : 0 ≤ x) (hx' : x ≤ 3 / 4) : Polynomial.eval x closureP2 ≤ 56152199999 / 100000000000

Exact positive-coefficient decomposition on the whole interval; no sampled values.

theorem LiLiuBuchstabSharp.closure_polynomial3_sharp {x : ℝ} (hx : 0 ≤ x) (hx' : x ≤ 1 / 4) : Polynomial.eval (1 - x) closureP3 ≤ 56152199999 / 100000000000

Exact positive-coefficient decomposition on the whole interval; no sampled values.

theorem LiLiuBuchstabSharp.rationalStage_two_sharp {u : ℝ} (hu : 17 / 4 ≤ u) (hu' : u ≤ 5) : rationalStage 2 u ≤ 56152199999 / 100000000000

First missing expression bound, unconditional on the complete requested interval.

theorem LiLiuBuchstabSharp.rationalStage_three_sharp {u : ℝ} (hu : 5 ≤ u) (hu' : u ≤ 21 / 4) : rationalStage 3 u ≤ 56152199999 / 100000000000

Second missing expression bound, unconditional on the complete requested interval.