Taylor Models - Hyperbolic Functions

This file contains Taylor polynomial definitions and remainder bounds for hyperbolic functions (sinh, cosh, tanh, atan, atanh, asinh), along with function-level Taylor models and their correctness proofs.

Main definitions

• sinhTaylorPoly, coshTaylorPoly, etc. - Taylor polynomials
• sinhRemainderBound, coshRemainderBound, etc. - Remainder bounds
• tmSinh, tmCosh, tmTanh, tmAtan, tmAtanh, tmAsinh - Taylor models
• tmSinh_correct, tmCosh_correct, tmAtanh_correct - Correctness theorems

sinh Taylor polynomial

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

Taylor polynomial coefficients for sinh at center c = 0: sinh(x) = x + x³/3! + x⁵/5! + ...

Equations

• LeanCert.Engine.TaylorModel.sinhTaylorCoeffs n i = if i ≤ n then if i % 2 = 1 then 1 / ↑i.factorial else 0 else 0

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

Taylor polynomial for sinh of degree n

Equations

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

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

Remainder bound for sinh: |sinh(x) - T_n(x)| ≤ cosh(r) * |x|^{n+1} / (n+1)! where r = max(|lo|, |hi|). We use cosh(r) ≤ exp(r) ≤ 3^(⌈r⌉+1).

Equations

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

theorem LeanCert.Engine.TaylorModel.sinhRemainderBound_nonneg (domain : Core.IntervalRat) (n : ℕ) : 0 ≤ sinhRemainderBound domain n

Remainder bound for sinh is nonnegative

cosh Taylor polynomial

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

Taylor polynomial coefficients for cosh at center c = 0: cosh(x) = 1 + x²/2! + x⁴/4! + ...

Equations

• LeanCert.Engine.TaylorModel.coshTaylorCoeffs n i = if i ≤ n then if i % 2 = 0 then 1 / ↑i.factorial else 0 else 0

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

Taylor polynomial for cosh of degree n

Equations

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

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

Remainder bound for cosh: |cosh(x) - T_n(x)| ≤ cosh(r) * |x|^{n+1} / (n+1)! where r = max(|lo|, |hi|). We use cosh(r) ≤ exp(r) ≤ 3^(⌈r⌉+1).

Equations

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

theorem LeanCert.Engine.TaylorModel.coshRemainderBound_nonneg (domain : Core.IntervalRat) (n : ℕ) : 0 ≤ coshRemainderBound domain n

Remainder bound for cosh is nonnegative

atan Taylor polynomial

atan(x) = x - x³/3 + x⁵/5 - x⁷/7 + ... = ∑_{k=0}^∞ (-1)^k x^{2k+1} / (2k+1)

