Taylor Models - Core Definitions

This file contains the core Taylor model abstraction, polynomial helpers, and basic operations with their correctness proofs.

Main definitions

• TaylorModel - A polynomial plus remainder interval
• evalSet, evalPoly, polyBoundInterval, bound - Evaluation and bounding
• const, identity, add, neg, mul, inv - Basic operations
• evalPoly_mem_polyBoundInterval, taylorModel_correct - Core correctness

Design notes

A Taylor model for f on interval I centered at c is: TM(f) = (P, R) where ∀x ∈ I, f(x) ∈ P(x-c) + R

Operations on Taylor models (add, mul, compose) preserve this property.

Polynomial helpers for Taylor models

noncomputable def LeanCert.Engine.truncPoly (p : Polynomial ℚ) (n : ℕ) : Polynomial ℚ

Truncate a polynomial to terms of degree ≤ n by summing coefficients

Equations

• LeanCert.Engine.truncPoly p n = ∑ i ∈ Finset.range (n + 1), Polynomial.C (p.coeff i) * Polynomial.X ^ i

noncomputable def LeanCert.Engine.tailPoly (p : Polynomial ℚ) (n : ℕ) : Polynomial ℚ

The tail of a polynomial (terms with degree > n)

Equations

• LeanCert.Engine.tailPoly p n = p - LeanCert.Engine.truncPoly p n

noncomputable def LeanCert.Engine.boundPolyAbs (p : Polynomial ℚ) (domain : Core.IntervalRat) (c : ℚ) : ℚ

Bound a polynomial over an interval centered at c. Evaluates at shifted argument: P(x - c) for x ∈ domain.

We bound each term: |aᵢ (x-c)ⁱ| ≤ |aᵢ| * r^i where r = radius of domain from c. Then the total bound is ∑ᵢ |aᵢ| * rⁱ

Equations

• LeanCert.Engine.boundPolyAbs p domain c = ∑ i ∈ Finset.range (p.natDegree + 1), |p.coeff i| * max |domain.hi - c| |domain.lo - c| ^ i

theorem LeanCert.Engine.boundPolyAbs_nonneg (p : Polynomial ℚ) (domain : Core.IntervalRat) (c : ℚ) : 0 ≤ boundPolyAbs p domain c

The bound computed by boundPolyAbs is nonnegative

Bernstein Polynomial Bounds

Bernstein polynomials provide tighter bounds than naive interval arithmetic. For a polynomial P(x) on [a,b], the range is contained in [min bⱼ, max bⱼ] where bⱼ are the Bernstein coefficients.

This avoids the "dependency problem" where naive interval arithmetic gives P(x) = x - x² on [0,1] → [-1, 1] instead of the true [0, 0.25].

def LeanCert.Engine.binomialRat (n k : ℕ) : ℚ

Binomial coefficient as rational (for Bernstein conversion)

Equations

• LeanCert.Engine.binomialRat n k = ↑(n.choose k)

def LeanCert.Engine.transformPolyCoeffs (p : Polynomial ℚ) (α β : ℚ) : List ℚ

Transform polynomial P(u) on [α, β] to Q(t) on [0,1] via u = α + t*(β-α). Returns the coefficients of Q as a list.

If P(u) = Σᵢ aᵢuⁱ, then Q(t) = P(α + t*w) where w = β - α. Using binomial expansion: (α + tw)ⁱ = Σⱼ C(i,j) αⁱ⁻ʲ wʲ tʲ So qⱼ = Σᵢ≥ⱼ aᵢ * C(i,j) * αⁱ⁻ʲ * wʲ

Equations

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

def LeanCert.Engine.monomialToBernstein (coeffs : List ℚ) : List ℚ

Convert monomial coefficients to Bernstein coefficients on [0,1]. For Q(t) = Σⱼ qⱼtʲ, the Bernstein coefficient bₖ = Σⱼ₌₀ᵏ C(k,j)/C(n,j) * qⱼ

Equations

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

def LeanCert.Engine.bernsteinCoeffsForDomain (p : Polynomial ℚ) (lo hi c : ℚ) : List ℚ

