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 ℂ #

source
theorem complex.has_sum_cos' (z : ℂ) :
has_sum (λ (n : ℕ), (z * complex.I) ^ (2 * n) / ↑((2 * n).factorial)) (complex.cos z)
source
theorem complex.has_sum_sin' (z : ℂ) :
has_sum (λ (n : ℕ), (z * complex.I) ^ (2 * n + 1) / ↑((2 * n + 1).factorial) / complex.I) (complex.sin z)
source
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.

source
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.

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

source
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.

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