Taylor Models - Special Functions

This file contains Taylor polynomial definitions and remainder bounds for special functions (erf, and future sqrt), along with function-level Taylor models.

Main definitions

• erfTaylorPoly - Taylor polynomial for erf
• erfRemainderBound - Remainder bound for erf
• tmErf - Function-level Taylor model for erf

erf Taylor polynomial

erf(x) = (2/√π) ∫₀ˣ e^{-t²} dt = (2/√π) Σ_{n=0}^∞ (-1)^n x^{2n+1} / (n! (2n+1)) = (2/√π) (x - x³/3 + x⁵/10 - x⁷/42 + ...)

We use rational approximations for 2/√π ≈ 1.128379...

def LeanCert.Engine.TaylorModel.erfCoeff_lo : ℚ

Rational approximation of 2/√π (lower bound)

Equations

• LeanCert.Engine.TaylorModel.erfCoeff_lo = 1128 / 1000

def LeanCert.Engine.TaylorModel.erfCoeff_hi : ℚ

Rational approximation of 2/√π (upper bound)

Equations

• LeanCert.Engine.TaylorModel.erfCoeff_hi = 1129 / 1000

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

Taylor polynomial coefficients for erf at center 0 (using middle approximation): erf(x) ≈ (2/√π) Σ (-1)^k x^{2k+1} / (k! (2k+1))

Equations

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

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

Taylor polynomial for erf of degree n

Equations

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

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

Remainder bound for erf: |erf(x)| ≤ 1 for all x, so we use Taylor remainder plus coefficient approximation error.

Equations

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

theorem LeanCert.Engine.TaylorModel.erfRemainderBound_nonneg (domain : Core.IntervalRat) (n : ℕ) : 0 ≤ erfRemainderBound domain n

Remainder bound for erf is nonnegative

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

Taylor model for erf z on domain J, centered at 0, degree n. erf(z) = (2/√π) ∫₀ᶻ e^{-t²} dt.

Equations

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

Future: sqrt Taylor model

sqrt(x) requires special treatment since it's not analytic at 0. It needs to be expanded around a positive center c > 0.

For now, we leave a placeholder comment.