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

source
theorem Complex.hasSum_cos' (z : ℂ) :
HasSum (fun (n : ℕ) => (z * I) ^ (2 * n) / ↑(2 * n).factorial) (cos z)
source
theorem Complex.hasSum_sin' (z : ℂ) :
HasSum (fun (n : ℕ) => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1).factorial / I) (sin z)
source
theorem Complex.hasSum_cos (z : ℂ) :
HasSum (fun (n : ℕ) => (-1) ^ n * z ^ (2 * n) / ↑(2 * n).factorial) (cos z)

The power series expansion of Complex.cos.

source
theorem Complex.hasSum_sin (z : ℂ) :
HasSum (fun (n : ℕ) => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1).factorial) (sin z)

The power series expansion of Complex.sin.

source
theorem Complex.cos_eq_tsum' (z : ℂ) :
cos z = ∑' (n : ℕ), (z * I) ^ (2 * n) / ↑(2 * n).factorial
source
theorem Complex.sin_eq_tsum' (z : ℂ) :
sin z = ∑' (n : ℕ), (z * I) ^ (2 * n + 1) / ↑(2 * n + 1).factorial / I
source
theorem Complex.cos_eq_tsum (z : ℂ) :
cos z = ∑' (n : ℕ), (-1) ^ n * z ^ (2 * n) / ↑(2 * n).factorial
source
theorem Complex.sin_eq_tsum (z : ℂ) :
sin z = ∑' (n : ℕ), (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1).factorial
source
theorem Real.hasSum_cos (r : ℝ) :
HasSum (fun (n : ℕ) => (-1) ^ n * r ^ (2 * n) / ↑(2 * n).factorial) (cos r)

The power series expansion of Real.cos.

source
theorem Real.hasSum_sin (r : ℝ) :
HasSum (fun (n : ℕ) => (-1) ^ n * r ^ (2 * n + 1) / ↑(2 * n + 1).factorial) (sin r)

The power series expansion of Real.sin.

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

cosh and sinh for ℝ and ℂ #

source
theorem Complex.hasSum_cosh (z : ℂ) :
HasSum (fun (n : ℕ) => z ^ (2 * n) / ↑(2 * n).factorial) (cosh z)

The power series expansion of Complex.cosh.

source
theorem Complex.hasSum_sinh (z : ℂ) :
HasSum (fun (n : ℕ) => z ^ (2 * n + 1) / ↑(2 * n + 1).factorial) (sinh z)

The power series expansion of Complex.sinh.

source
theorem Complex.cosh_eq_tsum (z : ℂ) :
cosh z = ∑' (n : ℕ), z ^ (2 * n) / ↑(2 * n).factorial
source
theorem Complex.sinh_eq_tsum (z : ℂ) :
sinh z = ∑' (n : ℕ), z ^ (2 * n + 1) / ↑(2 * n + 1).factorial
source
theorem Real.hasSum_cosh (r : ℝ) :
HasSum (fun (n : ℕ) => r ^ (2 * n) / ↑(2 * n).factorial) (cosh r)

The power series expansion of Real.cosh.

source
theorem Real.hasSum_sinh (r : ℝ) :
HasSum (fun (n : ℕ) => r ^ (2 * n + 1) / ↑(2 * n + 1).factorial) (sinh r)

The power series expansion of Real.sinh.

source
theorem Real.cosh_eq_tsum (r : ℝ) :
cosh r = ∑' (n : ℕ), r ^ (2 * n) / ↑(2 * n).factorial
source
theorem Real.sinh_eq_tsum (r : ℝ) :
sinh r = ∑' (n : ℕ), r ^ (2 * n + 1) / ↑(2 * n + 1).factorial
source
theorem Real.cosh_le_exp_half_sq (x : ℝ) :
cosh x ≤ exp (x ^ 2 / 2)