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_cos
(z : ℂ)
:
HasSum (fun n => (-1) ^ n * z ^ (2 * n) / ↑(Nat.factorial (2 * n))) (Complex.cos z)
The power series expansion of Complex.cos
.
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))