Generic Taylor Series Abstractions

This file provides generic Taylor series machinery for verified numerics. We wrap Mathlib's Taylor expansion theorems in forms convenient for our interval arithmetic framework.

Phase Status

This module is now Phase 3 complete. The main Taylor remainder bound theorem taylor_remainder_bound is fully proved with no sorry markers.

The theorem provides rigorous bounds on Taylor polynomial approximation errors using Lagrange's form of the remainder.

Main definitions

• TaylorApprox - A Taylor approximation with explicit remainder bounds
• Generic theorems for composing Taylor approximations

Design notes

This file provides the abstract theory. Specific Taylor expansions for exp, sin, cos, etc. are built using this machinery in conjunction with Mathlib's calculus lemmas.

Taylor approximation structure

structure LeanCert.Core.TaylorApprox : Type

A Taylor approximation of a function on an interval.

Given a function f, center c, and radius r, this represents:

• A polynomial approximation poly of degree n
• A remainder bound R such that for all x with |x - c| ≤ r: |f(x) - poly(x - c)| ≤ R

• degree : ℕ

  Degree of the polynomial

• coeffs : Fin (self.degree + 1) → ℚ

  Polynomial coefficients (Taylor coefficients at center)

• remainder : ℚ

  Remainder bound

• remainder_nonneg : 0 ≤ self.remainder

  The remainder is non-negative

noncomputable def LeanCert.Core.TaylorApprox.evalPoly (ta : TaylorApprox) (x : ℝ) : ℝ

Evaluate the polynomial part at a point

Equations

• ta.evalPoly x = ∑ i : Fin (ta.degree + 1), ↑(ta.coeffs i) * x ^ ↑i

Derivative bounds

structure LeanCert.Core.DerivBound : Type

A bound on the n-th derivative of a function on an interval

• order : ℕ

  The derivative order

• bound : ℚ

  Upper bound on |f^(n)(x)| for x in the interval

• bound_nonneg : 0 ≤ self.bound

  The bound is non-negative

Taylor remainder bounds

Helper lemmas for iteratedDerivWithin conversion

theorem LeanCert.Core.uniqueDiffWithinAt_Icc_left {c x : ℝ} (hcx : c < x) : UniqueDiffWithinAt ℝ (Set.Icc c x) c

Unique differentiability at the left endpoint of a closed interval.

theorem LeanCert.Core.uniqueDiffWithinAt_Icc_right {c x : ℝ} (hcx : c < x) : UniqueDiffWithinAt ℝ (Set.Icc c x) x

Unique differentiability at the right endpoint of a closed interval.

theorem LeanCert.Core.derivWithin_Icc_left_eq_deriv {f : ℝ → ℝ} {c x : ℝ} (hcx : c < x) (hf : DifferentiableAt ℝ f c) : derivWithin f (Set.Icc c x) c = deriv f c

At the left endpoint of [c, x], derivWithin equals deriv for differentiable functions.

theorem LeanCert.Core.derivWithin_Icc_right_eq_deriv {f : ℝ → ℝ} {c x : ℝ} (hcx : c < x) (hf : DifferentiableAt ℝ f x) : derivWithin f (Set.Icc c x) x = deriv f x

At the right endpoint of [c, x], derivWithin equals deriv for differentiable functions.

theorem LeanCert.Core.iteratedDerivWithin_Icc_interior_eq {f : ℝ → ℝ} {a b x : ℝ} {n : ℕ} (_hab : a < b) (hx : x ∈ Set.Ioo a b) : iteratedDerivWithin n f (Set.Icc a b) x = iteratedDeriv n f x

Helper lemma: iteratedDerivWithin on Icc a b equals iteratedDeriv at interior points.

This bridges Mathlib's iteratedDerivWithin-based Taylor theorems with global iteratedDeriv.

theorem LeanCert.Core.iteratedDerivWithin_Icc_left_eq_iteratedDeriv {f : ℝ → ℝ} {c x : ℝ} {n : ℕ} (hcx : c < x) (hf : ContDiff ℝ (↑n) f) : iteratedDerivWithin n f (Set.Icc c x) c = iteratedDeriv n f c

