mathlib3 documentation

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 #

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 : ) :
complex.cos z = ∑' (n : ), (z * complex.I) ^ (2 * n) / ((2 * n).factorial)
theorem complex.sin_eq_tsum' (z : ) :
complex.sin z = ∑' (n : ), (z * complex.I) ^ (2 * n + 1) / ((2 * n + 1).factorial) / complex.I
theorem complex.cos_eq_tsum (z : ) :
complex.cos z = ∑' (n : ), (-1) ^ n * z ^ (2 * n) / ((2 * n).factorial)
theorem complex.sin_eq_tsum (z : ) :
complex.sin 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 : ) :
real.cos r = ∑' (n : ), (-1) ^ n * r ^ (2 * n) / ((2 * n).factorial)
theorem real.sin_eq_tsum (r : ) :
real.sin r = ∑' (n : ), (-1) ^ n * r ^ (2 * n + 1) / ((2 * n + 1).factorial)