Compute Bernstein coefficients for polynomial P evaluated at (x - c) for x ∈ [lo, hi]. The polynomial argument u = x - c ranges over [lo - c, hi - c].

Equations

• LeanCert.Engine.bernsteinCoeffsForDomain p lo hi c = LeanCert.Engine.monomialToBernstein (LeanCert.Engine.transformPolyCoeffs p (lo - c) (hi - c))

def LeanCert.Engine.listMinMax (l : List ℚ) (default : ℚ) : ℚ × ℚ

Find min and max of a non-empty list, returning an interval

Equations

• LeanCert.Engine.listMinMax l default = List.foldl (fun (x : ℚ × ℚ) (x_1 : ℚ) => match x with | (lo, hi) => (min lo x_1, max hi x_1)) (default, default) l

theorem LeanCert.Engine.listMinMax_foldl_le (l : List ℚ) (p : ℚ × ℚ) (hp : p.1 ≤ p.2) : (List.foldl (fun (x : ℚ × ℚ) (x_1 : ℚ) => match x with | (lo, hi) => (min lo x_1, max hi x_1)) p l).1 ≤ (List.foldl (fun (x : ℚ × ℚ) (x_1 : ℚ) => match x with | (lo, hi) => (min lo x_1, max hi x_1)) p l).2

Helper: foldl preserves the invariant lo ≤ hi

theorem LeanCert.Engine.listMinMax_le (l : List ℚ) (d : ℚ) : (listMinMax l d).1 ≤ (listMinMax l d).2

The listMinMax function returns lo ≤ hi

def LeanCert.Engine.boundPolyBernstein (p : Polynomial ℚ) (domain : Core.IntervalRat) (c : ℚ) : Core.IntervalRat

Bound polynomial using Bernstein coefficients - gives [min bⱼ, max bⱼ]. This is typically MUCH tighter than the symmetric [-B, B] from boundPolyAbs.

For P(x) = x - x² on [0,1]: boundPolyAbs gives [-2, 2], Bernstein gives [0, 0.5]

Equations

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

Bernstein proof infrastructure

theorem LeanCert.Engine.boundPolyBernstein_zero_poly (domain : Core.IntervalRat) (c : ℚ) : (boundPolyBernstein 0 domain c).lo ≤ 0 ∧ 0 ≤ (boundPolyBernstein 0 domain c).hi

For the zero polynomial, Bernstein bounds contain zero.

listMinMax bounds

theorem LeanCert.Engine.listMinMax_bounds_elem (l : List ℚ) (d x : ℚ) (hx : x ∈ l) : (listMinMax l d).1 ≤ x ∧ x ≤ (listMinMax l d).2

Elements of a list lie between the listMinMax bounds

theorem LeanCert.Engine.listMinMax_bounds_default (l : List ℚ) (d : ℚ) : (listMinMax l d).1 ≤ d ∧ d ≤ (listMinMax l d).2

The default value lies between the listMinMax bounds

Convex combination bounds

theorem LeanCert.Engine.weighted_sum_le_sup {n : ℕ} (a w : Fin (n + 1) → ℝ) (M : ℝ) (hw_nn : ∀ (k : Fin (n + 1)), 0 ≤ w k) (hw_sum : Finset.univ.sum w = 1) (ha_le : ∀ (k : Fin (n + 1)), a k ≤ M) : ∑ k : Fin (n + 1), a k * w k ≤ M

A weighted sum with non-negative weights summing to 1 is bounded above by the max.

theorem LeanCert.Engine.inf_le_weighted_sum {n : ℕ} (a w : Fin (n + 1) → ℝ) (m : ℝ) (hw_nn : ∀ (k : Fin (n + 1)), 0 ≤ w k) (hw_sum : Finset.univ.sum w = 1) (hm_le : ∀ (k : Fin (n + 1)), m ≤ a k) : m ≤ ∑ k : Fin (n + 1), a k * w k

A weighted sum with non-negative weights summing to 1 is bounded below by the min.

Combinatorial identity

theorem LeanCert.Engine.choose_mul_choose_eq {n k j : ℕ} (hj : j ≤ k) (hk : k ≤ n) : k.choose j * n.choose k = n.choose j * (n - j).choose (k - j)