At the left endpoint of [c, x], iteratedDerivWithin equals iteratedDeriv for ContDiff functions.

theorem LeanCert.Core.iteratedDerivWithin_Icc_left_eq_iteratedDeriv_of_isOpen {f : ℝ → ℝ} {c x : ℝ} {n : ℕ} {U : Set ℝ} (hU_open : IsOpen U) (hcU : c ∈ U) (hcx : c < x) (hI_sub : Set.Icc c x ⊆ U) (hf : ContDiffOn ℝ (↑n) f U) : iteratedDerivWithin n f (Set.Icc c x) c = iteratedDeriv n f c

At the left endpoint of [c, x], iteratedDerivWithin equals iteratedDeriv for functions that are ContDiffOn on an open set containing c.

This is useful for functions like log that are only smooth on (0, ∞).

theorem LeanCert.Core.taylor_remainder_bound_on_c_lt_x {f : ℝ → ℝ} {a b c : ℝ} {m : ℕ} {M : ℝ} {U : Set ℝ} (hU_open : IsOpen U) (hI_sub : Set.Icc a b ⊆ U) (hca : a ≤ c) (hf : ContDiffOn ℝ (↑m + 1) f U) (hM : ∀ y ∈ Set.Icc a b, ‖iteratedDeriv (m + 1) f y‖ ≤ M) (x : ℝ) (hx : x ∈ Set.Icc a b) (hcx : c < x) : ‖f x - ∑ i ∈ Finset.range (m + 1), iteratedDeriv i f c / ↑i.factorial * (x - c) ^ i‖ ≤ M * |x - c| ^ (m + 1) / ↑(m + 1).factorial

Taylor remainder bound for c < x case with ContDiffOn hypothesis.

For functions that are ContDiffOn on an open set containing [a, b], this provides the same Lagrange remainder bound as the global ContDiff version.

theorem LeanCert.Core.iteratedDeriv_reflect_of_contDiffOn {f : ℝ → ℝ} {c : ℝ} {n : ℕ} {U : Set ℝ} (hU_open : IsOpen U) (hf : ContDiffOn ℝ (↑n) f U) (t : ℝ) (ht : 2 * c - t ∈ U) : iteratedDeriv n (fun (s : ℝ) => f (2 * c - s)) t = (-1) ^ n * iteratedDeriv n f (2 * c - t)

Key lemma for reflection: derivatives of g(t) = f(2c - t) when f is smooth on an open set.

This is a local version of iteratedDeriv_reflect that works with ContDiffOn on an open set rather than global ContDiff.

theorem LeanCert.Core.taylor_remainder_bound_on_x_lt_c {f : ℝ → ℝ} {a b c : ℝ} {m : ℕ} {M : ℝ} {U : Set ℝ} (hU_open : IsOpen U) (hI_sub : Set.Icc a b ⊆ U) (hcb : c ≤ b) (hf : ContDiffOn ℝ (↑m + 1) f U) (hM : ∀ y ∈ Set.Icc a b, ‖iteratedDeriv (m + 1) f y‖ ≤ M) (x : ℝ) (hx : x ∈ Set.Icc a b) (hxc : x < c) : ‖f x - ∑ i ∈ Finset.range (m + 1), iteratedDeriv i f c / ↑i.factorial * (x - c) ^ i‖ ≤ M * |x - c| ^ (m + 1) / ↑(m + 1).factorial

Taylor remainder bound for x < c case with ContDiffOn hypothesis.

For functions that are ContDiffOn on an open set containing [a, b], this provides the same Lagrange remainder bound as the global ContDiff version.

The proof uses reflection: define g(t) = f(2c - t), apply Lagrange to g on [c, 2c-x], then convert back.

