Documentation

Mathlib.Analysis.SpecialFunctions.Trigonometric.Series

Trigonometric functions as sums of infinite series #

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

Main results #

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_sin' (z : ) :
HasSum (fun n => (z * Complex.I) ^ (2 * n + 1) / ↑(Nat.factorial (2 * n + 1)) / Complex.I) (Complex.sin 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.

theorem Complex.hasSum_sin (z : ) :
HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(Nat.factorial (2 * n + 1))) (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) / ↑(Nat.factorial (2 * n))
theorem Complex.sin_eq_tsum' (z : ) :
Complex.sin z = ∑' (n : ), (z * Complex.I) ^ (2 * n + 1) / ↑(Nat.factorial (2 * n + 1)) / Complex.I
theorem Complex.cos_eq_tsum (z : ) :
Complex.cos z = ∑' (n : ), (-1) ^ n * z ^ (2 * n) / ↑(Nat.factorial (2 * n))
theorem Complex.sin_eq_tsum (z : ) :
Complex.sin z = ∑' (n : ), (-1) ^ n * z ^ (2 * n + 1) / ↑(Nat.factorial (2 * n + 1))
theorem Real.hasSum_cos (r : ) :
HasSum (fun n => (-1) ^ n * r ^ (2 * n) / ↑(Nat.factorial (2 * n))) (Real.cos r)

The power series expansion of Real.cos.

theorem Real.hasSum_sin (r : ) :
HasSum (fun n => (-1) ^ n * r ^ (2 * n + 1) / ↑(Nat.factorial (2 * n + 1))) (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) / ↑(Nat.factorial (2 * n))
theorem Real.sin_eq_tsum (r : ) :
Real.sin r = ∑' (n : ), (-1) ^ n * r ^ (2 * n + 1) / ↑(Nat.factorial (2 * n + 1))