# 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) / (2 * n).factorial) (Complex.cos z)
theorem Complex.hasSum_sin' (z : ) :
HasSum (fun (n : ) => (z * Complex.I) ^ (2 * n + 1) / (2 * n + 1).factorial / Complex.I) (Complex.sin z)
theorem Complex.hasSum_cos (z : ) :
HasSum (fun (n : ) => (-1) ^ n * z ^ (2 * n) / (2 * n).factorial) (Complex.cos z)

The power series expansion of Complex.cos.

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

The power series expansion of Complex.sin.

theorem Complex.cos_eq_tsum' (z : ) :
= ∑' (n : ), (z * Complex.I) ^ (2 * n) / (2 * n).factorial
theorem Complex.sin_eq_tsum' (z : ) :
= ∑' (n : ), (z * Complex.I) ^ (2 * n + 1) / (2 * n + 1).factorial / Complex.I
theorem Complex.cos_eq_tsum (z : ) :
= ∑' (n : ), (-1) ^ n * z ^ (2 * n) / (2 * n).factorial
theorem Complex.sin_eq_tsum (z : ) :
= ∑' (n : ), (-1) ^ n * z ^ (2 * n + 1) / (2 * n + 1).factorial
theorem Real.hasSum_cos (r : ) :
HasSum (fun (n : ) => (-1) ^ n * r ^ (2 * n) / (2 * n).factorial) (Real.cos r)

The power series expansion of Real.cos.

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

The power series expansion of Real.sin.

theorem Real.cos_eq_tsum (r : ) :
= ∑' (n : ), (-1) ^ n * r ^ (2 * n) / (2 * n).factorial
theorem Real.sin_eq_tsum (r : ) :
= ∑' (n : ), (-1) ^ n * r ^ (2 * n + 1) / (2 * n + 1).factorial

### cosh and sinh for ℝ and ℂ#

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

The power series expansion of Complex.cosh.

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

The power series expansion of Complex.sinh.

theorem Complex.cosh_eq_tsum (z : ) :
= ∑' (n : ), z ^ (2 * n) / (2 * n).factorial
theorem Complex.sinh_eq_tsum (z : ) :
= ∑' (n : ), z ^ (2 * n + 1) / (2 * n + 1).factorial
theorem Real.hasSum_cosh (r : ) :
HasSum (fun (n : ) => r ^ (2 * n) / (2 * n).factorial) (Real.cosh r)

The power series expansion of Real.cosh.

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

The power series expansion of Real.sinh.

theorem Real.cosh_eq_tsum (r : ) :
= ∑' (n : ), r ^ (2 * n) / (2 * n).factorial
theorem Real.sinh_eq_tsum (r : ) :
= ∑' (n : ), r ^ (2 * n + 1) / (2 * n + 1).factorial