Computable Bernstein certificates for rational polynomials

Engine/TaylorModel/Core.lean proves that a polynomial on a closed interval lies between the minimum and maximum of its Bernstein coefficients, but states the result over Mathlib's noncomputable Polynomial ℚ. This file evaluates the same enclosure on the executable QPoly representation so it can serve as a Boolean certificate:

• bernsteinCoeffs p I — exact Bernstein coefficients of p on [I.lo, I.hi], obtained by composing p with the affine reparametrisation of [0,1] onto I and converting monomial to Bernstein coefficients;
• bernsteinEnclosure p I — the interval [min bₖ, max bₖ];
• bernsteinCheck cmp p c I depth — a recursive certificate that either proves the comparison from the enclosure on the current box or bisects, up to depth.

Bisection recomputes the coefficients on each child from p (exact, O(n²) per box) so the soundness proof reduces to the one-box enclosure every time. Unlike Horner interval evaluation, the Bernstein enclosure is exact at the endpoints and converges quadratically under bisection, so polynomial bounds that are tight near an endpoint need no subdivision at all.

Affine reparametrisation

def LeanCert.Engine.QPoly.affineMap (I : Core.IntervalRat) : QPoly

The affine map t ↦ I.lo + (I.hi - I.lo) · t sending [0,1] onto I.

Equations

• LeanCert.Engine.QPoly.affineMap I = (LeanCert.Engine.QPoly.constant I.lo).add ((LeanCert.Engine.QPoly.constant (I.hi - I.lo)).mul LeanCert.Engine.QPoly.X)

theorem LeanCert.Engine.QPoly.aeval_affineMap (I : Core.IntervalRat) (t : ℝ) : (Polynomial.aeval t) (affineMap I).toPoly = ↑I.lo + (↑I.hi - ↑I.lo) * t

def LeanCert.Engine.QPoly.shiftedCoeffs (p : QPoly) (I : Core.IntervalRat) : List ℚ

Coefficients of t ↦ p(I.lo + (I.hi - I.lo) t), padded to be nonempty.

Equations

• p.shiftedCoeffs I = match (p.compose (LeanCert.Engine.QPoly.affineMap I)).coeffs.toList with | [] => [0] | c :: cs => c :: cs

theorem LeanCert.Engine.QPoly.shiftedCoeffs_length_pos (p : QPoly) (I : Core.IntervalRat) : 0 < (p.shiftedCoeffs I).length

theorem LeanCert.Engine.QPoly.aeval_shiftedCoeffs (p : QPoly) (I : Core.IntervalRat) (t : ℝ) : (Polynomial.aeval (↑I.lo + (↑I.hi - ↑I.lo) * t)) p.toPoly = ∑ j ∈ Finset.range (p.shiftedCoeffs I).length, ↑((p.shiftedCoeffs I).getD j 0) * t ^ j

Bernstein coefficients and enclosure

def LeanCert.Engine.QPoly.bernsteinCoeffs (p : QPoly) (I : Core.IntervalRat) : List ℚ

Exact Bernstein coefficients of p on I (degree p.coeffs.size - 1).

Equations

• p.bernsteinCoeffs I = LeanCert.Engine.monomialToBernstein (p.shiftedCoeffs I)

theorem LeanCert.Engine.QPoly.bernsteinCoeffs_length (p : QPoly) (I : Core.IntervalRat) : (p.bernsteinCoeffs I).length = (p.shiftedCoeffs I).length

def LeanCert.Engine.QPoly.bernsteinEnclosure (p : QPoly) (I : Core.IntervalRat) : Core.IntervalRat

[min bₖ, max bₖ] over the Bernstein coefficients of p on I.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanCert.Engine.QPoly.aeval_mem_bernsteinEnclosure (p : QPoly) (I : Core.IntervalRat) {x : ℝ} (hx : x ∈ I) : (Polynomial.aeval x) p.toPoly ∈ p.bernsteinEnclosure I

Bernstein enclosure. Every value of p on I lies in bernsteinEnclosure p I.

Recursive certificates

inductive LeanCert.Engine.QPoly.Cmp : Type

The four comparisons certified against an enclosure.

• lower : Cmp
• upper : Cmp
• strictLower : Cmp
• strictUpper : Cmp

@[instance_reducible]

instance LeanCert.Engine.QPoly.instDecidableEqCmp : DecidableEq Cmp

Equations

• LeanCert.Engine.QPoly.instDecidableEqCmp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance LeanCert.Engine.QPoly.instReprCmp : Repr Cmp

Equations

• LeanCert.Engine.QPoly.instReprCmp = { reprPrec := LeanCert.Engine.QPoly.instReprCmp.repr }

def LeanCert.Engine.QPoly.instReprCmp.repr : Cmp → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance LeanCert.Engine.QPoly.instInhabitedCmp : Inhabited Cmp

Equations

• LeanCert.Engine.QPoly.instInhabitedCmp = { default := LeanCert.Engine.QPoly.instInhabitedCmp.default }

