Taylor Models - Exponential and Logarithmic Functions

This file contains Taylor polynomial definitions and remainder bounds for exp and log functions, along with function-level Taylor models and their correctness proofs.

Main definitions

• expTaylorPoly, logTaylorPolyAtCenter - Taylor polynomials
• expRemainderBound, logRemainderBound - Remainder bounds
• tmExp, tmLog - Function-level Taylor models
• tmExp_correct, tmLog_correct - Correctness theorems

exp Taylor polynomial

noncomputable def LeanCert.Engine.TaylorModel.expTaylorPoly (n : ℕ) : Polynomial ℚ

Taylor polynomial for exp of degree n: ∑_{i=0}^n x^i / i!

Equations

• LeanCert.Engine.TaylorModel.expTaylorPoly n = ∑ i ∈ Finset.range (n + 1), Polynomial.C (1 / ↑i.factorial) * Polynomial.X ^ i

noncomputable def LeanCert.Engine.TaylorModel.expRemainderBound (domain : Core.IntervalRat) (n : ℕ) : ℚ

Remainder bound for exp Taylor series. The Lagrange remainder is exp(ξ) * x^{n+1} / (n+1)! where ξ is between 0 and x. We use e < 3, so e^r ≤ 3^(⌈r⌉+1) as a conservative bound.

Equations

• LeanCert.Engine.TaylorModel.expRemainderBound domain n = 3 ^ (⌈max |domain.lo| |domain.hi|⌉₊ + 1) * max |domain.lo| |domain.hi| ^ (n + 1) / ↑(n + 1).factorial

theorem LeanCert.Engine.TaylorModel.expRemainderBound_nonneg (domain : Core.IntervalRat) (n : ℕ) : 0 ≤ expRemainderBound domain n

Remainder bound for exp is nonnegative

noncomputable def LeanCert.Engine.TaylorModel.tmExp (J : Core.IntervalRat) (n : ℕ) : TaylorModel

Taylor model for exp z on domain J, centered at 0, degree n. This represents the function z ↦ exp(z) directly.

Equations

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

log Taylor polynomial

log(x) at center c > 0: log(x) = log(c) + Σ_{k=1}^n [(-1)^(k+1) / (k * c^k)] * (x - c)^k + R_n(x)

The constant term log(c) is transcendental, so we:

1. Approximate log(c) with a rational q using interval bounds
2. Add the approximation error to the remainder

The Lagrange remainder is: R_n(x) = (-1)^n / [(n+1) * ξ^(n+1)] * (x-c)^(n+1) where ξ is between x and c. For positive domain, |R_n| ≤ r^(n+1) / [(n+1) * min_domain^(n+1)].

noncomputable def LeanCert.Engine.TaylorModel.logTaylorCoeffs (c : ℚ) (n : ℕ) : ℕ → ℚ

Taylor polynomial coefficients for log at center c > 0: log(x) = log(c) + (1/c)(x-c) - (1/2c²)(x-c)² + (1/3c³)(x-c)³ - ... For k ≥ 1: coeff_k = (-1)^(k+1) / (k * c^k) For k = 0: we handle the transcendental log(c) separately in tmLog.

Equations

• LeanCert.Engine.TaylorModel.logTaylorCoeffs c n i = if i = 0 then 0 else if i ≤ n then (-1) ^ (i + 1) / (↑i * c ^ i) else 0

noncomputable def LeanCert.Engine.TaylorModel.logTaylorPolyAtCenter (c : ℚ) (n : ℕ) : Polynomial ℚ

Taylor polynomial for log at center c > 0 (without the log(c) constant term). The constant term is added as a rational approximation in tmLog.

Equations

• LeanCert.Engine.TaylorModel.logTaylorPolyAtCenter c n = ∑ i ∈ Finset.range (n + 1), Polynomial.C (LeanCert.Engine.TaylorModel.logTaylorCoeffs c n i) * Polynomial.X ^ i

noncomputable def LeanCert.Engine.TaylorModel.logLagrangeRemainder (domain : Core.IntervalRat) (c : ℚ) (n : ℕ) : ℚ

Lagrange remainder bound for log at center c > 0. |R_n(x)| ≤ r^(n+1) / [(n+1) * min_ξ^(n+1)] where r = max(|lo - c|, |hi - c|) and min_ξ = min(lo, c) for positive domain. Since domain ⊂ (0, ∞) and c is the midpoint, we use domain.lo as min_ξ.

