# mathlib3documentation

analysis.special_functions.trigonometric.series

# Trigonometric functions as sums of infinite series #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main results #

• complex.has_sum_cos, complex.tsum_cos: complex.cos as the sum of an infinite series.
• real.has_sum_cos, real.tsum_cos: real.cos as the sum of an infinite series.
• complex.has_sum_sin, complex.tsum_sin: complex.sin as the sum of an infinite series.
• real.has_sum_sin, real.tsum_sin: real.sin as the sum of an infinite series.

### cos and sin for ℝ and ℂ#

theorem complex.has_sum_cos' (z : ) :
has_sum (λ (n : ), (z * complex.I) ^ (2 * n) / ((2 * n).factorial)) (complex.cos z)
theorem complex.has_sum_sin' (z : ) :
has_sum (λ (n : ), (z * complex.I) ^ (2 * n + 1) / ((2 * n + 1).factorial) / complex.I) (complex.sin z)
theorem complex.has_sum_cos (z : ) :
has_sum (λ (n : ), (-1) ^ n * z ^ (2 * n) / ((2 * n).factorial)) (complex.cos z)

The power series expansion of complex.cos.

theorem complex.has_sum_sin (z : ) :
has_sum (λ (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.has_sum_cos (r : ) :
has_sum (λ (n : ), (-1) ^ n * r ^ (2 * n) / ((2 * n).factorial)) (real.cos r)

The power series expansion of real.cos.

theorem real.has_sum_sin (r : ) :
has_sum (λ (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)