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))

cosh and sinh for ℝ and ℂ

theorem Complex.hasSum_cosh (z : ℂ) : HasSum (fun (n : ℕ) => z ^ (2 * n) / ↑(Nat.factorial (2 * n))) (Complex.cosh z)

The power series expansion of Complex.cosh.

theorem Complex.hasSum_sinh (z : ℂ) : HasSum (fun (n : ℕ) => z ^ (2 * n + 1) / ↑(Nat.factorial (2 * n + 1))) (Complex.sinh z)

The power series expansion of Complex.sinh.

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

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

theorem Real.hasSum_cosh (r : ℝ) : HasSum (fun (n : ℕ) => r ^ (2 * n) / ↑(Nat.factorial (2 * n))) (Real.cosh r)

The power series expansion of Real.cosh.

theorem Real.hasSum_sinh (r : ℝ) : HasSum (fun (n : ℕ) => r ^ (2 * n + 1) / ↑(Nat.factorial (2 * n + 1))) (Real.sinh r)

The power series expansion of Real.sinh.

theorem Real.cosh_eq_tsum (r : ℝ) : Real.cosh r = ∑' (n : ℕ), r ^ (2 * n) / ↑(Nat.factorial (2 * n))

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

theorem Real.cosh_le_exp_half_sq (x : ℝ) : Real.cosh x ≤ Real.exp (x ^ 2 / 2)