Computable Range Reduction for Trigonometric Functions

This file implements range reduction for sin and cos to improve Taylor series convergence for intervals far from 0.

Problem

Standard Taylor series for sin/cos centered at 0 have remainder bounds of |x|^{n+1} / (n+1)!. For intervals far from 0 (e.g., [10, 11]), this remainder is huge even for moderate n.

Solution: Range Reduction

Use the periodicity of sin/cos:

• sin(x) = sin(x - 2πk) for any integer k
• cos(x) = cos(x - 2πk) for any integer k

By choosing k to bring x - 2πk into [-π, π], the Taylor series converges much faster since |x - 2πk| ≤ π ≈ 3.14.

Main definitions

• twoPiRatLo, twoPiRatHi - Rational bounds for 2π
• reduceToMainPeriod - Shift interval to be near 0
• sinComputableReduced, cosComputableReduced - Computable evaluation with range reduction

Rational approximations of π and 2π

def LeanCert.Core.IntervalRat.piRatLo : ℚ

Lower bound for π: 314159265/100000000 < π

Equations

• LeanCert.Core.IntervalRat.piRatLo = 314159265 / 100000000

def LeanCert.Core.IntervalRat.piRatHi : ℚ

Upper bound for π: π < 355/113

Equations

• LeanCert.Core.IntervalRat.piRatHi = 355 / 113

def LeanCert.Core.IntervalRat.twoPiRatLo : ℚ

Lower bound for 2π

Equations

• LeanCert.Core.IntervalRat.twoPiRatLo = 2 * LeanCert.Core.IntervalRat.piRatLo

def LeanCert.Core.IntervalRat.twoPiRatHi : ℚ

Upper bound for 2π

Equations

• LeanCert.Core.IntervalRat.twoPiRatHi = 2 * LeanCert.Core.IntervalRat.piRatHi

theorem LeanCert.Core.IntervalRat.piRatLo_lt_pi : ↑piRatLo < Real.pi

piRatLo < π, proved from Mathlib's decimal π bounds.

theorem LeanCert.Core.IntervalRat.pi_lt_piRatHi : Real.pi < ↑piRatHi

π < piRatHi, proved from Mathlib's decimal π bounds.

theorem LeanCert.Core.IntervalRat.twoPiRatLo_lt_two_pi : ↑twoPiRatLo < 2 * Real.pi

twoPiRatLo < 2π

theorem LeanCert.Core.IntervalRat.two_pi_lt_twoPiRatHi : 2 * Real.pi < ↑twoPiRatHi

2π < twoPiRatHi

theorem LeanCert.Core.IntervalRat.twoPiRatLo_le_twoPiRatHi : twoPiRatLo ≤ twoPiRatHi

twoPiRatLo ≤ twoPiRatHi

Range reduction

def LeanCert.Core.IntervalRat.computeShiftK (I : IntervalRat) : ℤ

Compute the shift amount k such that I.midpoint - k * 2π is approximately in [-π, π].

Equations

• I.computeShiftK = (I.midpoint / LeanCert.Core.IntervalRat.twoPiRatHi).floor

def LeanCert.Core.IntervalRat.shiftInterval (I : IntervalRat) (k : ℤ) : IntervalRat

Shift an interval by subtracting k * 2π (using rational bounds).

For positive k: subtract k * twoPiRatHi from lo, k * twoPiRatLo from hi For negative k: opposite to maintain containment

Equations

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

def LeanCert.Core.IntervalRat.reduceToMainPeriod (I : IntervalRat) : IntervalRat × ℤ

Reduce interval to be approximately in [-π, π] by subtracting multiples of 2π.

Equations

• I.reduceToMainPeriod = (I.shiftInterval I.computeShiftK, I.computeShiftK)

Correctness of range reduction

theorem LeanCert.Core.IntervalRat.mem_shiftInterval_of_mem {x : ℝ} {I : IntervalRat} {k : ℤ} (hx : x ∈ I) : x - 2 * Real.pi * ↑k ∈ I.shiftInterval k

If x ∈ I (as reals), then x - 2πk ∈ shiftInterval I k (as reals).

Computable reduced evaluation

def LeanCert.Core.IntervalRat.sinComputableReduced (I : IntervalRat) (n : ℕ := 10) : IntervalRat

Computable sin evaluation with range reduction.

Equations

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

def LeanCert.Core.IntervalRat.cosComputableReduced (I : IntervalRat) (n : ℕ := 10) : IntervalRat

Computable cos evaluation with range reduction.

Equations

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

theorem LeanCert.Core.IntervalRat.mem_sinComputableReduced {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (n : ℕ := 10) : Real.sin x ∈ I.sinComputableReduced n

sin x ∈ sinComputableReduced I for all x ∈ I

theorem LeanCert.Core.IntervalRat.mem_cosComputableReduced {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (n : ℕ := 10) : Real.cos x ∈ I.cosComputableReduced n

cos x ∈ cosComputableReduced I for all x ∈ I