def LeanCert.Engine.QPoly.Cmp.holds : Cmp → ℝ → ℝ → Prop

Semantic comparison c ?? y for each Cmp.

Equations

• LeanCert.Engine.QPoly.Cmp.lower.holds x✝¹ x✝ = (x✝¹ ≤ x✝)
• LeanCert.Engine.QPoly.Cmp.upper.holds x✝¹ x✝ = (x✝ ≤ x✝¹)
• LeanCert.Engine.QPoly.Cmp.strictLower.holds x✝¹ x✝ = (x✝¹ < x✝)
• LeanCert.Engine.QPoly.Cmp.strictUpper.holds x✝¹ x✝ = (x✝ < x✝¹)

def LeanCert.Engine.QPoly.Cmp.check : Cmp → Core.IntervalRat → ℚ → Bool

Does the enclosure J prove c ?? y for every y ∈ J?

Equations

• LeanCert.Engine.QPoly.Cmp.lower.check x✝¹ x✝ = decide (x✝ ≤ x✝¹.lo)
• LeanCert.Engine.QPoly.Cmp.upper.check x✝¹ x✝ = decide (x✝¹.hi ≤ x✝)
• LeanCert.Engine.QPoly.Cmp.strictLower.check x✝¹ x✝ = decide (x✝ < x✝¹.lo)
• LeanCert.Engine.QPoly.Cmp.strictUpper.check x✝¹ x✝ = decide (x✝¹.hi < x✝)

theorem LeanCert.Engine.QPoly.Cmp.holds_of_check {cmp : Cmp} {J : Core.IntervalRat} {c : ℚ} (h : cmp.check J c = true) {y : ℝ} (hy : y ∈ J) : cmp.holds (↑c) y

def LeanCert.Engine.QPoly.bernsteinCheck (cmp : Cmp) (p : QPoly) (c : ℚ) (I : Core.IntervalRat) : ℕ → Bool

Recursive Bernstein certificate: prove cmp from the enclosure on I, or bisect and certify both halves, up to depth levels.

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Engine.QPoly.bernsteinCheck cmp p c I 0 = cmp.check (p.bernsteinEnclosure I) c

def LeanCert.Engine.QPoly.bernsteinDepth? (cmp : Cmp) (p : QPoly) (c : ℚ) (I : Core.IntervalRat) (maxDepth : ℕ) : Option ℕ

Least depth at which bernsteinCheck succeeds, if any up to maxDepth. Untrusted search helper used for reporting; certificates re-run the checker.

Equations

• LeanCert.Engine.QPoly.bernsteinDepth? cmp p c I maxDepth = List.find? (fun (depth : ℕ) => LeanCert.Engine.QPoly.bernsteinCheck cmp p c I depth) (List.range (maxDepth + 1))

def LeanCert.Engine.QPoly.bernsteinBoxes (cmp : Cmp) (p : QPoly) (c : ℚ) (I : Core.IntervalRat) : ℕ → ℕ

Number of boxes examined by bernsteinCheck (reporting only).

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Engine.QPoly.bernsteinBoxes cmp p c I 0 = 1

theorem LeanCert.Engine.QPoly.bernsteinCheck_sound {cmp : Cmp} {p : QPoly} {c : ℚ} {I : Core.IntervalRat} {depth : ℕ} (h : bernsteinCheck cmp p c I depth = true) (x : ℝ) : x ∈ I → cmp.holds (↑c) ((Polynomial.aeval x) p.toPoly)

Soundness of the recursive Bernstein certificate.

theorem LeanCert.Engine.QPoly.le_aeval_of_bernsteinCheck {p : QPoly} {c : ℚ} {I : Core.IntervalRat} {depth : ℕ} (h : bernsteinCheck Cmp.lower p c I depth = true) (x : ℝ) : x ∈ I → ↑c ≤ (Polynomial.aeval x) p.toPoly

Lower bounds from a Bernstein certificate.

theorem LeanCert.Engine.QPoly.aeval_le_of_bernsteinCheck {p : QPoly} {c : ℚ} {I : Core.IntervalRat} {depth : ℕ} (h : bernsteinCheck Cmp.upper p c I depth = true) (x : ℝ) : x ∈ I → (Polynomial.aeval x) p.toPoly ≤ ↑c

theorem LeanCert.Engine.QPoly.lt_aeval_of_bernsteinCheck {p : QPoly} {c : ℚ} {I : Core.IntervalRat} {depth : ℕ} (h : bernsteinCheck Cmp.strictLower p c I depth = true) (x : ℝ) : x ∈ I → ↑c < (Polynomial.aeval x) p.toPoly

theorem LeanCert.Engine.QPoly.aeval_lt_of_bernsteinCheck {p : QPoly} {c : ℚ} {I : Core.IntervalRat} {depth : ℕ} (h : bernsteinCheck Cmp.strictUpper p c I depth = true) (x : ℝ) : x ∈ I → (Polynomial.aeval x) p.toPoly < ↑c