Equations

• LeanCert.Engine.TaylorModel.logLagrangeRemainder domain c n = if domain.lo ≤ 0 then 1000 else max |domain.lo - c| |domain.hi - c| ^ (n + 1) / ((↑n + 1) * domain.lo ^ (n + 1))

noncomputable def LeanCert.Engine.TaylorModel.logRemainderBound (domain : Core.IntervalRat) (c : ℚ) (n : ℕ) (logc_error : ℚ) : ℚ

Total remainder bound for log: Lagrange remainder + approximation error for log(c).

Equations

• LeanCert.Engine.TaylorModel.logRemainderBound domain c n logc_error = LeanCert.Engine.TaylorModel.logLagrangeRemainder domain c n + logc_error

theorem LeanCert.Engine.TaylorModel.logRemainderBound_nonneg (domain : Core.IntervalRat) (c : ℚ) (n : ℕ) (logc_error : ℚ) (_hc : c > 0) (herr : logc_error ≥ 0) (hdom : domain.lo > 0) : 0 ≤ logRemainderBound domain c n logc_error

Remainder bound for log is nonnegative (when domain is positive).

noncomputable def LeanCert.Engine.TaylorModel.tmLog (J : Core.IntervalRat) (n : ℕ) : Option TaylorModel

Taylor model for log z on domain J, centered at c = midpoint. Returns None if the domain is not strictly positive.

This handles the transcendental log(c) by:

1. Computing rational bounds [lo, hi] for log(c)
2. Using midpoint = (lo + hi) / 2 as the polynomial constant
3. Adding error = (hi - lo) / 2 to the remainder

Equations

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

Helper lemmas

Correctness theorems

theorem LeanCert.Engine.TaylorModel.expTaylorPoly_aeval_eq (n : ℕ) (z : ℝ) : (Polynomial.aeval z) (expTaylorPoly n) = ∑ i ∈ Finset.range (n + 1), iteratedDeriv i Real.exp 0 / ↑i.factorial * z ^ i

expTaylorPoly evaluates to the standard Taylor sum for exp at 0. This connects our rational polynomial to Mathlib's Taylor series.

theorem LeanCert.Engine.TaylorModel.tmExp_correct (J : Core.IntervalRat) (n : ℕ) (z : ℝ) : z ∈ J → Real.exp z ∈ (tmExp J n).evalSet z

exp z ∈ (tmExp J n).evalSet z for all z in J. Uses taylor_remainder_bound with f = Real.exp, M = exp(max of interval).

theorem LeanCert.Engine.TaylorModel.log_approx_error_bound {c : ℚ} (hc_pos : 0 < c) : have c_interval := let __IntervalRat := Core.IntervalRat.singleton c; { toIntervalRat := __IntervalRat, lo_pos := ⋯ }; have logc_interval := Core.IntervalRat.logInterval c_interval; have logc_approx := logc_interval.midpoint; have logc_error := logc_interval.width / 2; |Real.log ↑c - ↑logc_approx| ≤ ↑logc_error

Helper lemma: log(c) is within logc_error of logc_approx when logc_interval is computed from logInterval applied to a singleton interval containing c.

theorem LeanCert.Engine.TaylorModel.log_taylor_remainder_bound' (J : Core.IntervalRat) (c : ℚ) (n : ℕ) (z : ℝ) (hpos : J.lo > 0) (hc_lo : ↑J.lo ≤ ↑c) (hc_hi : ↑c ≤ ↑J.hi) (hz : z ∈ J) : |Real.log z - Real.log ↑c - (Polynomial.aeval (z - ↑c)) (logTaylorPolyAtCenter c n)| ≤ ↑(logLagrangeRemainder J c n)

The Taylor remainder for log at center c is bounded by the Lagrange form.

theorem LeanCert.Engine.TaylorModel.tmLog_correct (J : Core.IntervalRat) (n : ℕ) (tm : TaylorModel) (h : tmLog J n = some tm) (z : ℝ) : z ∈ J → Real.log z ∈ tm.evalSet z

log z ∈ (tmLog J n).evalSet z for all z in J when J.lo > 0.