Bounds for sin and cos

Monotonicity of sin on intervals

theorem Real.sin_monotone (n : ℤ) : MonotoneOn sin (Set.Icc (↑n * (2 * Real.pi) - Real.pi / 2) (↑n * (2 * Real.pi) + Real.pi / 2))

All the intervals on which sin is increasing

theorem Real.sin_antitone (n : ℤ) : AntitoneOn sin (Set.Icc (↑n * (2 * Real.pi) + Real.pi / 2) (↑n * (2 * Real.pi) + 3 * Real.pi / 2))

All the intervals on which sin is decreasing

Taylor series with remainder for sin and cos

theorem Finset.sum_range_even {M : Type u_1} [AddCommMonoid M] (n : ℕ) (f : ℕ → M) : ∑ k ∈ range n, f k = ∑ k ∈ range (2 * n), if Even k then f (k / 2) else 0

Double the range of a Finset.sum

theorem Complex.sin_series_bound {z : ℂ} (z1 : ‖z‖ ≤ 1) (n : ℕ) : ‖sin z - z * ∑ k ∈ Finset.range n, (-1) ^ k * z ^ (2 * k) / ↑(2 * k + 1).factorial‖ ≤ ‖z‖ ^ (2 * n + 1) * ((2 * ↑n + 2) / (↑(2 * n + 1).factorial * (2 * ↑n + 1)))

theorem Complex.cos_series_bound {z : ℂ} (z1 : ‖z‖ ≤ 1) {n : ℕ} (n0 : 0 < n) : ‖cos z - ∑ k ∈ Finset.range n, (-1) ^ k * z ^ (2 * k) / ↑(2 * k).factorial‖ ≤ ‖z‖ ^ (2 * n) * ((2 * ↑n + 1) / (↑(2 * n).factorial * (2 * ↑n)))

theorem Real.sin_series_bound {x : ℝ} (x1 : |x| ≤ 1) (n : ℕ) : |sin x - x * ∑ k ∈ Finset.range n, (-1) ^ k * x ^ (2 * k) / ↑(2 * k + 1).factorial| ≤ |x| ^ (2 * n + 1) * ((2 * ↑n + 2) / (↑(2 * n + 1).factorial * (2 * ↑n + 1)))

theorem Real.cos_series_bound {x : ℝ} (x1 : |x| ≤ 1) {n : ℕ} (n0 : 0 < n) : |cos x - ∑ k ∈ Finset.range n, (-1) ^ k * x ^ (2 * k) / ↑(2 * k).factorial| ≤ |x| ^ (2 * n) * ((2 * ↑n + 1) / (↑(2 * n).factorial * (2 * ↑n)))

Real.sinc and Complex.sinc

noncomputable def Complex.sinc (z : ℂ) : ℂ

Equations

• z.sinc = if z = 0 then 1 else Complex.sin z / z

theorem Real.sin_eq_sinc (x : ℝ) : sin x = x * sinc x

sinc suffices to compute sin

theorem Complex.sin_eq_sinc (z : ℂ) : sin z = z * z.sinc

sinc suffices to compute sin

@[simp]

theorem Complex.sinc_neg (x : ℝ) : (-↑x).sinc = (↑x).sinc

@[simp]

theorem Real.sinc_abs (x : ℝ) : sinc |x| = sinc x

sinc is even

@[simp]

theorem Complex.ofReal_sinc (x : ℝ) : ↑(Real.sinc x) = (↑x).sinc

Taylor series with remainder for sinc

theorem Complex.sinc_series_bound {z : ℂ} (z1 : ‖z‖ ≤ 1) (n : ℕ) : ‖z.sinc - ∑ k ∈ Finset.range n, (-1) ^ k * z ^ (2 * k) / ↑(2 * k + 1).factorial‖ ≤ ‖z‖ ^ (2 * n) * ((2 * ↑n + 2) / (↑(2 * n + 1).factorial * (2 * ↑n + 1)))

theorem Real.sinc_series_bound {x : ℝ} (x1 : |x| ≤ 1) (n : ℕ) : |sinc x - ∑ k ∈ Finset.range n, (-1) ^ k * x ^ (2 * k) / ↑(2 * k + 1).factorial| ≤ |x| ^ (2 * n) * ((2 * ↑n + 2) / (↑(2 * n + 1).factorial * (2 * ↑n + 1)))

Auxiliary functions with cleaner power series

noncomputable def sinc_sqrt (x : ℝ) : ℝ

Equations

• sinc_sqrt x = Real.sinc √x

noncomputable def cos_sqrt (x : ℝ) : ℝ

Equations

• cos_sqrt x = Real.cos √x

theorem Real.sinc_eq_sinc_sqrt (x : ℝ) : sinc x = sinc_sqrt (|x| ^ 2)

sinc_sqrt suffices to compute sinc

theorem Real.sin_eq_sinc_sqrt (x : ℝ) : sin x = x * sinc_sqrt (|x| ^ 2)

sinc_sqrt suffices to compute sin

theorem cos_eq_cos_sqrt (x : ℝ) : Real.cos x = cos_sqrt (|x| ^ 2)

cos_sqrt suffices to compute cos