Key identity: C(k,j) * C(n,k) = C(n,j) * C(n-j, k-j) for j ≤ k ≤ n

Partition of unity for Bernstein basis

theorem LeanCert.Engine.bernstein_partition_of_unity (n : ℕ) (t : ℝ) : ∑ k ∈ Finset.range (n + 1), ↑(n.choose k) * t ^ k * (1 - t) ^ (n - k) = 1

Bernstein basis functions sum to 1 (follows from binomial theorem).

theorem LeanCert.Engine.bernstein_nonneg (n k : ℕ) (t : ℝ) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : 0 ≤ ↑(n.choose k) * t ^ k * (1 - t) ^ (n - k)

Bernstein basis functions are non-negative on [0, 1].

Bernstein representation identity

The key identity: for a polynomial Q(t) = Σⱼ qⱼ tʲ of degree n, with Bernstein coefficients bₖ = Σⱼ≤k C(k,j)/C(n,j) · qⱼ, we have: Q(t) = Σₖ bₖ · C(n,k) · tᵏ · (1-t)^(n-k)

The proof uses: tʲ = Σₖ≥ⱼ C(n-j,k-j) · tᵏ · (1-t)^(n-k) which follows from tʲ · (t + (1-t))^(n-j) = tʲ (binomial theorem).

theorem LeanCert.Engine.monomial_bernstein_expansion (n j : ℕ) (hjn : j ≤ n) (t : ℝ) : t ^ j = ∑ k ∈ Finset.range (n + 1), if j ≤ k then ↑((n - j).choose (k - j)) * t ^ k * (1 - t) ^ (n - k) else 0

The monomial tʲ expanded in Bernstein basis. tʲ · 1 = tʲ · (t + (1-t))^(n-j) = Σₘ C(n-j,m) · t^(m+j) · (1-t)^(n-j-m) = Σₖ≥ⱼ C(n-j,k-j) · tᵏ · (1-t)^(n-k)

The proof follows from the binomial theorem: tʲ · (t + (1-t))^(n-j) = tʲ. Expanding the binomial and reindexing m ↦ k=m+j gives the result.

Main Bernstein enclosure theorem

theorem LeanCert.Engine.poly_eval_mem_boundPolyBernstein (p : Polynomial ℚ) (domain : Core.IntervalRat) (c : ℚ) (x : ℝ) (hx : x ∈ domain) : (Polynomial.aeval (x - ↑c)) p ∈ boundPolyBernstein p domain c

noncomputable def LeanCert.Engine.boundTail (p : Polynomial ℚ) (d : ℕ) (domain : Core.IntervalRat) (c : ℚ) : Core.IntervalRat

Bound the tail of polynomial p (terms with degree > d) when evaluated at (x-c) for x ∈ domain.

Equations

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

Taylor Model structure

structure LeanCert.Engine.TaylorModel : Type

A Taylor model: polynomial approximation with remainder interval.

• poly : Polynomial ℚ

  The polynomial part (coefficients are rationals)

• remainder : Core.IntervalRat

  The remainder interval

• center : ℚ

  The center of expansion

• domain : Core.IntervalRat

  The domain interval

noncomputable def LeanCert.Engine.TaylorModel.evalSet (tm : TaylorModel) (x : ℝ) : Set ℝ

The set of real values this Taylor model can take at point x

Equations

• tm.evalSet x = {y : ℝ | ∃ r ∈ tm.remainder, y = (Polynomial.aeval (x - ↑tm.center)) tm.poly + r}

noncomputable def LeanCert.Engine.TaylorModel.evalPoly (tm : TaylorModel) (x : ℝ) : ℝ

Evaluate polynomial part at a point

Equations

• tm.evalPoly x = (Polynomial.aeval (x - ↑tm.center)) tm.poly

noncomputable def LeanCert.Engine.TaylorModel.polyBoundInterval (tm : TaylorModel) : Core.IntervalRat

Interval bound for the polynomial part over the domain (naive symmetric bound).

Equations

• tm.polyBoundInterval = { lo := -LeanCert.Engine.boundPolyAbs tm.poly tm.domain tm.center, hi := LeanCert.Engine.boundPolyAbs tm.poly tm.domain tm.center, le := ⋯ }