Converges for |x| ≤ 1 (inclusive at endpoints by Abel's theorem).

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

Taylor polynomial coefficients for atan at center 0

Equations

• LeanCert.Engine.TaylorModel.atanTaylorCoeffs n i = if i ≤ n then if i % 2 = 1 then have k := (i - 1) / 2; (-1) ^ k / (2 * ↑k + 1) else 0 else 0

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

Taylor polynomial for atan of degree n

Equations

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

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

Remainder bound for atan

Equations

• LeanCert.Engine.TaylorModel.atanRemainderBound domain n = min (max |domain.lo| |domain.hi|) (99 / 100) ^ (n + 1) / max (1 - min (max |domain.lo| |domain.hi|) (99 / 100) ^ 2) (1 / 100)

theorem LeanCert.Engine.TaylorModel.atanRemainderBound_nonneg (domain : Core.IntervalRat) (n : ℕ) : 0 ≤ atanRemainderBound domain n

Remainder bound for atan is nonnegative

atanh Taylor polynomial

atanh(x) = x + x³/3 + x⁵/5 + ... = ∑_{k=0}^∞ x^{2k+1} / (2k+1)

Converges for |x| < 1.

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

Taylor polynomial coefficients for atanh at center 0

Equations

• LeanCert.Engine.TaylorModel.atanhTaylorCoeffs n i = if i ≤ n then if i % 2 = 1 then have k := (i - 1) / 2; 1 / (2 * ↑k + 1) else 0 else 0

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

Taylor polynomial for atanh of degree n

Equations

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

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

Remainder bound for atanh

Equations

• LeanCert.Engine.TaylorModel.atanhRemainderBound domain n = min (max |domain.lo| |domain.hi|) (99 / 100) ^ (n + 1) / max (1 - min (max |domain.lo| |domain.hi|) (99 / 100) ^ 2) (1 / 100)

theorem LeanCert.Engine.TaylorModel.atanhRemainderBound_nonneg (domain : Core.IntervalRat) (n : ℕ) : 0 ≤ atanhRemainderBound domain n

Remainder bound for atanh is nonnegative

asinh Taylor polynomial

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

Taylor polynomial coefficients for asinh at center 0

Equations

• LeanCert.Engine.TaylorModel.asinhTaylorCoeffs n i = if i ≤ n then if i % 2 = 1 then have k := (i - 1) / 2; Ring.choose (-(1 / 2)) k / (2 * ↑k + 1) else 0 else 0

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

Taylor polynomial for asinh of degree n

Equations

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

noncomputable def LeanCert.Engine.TaylorModel.asinhDerivSup (domain : Core.IntervalRat) (n : ℕ) : ℝ

Supremum of the n-th derivative of arsinh over the interval hull of domain and 0.

Equations

• LeanCert.Engine.TaylorModel.asinhDerivSup domain n = sSup ((fun (x : ℝ) => ‖iteratedDeriv n Real.arsinh x‖) '' Set.Icc (min (↑domain.lo) 0) (max (↑domain.hi) 0))

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

Remainder bound for asinh

Equations

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

theorem LeanCert.Engine.TaylorModel.asinhRemainderBound_nonneg (domain : Core.IntervalRat) (n : ℕ) : 0 ≤ asinhRemainderBound domain n

Remainder bound for asinh is nonnegative

Function-level Taylor models

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

Taylor model for sinh z on domain J, centered at 0, degree n.

Equations

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

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

Taylor model for cosh z on domain J, centered at 0, degree n.

Equations

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

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

Function-level Taylor model for tanh at center 0. Uses tanh = sinh / cosh with the fact that cosh(x) ≥ 1 > 0 for all x.

Equations

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

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

Taylor model for atan z on domain J, centered at 0, degree n. Valid for |z| ≤ 1.

Equations

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

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

Taylor model for atanh z on domain J, centered at 0, degree n. Valid for |z| < 1.

Equations

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

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

Taylor model for asinh z on domain J, centered at 0, degree n.

Equations

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

Helper lemmas

Helper lemmas for iterated derivatives

theorem LeanCert.Engine.TaylorModel.iteratedDeriv_sinh_cosh_zero (n : ℕ) : (iteratedDeriv n Real.sinh 0 = if n % 2 = 0 then 0 else 1) ∧ iteratedDeriv n Real.cosh 0 = if n % 2 = 0 then 1 else 0

iteratedDeriv for sinh and cosh at 0, proved together. sinh: even n → 0, odd n → 1 cosh: even n → 1, odd n → 0

theorem LeanCert.Engine.TaylorModel.iteratedDeriv_sinh_zero (n : ℕ) : iteratedDeriv n Real.sinh 0 = if n % 2 = 0 then 0 else 1

iteratedDeriv n sinh at 0

theorem LeanCert.Engine.TaylorModel.iteratedDeriv_cosh_zero (n : ℕ) : iteratedDeriv n Real.cosh 0 = if n % 2 = 0 then 1 else 0

iteratedDeriv n cosh at 0

arsinh series helpers

theorem LeanCert.Engine.TaylorModel.sinhTaylorCoeffs_eq_iteratedDeriv (n i : ℕ) (hi : i ≤ n) : ↑(sinhTaylorCoeffs n i) = iteratedDeriv i Real.sinh 0 / ↑i.factorial

The sinhTaylorCoeffs match the Mathlib Taylor coefficients for sinh at 0

theorem LeanCert.Engine.TaylorModel.coshTaylorCoeffs_eq_iteratedDeriv (n i : ℕ) (hi : i ≤ n) : ↑(coshTaylorCoeffs n i) = iteratedDeriv i Real.cosh 0 / ↑i.factorial

The coshTaylorCoeffs match the Mathlib Taylor coefficients for cosh at 0

Polynomial evaluation lemmas

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

sinhTaylorPoly evaluates to the standard Taylor sum for sinh at 0.

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

coshTaylorPoly evaluates to the standard Taylor sum for cosh at 0.

atanh correctness helper

theorem LeanCert.Engine.TaylorModel.Real.atanh_hasSum {x : ℝ} (hx : |x| < 1) : HasSum (fun (k : ℕ) => x ^ (2 * k + 1) / (2 * ↑k + 1)) (Core.Real.atanh x)

The atanh series representation: atanh(x) = Σ x^(2k+1)/(2k+1) for |x| < 1. Derived from Mathlib's hasSum_log_sub_log_of_abs_lt_one.

theorem LeanCert.Engine.TaylorModel.atanhTaylorPoly_aeval_eq (n : ℕ) (z : ℝ) : (Polynomial.aeval z) (atanhTaylorPoly n) = ∑ k ∈ Finset.range (n + 1), ↑(atanhTaylorCoeffs n k) * z ^ k

atanhTaylorPoly evaluates to the standard sum.

theorem LeanCert.Engine.TaylorModel.atanh_series_remainder_bound {z : ℝ} (hz : |z| < 1) (n : ℕ) : |Core.Real.atanh z - ∑ k ∈ Finset.range (n + 1), ↑(atanhTaylorCoeffs n k) * z ^ k| ≤ |z| ^ (n + 1) / (1 - z ^ 2)

Remainder bound for the atanh series: for |z| < 1, the tail after degree n is bounded. Uses the geometric series bound on the tail.

Proof sketch:

1. atanh(z) = Σ_{k=0}^∞ z^(2k+1)/(2k+1) by Real.atanh_hasSum
2. The polynomial computes partial sum of odd terms up to degree n
3. Remainder = tail = Σ_{k: 2k+1 > n} z^(2k+1)/(2k+1)
4. |tail| ≤ Σ_{k: 2k+1 > n} |z|^(2k+1) ≤ |z|^(n+1)/(1-z²) by geometric series

Correctness theorems

theorem LeanCert.Engine.TaylorModel.tmAtanh_correct (J : Core.IntervalRat) (n : ℕ) (hJ_radius : max |J.lo| |J.hi| ≤ 99 / 100) (z : ℝ) : z ∈ J → |z| < 1 → Core.Real.atanh z ∈ (tmAtanh J n).evalSet z

atanh z ∈ (tmAtanh J n).evalSet z for all z in J with |z| < 1. Precondition: The domain radius must be ≤ 99/100.

theorem LeanCert.Engine.TaylorModel.tmSinh_correct (J : Core.IntervalRat) (n : ℕ) (z : ℝ) : z ∈ J → Real.sinh z ∈ (tmSinh J n).evalSet z

sinh z ∈ (tmSinh J n).evalSet z for all z in J. Uses taylor_remainder_bound with f = Real.sinh.

theorem LeanCert.Engine.TaylorModel.tmCosh_correct (J : Core.IntervalRat) (n : ℕ) (z : ℝ) : z ∈ J → Real.cosh z ∈ (tmCosh J n).evalSet z

cosh z ∈ (tmCosh J n).evalSet z for all z in J.

asinh correctness infrastructure

theorem LeanCert.Engine.TaylorModel.iteratedDeriv_arsinh_zero (n : ℕ) : iteratedDeriv n Real.arsinh 0 = if n % 2 = 0 then 0 else ↑(n - 1).factorial * Ring.choose (-(1 / 2)) ((n - 1) / 2)

The n-th derivative of arsinh at 0 follows the pattern:

• For even n: 0
• For odd n = 2k+1: (2k)! * Ring.choose (-1/2) k

This matches the coefficients in asinhTaylorCoeffs times n!.

Note: This is proved using the known series expansion of arsinh, which satisfies arsinh(x) = Σ_{k=0}^∞ a_k x^(2k+1) where a_k = Ring.choose (-1/2) k / (2k+1).

theorem LeanCert.Engine.TaylorModel.asinhTaylorCoeffs_eq_iteratedDeriv (n i : ℕ) (hi : i ≤ n) : ↑(asinhTaylorCoeffs n i) = iteratedDeriv i Real.arsinh 0 / ↑i.factorial

The asinhTaylorCoeffs match the Mathlib Taylor coefficients for arsinh at 0

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

asinhTaylorPoly evaluates to the standard Taylor sum for arsinh at 0.

theorem LeanCert.Engine.TaylorModel.arsinh_deriv_bound (domain : Core.IntervalRat) (n : ℕ) (x : ℝ) : x ∈ Set.Icc (min (↑domain.lo) 0) (max (↑domain.hi) 0) → ‖iteratedDeriv n Real.arsinh x‖ ≤ asinhDerivSup domain n

Bound on the n-th derivative of arsinh on the interval hull of domain and 0.

theorem LeanCert.Engine.TaylorModel.tmAsinh_correct (J : Core.IntervalRat) (n : ℕ) (z : ℝ) : z ∈ J → Real.arsinh z ∈ (tmAsinh J n).evalSet z

arsinh z ∈ (tmAsinh J n).evalSet z for all z in J. Uses taylor_remainder_bound with f = Real.arsinh, M = asinhDerivSup J (n+1).