theorem LeanCert.Core.taylor_remainder_bound_on {f : ℝ → ℝ} {a b c : ℝ} {n : ℕ} {M : ℝ} {U : Set ℝ} (hU_open : IsOpen U) (hI_sub : Set.Icc a b ⊆ U) (hca : a ≤ c) (hcb : c ≤ b) (hf : ContDiffOn ℝ (↑n) f U) (hM : ∀ x ∈ Set.Icc a b, ‖iteratedDeriv n f x‖ ≤ M) (_hMnonneg : 0 ≤ M) (x : ℝ) : x ∈ Set.Icc a b → ‖f x - ∑ i ∈ Finset.range n, iteratedDeriv i f c / ↑i.factorial * (x - c) ^ i‖ ≤ M * |x - c| ^ n / ↑n.factorial

Combined Taylor remainder bound with ContDiffOn hypothesis.

For functions that are ContDiffOn on an open set containing [a, b], this provides the Lagrange remainder bound for any x ∈ [a, b] and center c ∈ [a, b].

theorem LeanCert.Core.iteratedDeriv_reflect {f : ℝ → ℝ} {c : ℝ} {n : ℕ} (hf : ContDiff ℝ (↑n) f) (t : ℝ) : iteratedDeriv n (fun (s : ℝ) => f (2 * c - s)) t = (-1) ^ n * iteratedDeriv n f (2 * c - t)

Key lemma: derivatives of reflected function g(t) = f(2c - t).

For the x < c case, we use reflection: define g(t) = f(2c - t), apply Lagrange to g on [c, 2c-x], then convert back. This lemma shows how g's derivatives relate to f's derivatives.

theorem LeanCert.Core.neg_one_pow_mul_self (n : ℕ) : (-1) ^ n * (-1) ^ n = 1

Auxiliary lemma: (-1)^n * (-1)^n = 1 for any natural n.

theorem LeanCert.Core.taylor_remainder_bound_c_lt_x {f : ℝ → ℝ} {a b c : ℝ} {m : ℕ} {M : ℝ} (hca : a ≤ c) (hf : ContDiff ℝ (↑m + 1) f) (hM : ∀ y ∈ Set.Icc a b, ‖iteratedDeriv (m + 1) f y‖ ≤ M) (x : ℝ) (hx : x ∈ Set.Icc a b) (hcx : c < x) : ‖f x - ∑ i ∈ Finset.range (m + 1), iteratedDeriv i f c / ↑i.factorial * (x - c) ^ i‖ ≤ M * |x - c| ^ (m + 1) / ↑(m + 1).factorial

Taylor remainder bound for c < x case (Lagrange form).

For c < x, we apply taylor_mean_remainder_lagrange on [c, x] and convert iteratedDerivWithin to iteratedDeriv using the helper lemmas above.

theorem LeanCert.Core.taylor_remainder_bound_x_lt_c {f : ℝ → ℝ} {a b c : ℝ} {m : ℕ} {M : ℝ} (hcb : c ≤ b) (hf : ContDiff ℝ (↑m + 1) f) (hM : ∀ y ∈ Set.Icc a b, ‖iteratedDeriv (m + 1) f y‖ ≤ M) (x : ℝ) (hx : x ∈ Set.Icc a b) (hxc : x < c) : ‖f x - ∑ i ∈ Finset.range (m + 1), iteratedDeriv i f c / ↑i.factorial * (x - c) ^ i‖ ≤ M * |x - c| ^ (m + 1) / ↑(m + 1).factorial

Taylor remainder bound for x < c case (Lagrange form via reflection).

For x < c, we define g(t) = f(2c - t), apply taylor_mean_remainder_lagrange on [c, 2c-x], then use iteratedDeriv_reflect to convert back to f's derivatives. The key insight is that g's Taylor expansion at c, evaluated at 2c-x, equals f's Taylor expansion at c, evaluated at x, because the (-1)^i factors from the derivatives cancel with the (-1)^i factors from the powers.

theorem LeanCert.Core.taylor_remainder_bound {f : ℝ → ℝ} {a b c : ℝ} {n : ℕ} {M : ℝ} (_hab : a ≤ b) (hca : a ≤ c) (hcb : c ≤ b) (hf : ContDiff ℝ (↑n) f) (hM : ∀ x ∈ Set.Icc a b, ‖iteratedDeriv n f x‖ ≤ M) (_hMnonneg : 0 ≤ M) (x : ℝ) : x ∈ Set.Icc a b → ‖f x - ∑ i ∈ Finset.range n, iteratedDeriv i f c / ↑i.factorial * (x - c) ^ i‖ ≤ M * |x - c| ^ n / ↑n.factorial

