Taylor Models - Trigonometric Functions

This file contains Taylor polynomial definitions and remainder bounds for trigonometric functions (sin, cos, sinc), along with function-level Taylor models and their correctness proofs.

Main definitions

• sinTaylorPoly, cosTaylorPoly, sincTaylorPoly - Taylor polynomials
• sinRemainderBound, cosRemainderBound, sincRemainderBound - Remainder bounds
• tmSin, tmCos, tmSinc - Function-level Taylor models
• tmSin_correct, tmCos_correct - Correctness theorems

sin Taylor polynomial

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

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

Equations

• LeanCert.Engine.TaylorModel.sinTaylorCoeffs n i = if i ≤ n then if i % 2 = 1 then (-1) ^ ((i - 1) / 2) / ↑i.factorial else 0 else 0

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

Taylor polynomial for sin of degree n

Equations

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

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

Remainder bound for sin: |sin(x) - T_n(x)| ≤ |x|^{n+1} / (n+1)! since |sin^{(k)}| ≤ 1

Equations

• LeanCert.Engine.TaylorModel.sinRemainderBound domain n = max |domain.lo| |domain.hi| ^ (n + 1) / ↑(n + 1).factorial

theorem LeanCert.Engine.TaylorModel.sinRemainderBound_nonneg (domain : Core.IntervalRat) (n : ℕ) : 0 ≤ sinRemainderBound domain n

Remainder bound for sin is nonnegative

cos Taylor polynomial

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

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

Equations

• LeanCert.Engine.TaylorModel.cosTaylorCoeffs n i = if i ≤ n then if i % 2 = 0 then (-1) ^ (i / 2) / ↑i.factorial else 0 else 0

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

Taylor polynomial for cos of degree n

Equations

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

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

Remainder bound for cos: |cos(x) - T_n(x)| ≤ |x|^{n+1} / (n+1)! since |cos^{(k)}| ≤ 1

Equations

• LeanCert.Engine.TaylorModel.cosRemainderBound domain n = max |domain.lo| |domain.hi| ^ (n + 1) / ↑(n + 1).factorial

theorem LeanCert.Engine.TaylorModel.cosRemainderBound_nonneg (domain : Core.IntervalRat) (n : ℕ) : 0 ≤ cosRemainderBound domain n

Remainder bound for cos is nonnegative

sinc Taylor polynomial

sinc(x) = sin(x)/x for x ≠ 0, sinc(0) = 1 = 1 - x²/6 + x⁴/120 - x⁶/5040 + ... = Σ_{n=0}^∞ (-1)^n x^{2n} / (2n+1)!

Note: sinc is entire (analytic everywhere), so the series converges for all x.

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

Taylor polynomial coefficients for sinc at center 0: sinc(x) = 1 - x²/6 + x⁴/120 - ... = Σ (-1)^k x^{2k} / (2k+1)!

Equations

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

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

Taylor polynomial for sinc of degree n

Equations

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

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

Remainder bound for sinc: uses the fact that |sinc^(n+1)(ξ)| ≤ 1 for all ξ. This follows from |sinc(x)| ≤ 1 and derivatives being bounded. We use a crude but safe exponential bound.

Equations

• LeanCert.Engine.TaylorModel.sincRemainderBound domain n = max |domain.lo| |domain.hi| ^ (n + 1) / ↑(n + 1).factorial

theorem LeanCert.Engine.TaylorModel.sincRemainderBound_nonneg (domain : Core.IntervalRat) (n : ℕ) : 0 ≤ sincRemainderBound domain n

Remainder bound for sinc is nonnegative

Function-level Taylor models

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

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

Equations

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

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

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

Equations

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

noncomputable def LeanCert.Engine.TaylorModel.tmSinc (J : Core.IntervalRat) (_n : ℕ) : TaylorModel

Taylor model for sinc z on domain J, centered at 0, degree n. sinc(z) = sin(z)/z for z ≠ 0, sinc(0) = 1.

Equations

• LeanCert.Engine.TaylorModel.tmSinc J _n = { poly := 0, remainder := { lo := -1, hi := 1, le := LeanCert.Engine.TaylorModel.tmSinc._proof_1 }, center := 0, domain := J }

Helper lemmas for iterated derivatives

theorem LeanCert.Engine.TaylorModel.iteratedDeriv_sin_zero (n : ℕ) : iteratedDeriv n Real.sin 0 = if n % 4 = 0 then 0 else if n % 4 = 1 then 1 else if n % 4 = 2 then 0 else -1

iteratedDeriv n sin at 0

theorem LeanCert.Engine.TaylorModel.iteratedDeriv_cos_zero (n : ℕ) : iteratedDeriv n Real.cos 0 = if n % 4 = 0 then 1 else if n % 4 = 1 then 0 else if n % 4 = 2 then -1 else 0

iteratedDeriv n cos at 0

