theorem LiLiuBuchstabSharp.closure_stage1_upper {u : ℝ} (hu : 3 ≤ u) (hu' : u ≤ 4) : rationalStage 1 u ≤ Polynomial.eval (4 - u) closureP1

The explicit polynomial majorizes the actual integral expression on a full unit interval.

theorem LiLiuBuchstabSharp.closure_stage2_upper {u : ℝ} (hu : 4 ≤ u) (hu' : u ≤ 5) : rationalStage 2 u ≤ Polynomial.eval (5 - u) closureP2

The explicit polynomial majorizes the actual integral expression on a full unit interval.

theorem LiLiuBuchstabSharp.closure_stage3_upper {u : ℝ} (hu : 5 ≤ u) (hu' : u ≤ 6) : rationalStage 3 u ≤ Polynomial.eval (6 - u) closureP3

The explicit polynomial majorizes the actual integral expression on a full unit interval.