Lagrange form remainder bound for Taylor approximation.

If |f^(n)(x)| ≤ M for all x in [a, b], and c ∈ [a, b], then the Taylor polynomial of degree n-1 (sum over range n) satisfies: for any x ∈ [a, b]: |f(x) - T_{n-1}(x; c)| ≤ M * |x - c|^n / n!

Note: The sum ∑ i ∈ Finset.range n gives terms 0..n-1 (degree n-1 polynomial). The remainder involves the n-th derivative, matching our bound on iteratedDeriv n f.

All cases are fully proved:

• Case n = 0: Direct bound. ✓
• Case n > 0, x = c: Trivial (both sides zero). ✓
• Case n > 0, c < x: Via taylor_remainder_bound_c_lt_x. ✓
• Case n > 0, x < c: Via taylor_remainder_bound_x_lt_c (reflection). ✓

Common Taylor expansions

def LeanCert.Core.expTaylorCoeff (n : ℕ) : ℚ

Taylor coefficients for exp at 0: 1/n!

Equations

• LeanCert.Core.expTaylorCoeff n = 1 / ↑n.factorial

def LeanCert.Core.sinTaylorCoeff (n : ℕ) : ℚ

Taylor coefficients for sin at 0

Equations

• LeanCert.Core.sinTaylorCoeff n = if n % 2 = 0 then 0 else if n / 2 % 2 = 0 then 1 / ↑n.factorial else -1 / ↑n.factorial

def LeanCert.Core.cosTaylorCoeff (n : ℕ) : ℚ

Taylor coefficients for cos at 0

Equations

• LeanCert.Core.cosTaylorCoeff n = if n % 2 = 1 then 0 else if n / 2 % 2 = 0 then 1 / ↑n.factorial else -1 / ↑n.factorial

Derivative bounds for common functions

theorem LeanCert.Core.exp_deriv_bound {a b : ℝ} (_hab : a ≤ b) (n : ℕ) (x : ℝ) : x ∈ Set.Icc a b → ‖iteratedDeriv n Real.exp x‖ ≤ Real.exp b

All derivatives of exp are bounded by exp on any bounded interval

theorem LeanCert.Core.sin_cos_deriv_bound (n : ℕ) (x : ℝ) : ‖iteratedDeriv n Real.sin x‖ ≤ 1 ∧ ‖iteratedDeriv n Real.cos x‖ ≤ 1

All derivatives of sin and cos are bounded by 1. The derivatives cycle: sin → cos → -sin → -cos → sin → ...

theorem LeanCert.Core.cosh_le_exp_abs (x : ℝ) : Real.cosh x ≤ Real.exp |x|

cosh x ≤ exp |x| for all x

theorem LeanCert.Core.abs_sinh_le_cosh (x : ℝ) : |Real.sinh x| ≤ Real.cosh x

|sinh x| ≤ cosh x for all x

theorem LeanCert.Core.sinh_cosh_deriv_bound {a b : ℝ} (_hab : a ≤ b) (n : ℕ) (x : ℝ) : x ∈ Set.Icc a b → ‖iteratedDeriv n Real.sinh x‖ ≤ Real.exp (max |a| |b|) ∧ ‖iteratedDeriv n Real.cosh x‖ ≤ Real.exp (max |a| |b|)

All derivatives of sinh and cosh are bounded by exp(max(|a|, |b|)) on [a, b]. The derivatives cycle: sinh → cosh → sinh → cosh → ...

theorem LeanCert.Core.iteratedDeriv_log {n : ℕ} (hn : n ≠ 0) {x : ℝ} (hx : 0 < x) : iteratedDeriv n Real.log x = (-1) ^ (n - 1) * ↑(n - 1).factorial * x ^ (-↑n)