def LeanCert.Engine.TaylorModel.polyBoundIntervalBernstein (tm : TaylorModel) : Core.IntervalRat

Interval bound for the polynomial part using BERNSTEIN bounds (tighter!). For P(x) = x - x² on [0,1]: naive gives [-2, 2], Bernstein gives [0, 0.5]

Equations

• tm.polyBoundIntervalBernstein = LeanCert.Engine.boundPolyBernstein tm.poly tm.domain tm.center

def LeanCert.Engine.TaylorModel.bound (tm : TaylorModel) : Core.IntervalRat

Get bounds on the Taylor model over its domain: polynomial bound + remainder. NOW USES BERNSTEIN BOUNDS for tighter intervals!

Equations

• tm.bound = tm.polyBoundIntervalBernstein.add tm.remainder

def LeanCert.Engine.TaylorModel.boundBernstein (tm : TaylorModel) : Core.IntervalRat

Get bounds using Bernstein polynomial bounds (tighter than naive bound)

Equations

• tm.boundBernstein = tm.polyBoundIntervalBernstein.add tm.remainder

noncomputable def LeanCert.Engine.TaylorModel.valueAtCenterInterval (tm : TaylorModel) : Core.IntervalRat

Interval bound for f(center).

Equations

• tm.valueAtCenterInterval = (LeanCert.Core.IntervalRat.singleton (tm.poly.coeff 0)).add tm.remainder

theorem LeanCert.Engine.TaylorModel.valueAtCenter_correct (tm : TaylorModel) (f : ℝ → ℝ) (hf : ∀ x ∈ tm.domain, f x ∈ tm.evalSet x) (hc : ↑tm.center ∈ tm.domain) : f ↑tm.center ∈ tm.valueAtCenterInterval

Correctness: the true function value at center is in valueAtCenterInterval.

Taylor model operations

noncomputable def LeanCert.Engine.TaylorModel.const (q : ℚ) (domain : Core.IntervalRat) : TaylorModel

Constant Taylor model

Equations

• LeanCert.Engine.TaylorModel.const q domain = { poly := Polynomial.C q, remainder := LeanCert.Core.IntervalRat.singleton 0, center := domain.midpoint, domain := domain }

noncomputable def LeanCert.Engine.TaylorModel.identity (domain : Core.IntervalRat) : TaylorModel

Identity Taylor model: represents the function x ↦ x

Equations

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

noncomputable def LeanCert.Engine.TaylorModel.add (tm1 tm2 : TaylorModel) : TaylorModel

Add two Taylor models

Equations

• tm1.add tm2 = { poly := tm1.poly + tm2.poly, remainder := tm1.remainder.add tm2.remainder, center := tm1.center, domain := tm1.domain }

noncomputable def LeanCert.Engine.TaylorModel.neg (tm : TaylorModel) : TaylorModel

Negate a Taylor model

Equations

• tm.neg = { poly := -tm.poly, remainder := tm.remainder.neg, center := tm.center, domain := tm.domain }

noncomputable def LeanCert.Engine.TaylorModel.sub (tm1 tm2 : TaylorModel) : TaylorModel

Subtract Taylor models

Equations

• tm1.sub tm2 = tm1.add tm2.neg

noncomputable def LeanCert.Engine.TaylorModel.inv (tm : TaylorModel) (hnz : ¬tm.bound.containsZero) : TaylorModel

Invert a Taylor model, assuming its bound does not contain 0.

Equations

• tm.inv hnz = { poly := Polynomial.C 0, remainder := LeanCert.Core.IntervalRat.invNonzero { toIntervalRat := tm.bound, nonzero := hnz }, center := tm.center, domain := tm.domain }

noncomputable def LeanCert.Engine.TaylorModel.mul (tm1 tm2 : TaylorModel) (maxDegree : ℕ) : TaylorModel

Multiply Taylor models with truncation and proper remainder handling.

Equations

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

Core Correctness Theorems

theorem LeanCert.Engine.evalPoly_mem_polyBoundInterval (tm : TaylorModel) (x : ℝ) (hx : x ∈ tm.domain) : tm.evalPoly x ∈ tm.polyBoundInterval