theorem LeanCert.Engine.TaylorModel.iteratedDeriv_sin_zero_even {n : ℕ} (hn : n % 2 = 0) : iteratedDeriv n Real.sin 0 = 0

For even n, iteratedDeriv n sin 0 = 0

theorem LeanCert.Engine.TaylorModel.iteratedDeriv_sin_zero_odd {n : ℕ} (hn : n % 2 = 1) : iteratedDeriv n Real.sin 0 = (-1) ^ ((n - 1) / 2)

For odd n, iteratedDeriv n sin 0 = (-1)^((n-1)/2)

theorem LeanCert.Engine.TaylorModel.sinTaylorCoeffs_eq_iteratedDeriv (n i : ℕ) (hi : i ≤ n) : ↑(sinTaylorCoeffs n i) = iteratedDeriv i Real.sin 0 / ↑i.factorial

The sinTaylorCoeffs match the Mathlib Taylor coefficients for sin at 0

theorem LeanCert.Engine.TaylorModel.iteratedDeriv_cos_zero_even {n : ℕ} (hn : n % 2 = 0) : iteratedDeriv n Real.cos 0 = (-1) ^ (n / 2)

For even n, iteratedDeriv n cos 0 = (-1)^(n/2)

theorem LeanCert.Engine.TaylorModel.iteratedDeriv_cos_zero_odd {n : ℕ} (hn : n % 2 = 1) : iteratedDeriv n Real.cos 0 = 0

For odd n, iteratedDeriv n cos 0 = 0

theorem LeanCert.Engine.TaylorModel.cosTaylorCoeffs_eq_iteratedDeriv (n i : ℕ) (hi : i ≤ n) : ↑(cosTaylorCoeffs n i) = iteratedDeriv i Real.cos 0 / ↑i.factorial

The cosTaylorCoeffs match the Mathlib Taylor coefficients for cos at 0

Polynomial evaluation lemmas

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

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

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

cosTaylorPoly evaluates to the standard Taylor sum for cos at 0.

Correctness theorems

theorem LeanCert.Engine.TaylorModel.tmSin_correct (J : Core.IntervalRat) (n : ℕ) (z : ℝ) : z ∈ J → Real.sin z ∈ (tmSin J n).evalSet z

sin z ∈ (tmSin J n).evalSet z for all z in J. Uses taylor_remainder_bound with f = Real.sin, c = 0, M = 1.

theorem LeanCert.Engine.TaylorModel.tmCos_correct (J : Core.IntervalRat) (n : ℕ) (z : ℝ) : z ∈ J → Real.cos z ∈ (tmCos J n).evalSet z

cos z ∈ (tmCos J n).evalSet z for all z in J. Uses taylor_remainder_bound with f = Real.cos, c = 0, M = 1.

sinc correctness infrastructure

theorem LeanCert.Engine.TaylorModel.contDiff_sinc : ContDiff ℝ ⊤ Real.sinc

sinc is C^∞ (smooth).

Mathematical justification: sinc is analytic everywhere with the series sinc(x) = Σ_{k=0}^∞ (-1)^k x^{2k} / (2k+1)! which converges for all x ∈ ℝ. Being analytic, it is smooth (C^∞).

This fact follows from sinc being the dslope of sin at 0, and sin being entire (analytic everywhere). The smoothness can be proven using the series representation or by showing the iterated derivatives exist and are continuous at all points including 0.

Technical note: The proof at x = 0 is subtle because we need to show that the limit defining each higher derivative exists. This follows from the Taylor series representation.

theorem LeanCert.Engine.TaylorModel.iteratedDeriv_sinc_zero (n : ℕ) : iteratedDeriv n Real.sinc 0 = if n % 2 = 0 then have k := n / 2; (-1) ^ k / ↑(2 * k + 1) else 0

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

• For odd n: 0 (sinc is even, so odd derivatives at 0 vanish)
• For even n = 2k: (-1)^k * (2k)! / (2k+1)! = (-1)^k / (2k+1)

This matches the coefficients in sincTaylorCoeffs times n!.

The proof uses the recurrence: (n+1) * sinc^{(n)}(0) = sin^{(n+1)}(0), which follows from differentiating x * sinc(x) = sin(x).

theorem LeanCert.Engine.TaylorModel.sincTaylorCoeffs_eq_iteratedDeriv (n i : ℕ) (hi : i ≤ n) : ↑(sincTaylorCoeffs n i) = iteratedDeriv i Real.sinc 0 / ↑i.factorial

The sincTaylorCoeffs match the Taylor coefficients for sinc at 0

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

sincTaylorPoly evaluates to the standard Taylor sum for sinc at 0.

theorem LeanCert.Engine.TaylorModel.tmSinc_correct (J : Core.IntervalRat) (n : ℕ) (z : ℝ) : z ∈ J → Real.sinc z ∈ (tmSinc J n).evalSet z

sinc z ∈ (tmSinc J n).evalSet z for all z in J. Uses the global bound |sinc z| ≤ 1.