Trigonometric functions as sums of infinite series

In this file we express trigonometric functions in terms of their series expansion.

Main results

• Complex.hasSum_cos, Complex.cos_eq_tsum: Complex.cos as the sum of an infinite series.
• Real.hasSum_cos, Real.cos_eq_tsum: Real.cos as the sum of an infinite series.
• Complex.hasSum_sin, Complex.sin_eq_tsum: Complex.sin as the sum of an infinite series.
• Real.hasSum_sin, Real.sin_eq_tsum: Real.sin as the sum of an infinite series.

cos and sin for ℝ and ℂ

theorem Complex.hasSum_cos' (z : ℂ) : HasSum (fun n => (z * Complex.I) ^ (2 * n) / ↑(Nat.factorial (2 * n))) (Complex.cos z)

theorem Complex.hasSum_sin' (z : ℂ) : HasSum (fun n => (z * Complex.I) ^ (2 * n + 1) / ↑(Nat.factorial (2 * n + 1)) / Complex.I) (Complex.sin z)

theorem Complex.hasSum_cos (z : ℂ) : HasSum (fun n => (-1) ^ n * z ^ (2 * n) / ↑(Nat.factorial (2 * n))) (Complex.cos z)

The power series expansion of Complex.cos.

theorem Complex.hasSum_sin (z : ℂ) : HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(Nat.factorial (2 * n + 1))) (Complex.sin z)

The power series expansion of Complex.sin.

theorem Complex.cos_eq_tsum' (z : ℂ) : Complex.cos z = ∑' (n : ℕ), (z * Complex.I) ^ (2 * n) / ↑(Nat.factorial (2 * n))

theorem Complex.sin_eq_tsum' (z : ℂ) : Complex.sin z = ∑' (n : ℕ), (z * Complex.I) ^ (2 * n + 1) / ↑(Nat.factorial (2 * n + 1)) / Complex.I

theorem Complex.cos_eq_tsum (z : ℂ) : Complex.cos z = ∑' (n : ℕ), (-1) ^ n * z ^ (2 * n) / ↑(Nat.factorial (2 * n))

theorem Complex.sin_eq_tsum (z : ℂ) : Complex.sin z = ∑' (n : ℕ), (-1) ^ n * z ^ (2 * n + 1) / ↑(Nat.factorial (2 * n + 1))

theorem Real.hasSum_cos (r : ℝ) : HasSum (fun n => (-1) ^ n * r ^ (2 * n) / ↑(Nat.factorial (2 * n))) (Real.cos r)

The power series expansion of Real.cos.

theorem Real.hasSum_sin (r : ℝ) : HasSum (fun n => (-1) ^ n * r ^ (2 * n + 1) / ↑(Nat.factorial (2 * n + 1))) (Real.sin r)

The power series expansion of Real.sin.

theorem Real.cos_eq_tsum (r : ℝ) : Real.cos r = ∑' (n : ℕ), (-1) ^ n * r ^ (2 * n) / ↑(Nat.factorial (2 * n))

theorem Real.sin_eq_tsum (r : ℝ) : Real.sin r = ∑' (n : ℕ), (-1) ^ n * r ^ (2 * n + 1) / ↑(Nat.factorial (2 * n + 1))