Key lemma: polynomial evaluation is bounded by polyBoundInterval.

theorem LeanCert.Engine.taylorModel_correct (tm : TaylorModel) (f : ℝ → ℝ) (hf : ∀ x ∈ tm.domain, f x ∈ tm.evalSet x) (x : ℝ) : x ∈ tm.domain → f x ∈ tm.bound

Taylor model bounds are correct: if f(x) ∈ evalSet for all x in domain, then f(x) ∈ bound for all x in domain.

Local evalSet correctness lemmas

theorem LeanCert.Engine.TaylorModel.const_evalSet_correct (q : ℚ) (domain : Core.IntervalRat) (x : ℝ) : x ∈ domain → ↑q ∈ (const q domain).evalSet x

Constant TM correctness for evalSet: q ∈ const(q).evalSet x.

theorem LeanCert.Engine.TaylorModel.identity_evalSet_correct (domain : Core.IntervalRat) (x : ℝ) : x ∈ domain → x ∈ (identity domain).evalSet x

Identity TM correctness for evalSet: x ∈ identity.evalSet x.

theorem LeanCert.Engine.TaylorModel.neg_evalSet_of_mem {tm : TaylorModel} {x r : ℝ} (hr : r ∈ tm.remainder) : -(tm.evalPoly x + r) ∈ tm.neg.evalSet x

Negation preserves evalSet membership.

theorem LeanCert.Engine.TaylorModel.evalSet_of_remainder (tm : TaylorModel) (x : ℝ) {r : ℝ} (hr : r ∈ tm.remainder) : tm.evalPoly x + r ∈ tm.evalSet x

Convenience: any evalPoly x + r with r ∈ remainder lies in evalSet.

theorem LeanCert.Engine.TaylorModel.add_evalSet_of_mem {tm1 tm2 : TaylorModel} {x : ℝ} (hcenter : tm1.center = tm2.center) {v1 v2 : ℝ} (hv1 : v1 ∈ tm1.evalSet x) (hv2 : v2 ∈ tm2.evalSet x) : v1 + v2 ∈ (tm1.add tm2).evalSet x

Addition preserves evalSet membership when centers match.

Polynomial helper lemmas for multiplication

theorem LeanCert.Engine.truncPoly_add_tailPoly (p : Polynomial ℚ) (n : ℕ) : truncPoly p n + tailPoly p n = p

truncPoly + tailPoly = original polynomial

theorem LeanCert.Engine.aeval_eq_truncPoly_add_tailPoly (p : Polynomial ℚ) (n : ℕ) (y : ℝ) : (Polynomial.aeval y) p = (Polynomial.aeval y) (truncPoly p n) + (Polynomial.aeval y) (tailPoly p n)

aeval distributes over truncPoly + tailPoly

theorem LeanCert.Engine.tailPoly_eval_bounded (p : Polynomial ℚ) (n : ℕ) (domain : Core.IntervalRat) (c : ℚ) (x : ℝ) (hx : x ∈ domain) : |(Polynomial.aeval (x - ↑c)) (tailPoly p n)| ≤ ↑(boundPolyAbs (tailPoly p n) domain c)

Tail polynomial evaluation is bounded by boundPolyAbs of tail.

theorem LeanCert.Engine.poly_eval_bounded (p : Polynomial ℚ) (domain : Core.IntervalRat) (c : ℚ) (x : ℝ) (hx : x ∈ domain) : |(Polynomial.aeval (x - ↑c)) p| ≤ ↑(boundPolyAbs p domain c)

Polynomial bound lemma: |P(y)| ≤ boundPolyAbs P domain c for y = x - c, x ∈ domain

theorem LeanCert.Engine.mem_symmetric_interval_of_abs_le {x : ℝ} {B : ℚ} (hB : 0 ≤ B) (h : |x| ≤ ↑B) : x ∈ { lo := -B, hi := B, le := ⋯ }

Value in symmetric interval from absolute bound

Generic Taylor model algebra lemmas

These lemmas are pure TM algebra that don't depend on Expr or transcendentals.

