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

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.

Equations

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

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

Get bounds on the Taylor model over its domain: polynomial bound + remainder

Equations

• tm.bound = tm.polyBoundInterval.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.