theorem LeanCert.Engine.TaylorModel.ne_zero_of_mem_nonzero_bound {x : ℝ} {I : Core.IntervalRat} (hx : x ∈ I) (hnz : ¬I.containsZero) : x ≠ 0

If x ∈ bound and bound doesn't contain zero, then x ≠ 0.

theorem LeanCert.Engine.TaylorModel.foil_to_trunc_remainder {p1 p2 : Polynomial ℚ} {r1 r2 y : ℝ} {degree : ℕ} (hsplit : (Polynomial.aeval y) (p1 * p2) = (Polynomial.aeval y) (truncPoly (p1 * p2) degree) + (Polynomial.aeval y) (tailPoly (p1 * p2) degree)) : ((Polynomial.aeval y) p1 + r1) * ((Polynomial.aeval y) p2 + r2) = (Polynomial.aeval y) (truncPoly (p1 * p2) degree) + ((Polynomial.aeval y) (tailPoly (p1 * p2) degree) + (Polynomial.aeval y) p1 * r2 + (Polynomial.aeval y) p2 * r1 + r1 * r2)

FOIL expansion for Taylor model multiplication. (P₁ + r₁)(P₂ + r₂) = trunc(P₁P₂) + [tail(P₁P₂) + P₁r₂ + P₂r₁ + r₁r₂]

theorem LeanCert.Engine.TaylorModel.remainder_four_terms_mem {v_tail v_p1r2 v_p2r1 v_r1r2 : ℝ} {I_tail I_p1r2 I_p2r1 I_r1r2 : Core.IntervalRat} (htail : v_tail ∈ I_tail) (hp1r2 : v_p1r2 ∈ I_p1r2) (hp2r1 : v_p2r1 ∈ I_p2r1) (hr1r2 : v_r1r2 ∈ I_r1r2) : v_tail + v_p1r2 + v_p2r1 + v_r1r2 ∈ I_tail.add (I_p1r2.add (I_p2r1.add I_r1r2))

Four-term remainder membership: tail + p1r2 + p2r1 + r1r2 ∈ totalRemainder. This extracts the nested interval addition pattern from mul_evalSet_correct.

theorem LeanCert.Engine.TaylorModel.mul_evalSet_correct (f₁ f₂ : ℝ → ℝ) (tm1 tm2 : TaylorModel) (degree : ℕ) (hcenter : tm1.center = tm2.center) (hdomain : tm1.domain = tm2.domain) (hf1 : ∀ x ∈ tm1.domain, f₁ x ∈ tm1.evalSet x) (hf2 : ∀ x ∈ tm2.domain, f₂ x ∈ tm2.evalSet x) (x : ℝ) : x ∈ tm1.domain → f₁ x * f₂ x ∈ (tm1.mul tm2 degree).evalSet x

Multiplication preserves evalSet membership.

Given:

• f₁(x) ∈ tm1.evalSet x (i.e., f₁(x) = P₁(y) + r₁ with r₁ ∈ tm1.remainder)
• f₂(x) ∈ tm2.evalSet x (i.e., f₂(x) = P₂(y) + r₂ with r₂ ∈ tm2.remainder)

Then f₁(x) * f₂(x) ∈ (TaylorModel.mul tm1 tm2 degree).evalSet x.

The expansion is: (P₁ + r₁)(P₂ + r₂) = P₁P₂ + P₁r₂ + P₂r₁ + r₁r₂ = trunc(P₁P₂) + [tail(P₁P₂) + P₁r₂ + P₂r₁ + r₁r₂]

theorem LeanCert.Engine.TaylorModel.inv_evalSet_correct (f : ℝ → ℝ) (tm : TaylorModel) (hnz : ¬tm.bound.containsZero) (hf : ∀ x ∈ tm.domain, f x ∈ tm.evalSet x) (x : ℝ) : x ∈ tm.domain → (f x)⁻¹ ∈ (tm.inv hnz).evalSet x

Inversion preserves evalSet membership (conservative construction).

Since TaylorModel.inv uses poly = 0 and remainder = invBound, we show that if f(x) ∈ tm.evalSet x for all x in domain, then f(x)⁻¹ ∈ (inv tm hnz).evalSet x.