Documentation

Mathlib.Data.Complex.Trigonometric

Trigonometric and hyperbolic trigonometric functions #

This file contains the definitions of the sine, cosine, tangent, hyperbolic sine, hyperbolic cosine, and hyperbolic tangent functions.

def Complex.sin (z : ) :

The complex sine function, defined via exp

Equations
def Complex.cos (z : ) :

The complex cosine function, defined via exp

Equations
def Complex.tan (z : ) :

The complex tangent function, defined as sin z / cos z

Equations
def Complex.cot (z : ) :

The complex cotangent function, defined as cos z / sin z

Equations
def Complex.sinh (z : ) :

The complex hyperbolic sine function, defined via exp

Equations
def Complex.cosh (z : ) :

The complex hyperbolic cosine function, defined via exp

Equations
def Complex.tanh (z : ) :

The complex hyperbolic tangent function, defined as sinh z / cosh z

Equations
def Real.sin (x : ) :

The real sine function, defined as the real part of the complex sine

Equations
def Real.cos (x : ) :

The real cosine function, defined as the real part of the complex cosine

Equations
def Real.tan (x : ) :

The real tangent function, defined as the real part of the complex tangent

Equations
def Real.cot (x : ) :

The real cotangent function, defined as the real part of the complex cotangent

Equations
def Real.sinh (x : ) :

The real hypebolic sine function, defined as the real part of the complex hyperbolic sine

Equations
def Real.cosh (x : ) :

The real hypebolic cosine function, defined as the real part of the complex hyperbolic cosine

Equations
def Real.tanh (x : ) :

The real hypebolic tangent function, defined as the real part of the complex hyperbolic tangent

Equations
theorem Complex.two_sinh (x : ) :
2 * sinh x = exp x - exp (-x)
theorem Complex.two_cosh (x : ) :
2 * cosh x = exp x + exp (-x)
@[simp]
theorem Complex.sinh_zero :
sinh 0 = 0
@[simp]
theorem Complex.sinh_neg (x : ) :
sinh (-x) = -sinh x
theorem Complex.sinh_add (x y : ) :
sinh (x + y) = sinh x * cosh y + cosh x * sinh y
@[simp]
theorem Complex.cosh_zero :
cosh 0 = 1
@[simp]
theorem Complex.cosh_neg (x : ) :
cosh (-x) = cosh x
theorem Complex.cosh_add (x y : ) :
cosh (x + y) = cosh x * cosh y + sinh x * sinh y
theorem Complex.sinh_sub (x y : ) :
sinh (x - y) = sinh x * cosh y - cosh x * sinh y
theorem Complex.cosh_sub (x y : ) :
cosh (x - y) = cosh x * cosh y - sinh x * sinh y
@[simp]
theorem Complex.ofReal_sinh_ofReal_re (x : ) :
(sinh x).re = sinh x
@[simp]
theorem Complex.ofReal_sinh (x : ) :
(Real.sinh x) = sinh x
@[simp]
theorem Complex.sinh_ofReal_im (x : ) :
(sinh x).im = 0
theorem Complex.ofReal_cosh_ofReal_re (x : ) :
(cosh x).re = cosh x
@[simp]
theorem Complex.ofReal_cosh (x : ) :
(Real.cosh x) = cosh x
@[simp]
theorem Complex.cosh_ofReal_im (x : ) :
(cosh x).im = 0
@[simp]
theorem Complex.cosh_ofReal_re (x : ) :
(cosh x).re = Real.cosh x
@[simp]
theorem Complex.tanh_zero :
tanh 0 = 0
@[simp]
theorem Complex.tanh_neg (x : ) :
tanh (-x) = -tanh x
@[simp]
theorem Complex.ofReal_tanh_ofReal_re (x : ) :
(tanh x).re = tanh x
@[simp]
theorem Complex.ofReal_tanh (x : ) :
(Real.tanh x) = tanh x
@[simp]
theorem Complex.tanh_ofReal_im (x : ) :
(tanh x).im = 0
@[simp]
theorem Complex.cosh_add_sinh (x : ) :
cosh x + sinh x = exp x
@[simp]
theorem Complex.sinh_add_cosh (x : ) :
sinh x + cosh x = exp x
@[simp]
theorem Complex.exp_sub_cosh (x : ) :
exp x - cosh x = sinh x
@[simp]
theorem Complex.exp_sub_sinh (x : ) :
exp x - sinh x = cosh x
@[simp]
theorem Complex.cosh_sub_sinh (x : ) :
cosh x - sinh x = exp (-x)
@[simp]
theorem Complex.sinh_sub_cosh (x : ) :
sinh x - cosh x = -exp (-x)
@[simp]
theorem Complex.cosh_sq_sub_sinh_sq (x : ) :
cosh x ^ 2 - sinh x ^ 2 = 1
theorem Complex.cosh_sq (x : ) :
cosh x ^ 2 = sinh x ^ 2 + 1
theorem Complex.sinh_sq (x : ) :
sinh x ^ 2 = cosh x ^ 2 - 1
theorem Complex.cosh_two_mul (x : ) :
cosh (2 * x) = cosh x ^ 2 + sinh x ^ 2
theorem Complex.sinh_two_mul (x : ) :
sinh (2 * x) = 2 * sinh x * cosh x
theorem Complex.cosh_three_mul (x : ) :
cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x
theorem Complex.sinh_three_mul (x : ) :
sinh (3 * x) = 4 * sinh x ^ 3 + 3 * sinh x
@[simp]
theorem Complex.sin_zero :
sin 0 = 0
@[simp]
theorem Complex.sin_neg (x : ) :
sin (-x) = -sin x
theorem Complex.two_sin (x : ) :
2 * sin x = (exp (-x * I) - exp (x * I)) * I
theorem Complex.two_cos (x : ) :
2 * cos x = exp (x * I) + exp (-x * I)
theorem Complex.sinh_mul_I (x : ) :
sinh (x * I) = sin x * I
theorem Complex.cosh_mul_I (x : ) :
cosh (x * I) = cos x
theorem Complex.tanh_mul_I (x : ) :
tanh (x * I) = tan x * I
theorem Complex.cos_mul_I (x : ) :
cos (x * I) = cosh x
theorem Complex.sin_mul_I (x : ) :
sin (x * I) = sinh x * I
theorem Complex.tan_mul_I (x : ) :
tan (x * I) = tanh x * I
theorem Complex.sin_add (x y : ) :
sin (x + y) = sin x * cos y + cos x * sin y
@[simp]
theorem Complex.cos_zero :
cos 0 = 1
@[simp]
theorem Complex.cos_neg (x : ) :
cos (-x) = cos x
theorem Complex.cos_add (x y : ) :
cos (x + y) = cos x * cos y - sin x * sin y
theorem Complex.sin_sub (x y : ) :
sin (x - y) = sin x * cos y - cos x * sin y
theorem Complex.cos_sub (x y : ) :
cos (x - y) = cos x * cos y + sin x * sin y
theorem Complex.sin_add_mul_I (x y : ) :
sin (x + y * I) = sin x * cosh y + cos x * sinh y * I
theorem Complex.sin_eq (z : ) :
sin z = sin z.re * cosh z.im + cos z.re * sinh z.im * I
theorem Complex.cos_add_mul_I (x y : ) :
cos (x + y * I) = cos x * cosh y - sin x * sinh y * I
theorem Complex.cos_eq (z : ) :
cos z = cos z.re * cosh z.im - sin z.re * sinh z.im * I
theorem Complex.sin_sub_sin (x y : ) :
sin x - sin y = 2 * sin ((x - y) / 2) * cos ((x + y) / 2)
theorem Complex.cos_sub_cos (x y : ) :
cos x - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)
theorem Complex.sin_add_sin (x y : ) :
sin x + sin y = 2 * sin ((x + y) / 2) * cos ((x - y) / 2)
theorem Complex.cos_add_cos (x y : ) :
cos x + cos y = 2 * cos ((x + y) / 2) * cos ((x - y) / 2)
@[simp]
theorem Complex.ofReal_sin_ofReal_re (x : ) :
(sin x).re = sin x
@[simp]
theorem Complex.ofReal_sin (x : ) :
(Real.sin x) = sin x
@[simp]
theorem Complex.sin_ofReal_im (x : ) :
(sin x).im = 0
@[simp]
theorem Complex.ofReal_cos_ofReal_re (x : ) :
(cos x).re = cos x
@[simp]
theorem Complex.ofReal_cos (x : ) :
(Real.cos x) = cos x
@[simp]
theorem Complex.cos_ofReal_im (x : ) :
(cos x).im = 0
@[simp]
theorem Complex.tan_zero :
tan 0 = 0
theorem Complex.tan_mul_cos {x : } (hx : cos x 0) :
tan x * cos x = sin x
@[simp]
theorem Complex.tan_neg (x : ) :
tan (-x) = -tan x
@[simp]
theorem Complex.ofReal_tan_ofReal_re (x : ) :
(tan x).re = tan x
@[simp]
theorem Complex.ofReal_cot_ofReal_re (x : ) :
(↑x).cot.re = (↑x).cot
@[simp]
theorem Complex.ofReal_tan (x : ) :
(Real.tan x) = tan x
@[simp]
theorem Complex.ofReal_cot (x : ) :
x.cot = (↑x).cot
@[simp]
theorem Complex.tan_ofReal_im (x : ) :
(tan x).im = 0
theorem Complex.cos_add_sin_I (x : ) :
cos x + sin x * I = exp (x * I)
theorem Complex.cos_sub_sin_I (x : ) :
cos x - sin x * I = exp (-x * I)
@[simp]
theorem Complex.sin_sq_add_cos_sq (x : ) :
sin x ^ 2 + cos x ^ 2 = 1
@[simp]
theorem Complex.cos_sq_add_sin_sq (x : ) :
cos x ^ 2 + sin x ^ 2 = 1
theorem Complex.cos_two_mul' (x : ) :
cos (2 * x) = cos x ^ 2 - sin x ^ 2
theorem Complex.cos_two_mul (x : ) :
cos (2 * x) = 2 * cos x ^ 2 - 1
theorem Complex.sin_two_mul (x : ) :
sin (2 * x) = 2 * sin x * cos x
theorem Complex.cos_sq (x : ) :
cos x ^ 2 = 1 / 2 + cos (2 * x) / 2
theorem Complex.cos_sq' (x : ) :
cos x ^ 2 = 1 - sin x ^ 2
theorem Complex.sin_sq (x : ) :
sin x ^ 2 = 1 - cos x ^ 2
theorem Complex.inv_one_add_tan_sq {x : } (hx : cos x 0) :
(1 + tan x ^ 2)⁻¹ = cos x ^ 2
theorem Complex.tan_sq_div_one_add_tan_sq {x : } (hx : cos x 0) :
tan x ^ 2 / (1 + tan x ^ 2) = sin x ^ 2
theorem Complex.cos_three_mul (x : ) :
cos (3 * x) = 4 * cos x ^ 3 - 3 * cos x
theorem Complex.sin_three_mul (x : ) :
sin (3 * x) = 3 * sin x - 4 * sin x ^ 3
theorem Complex.exp_mul_I (x : ) :
exp (x * I) = cos x + sin x * I
theorem Complex.exp_add_mul_I (x y : ) :
exp (x + y * I) = exp x * (cos y + sin y * I)
theorem Complex.exp_eq_exp_re_mul_sin_add_cos (x : ) :
exp x = exp x.re * (cos x.im + sin x.im * I)
@[simp]
theorem Complex.exp_ofReal_mul_I_re (x : ) :
(exp (x * I)).re = Real.cos x
@[simp]
theorem Complex.exp_ofReal_mul_I_im (x : ) :
(exp (x * I)).im = Real.sin x
theorem Complex.cos_add_sin_mul_I_pow (n : ) (z : ) :
(cos z + sin z * I) ^ n = cos (n * z) + sin (n * z) * I

De Moivre's formula

@[simp]
theorem Real.sin_zero :
sin 0 = 0
@[simp]
theorem Real.sin_neg (x : ) :
sin (-x) = -sin x
theorem Real.sin_add (x y : ) :
sin (x + y) = sin x * cos y + cos x * sin y
@[simp]
theorem Real.cos_zero :
cos 0 = 1
@[simp]
theorem Real.cos_neg (x : ) :
cos (-x) = cos x
@[simp]
theorem Real.cos_abs (x : ) :
cos |x| = cos x
theorem Real.cos_add (x y : ) :
cos (x + y) = cos x * cos y - sin x * sin y
theorem Real.sin_sub (x y : ) :
sin (x - y) = sin x * cos y - cos x * sin y
theorem Real.cos_sub (x y : ) :
cos (x - y) = cos x * cos y + sin x * sin y
theorem Real.sin_sub_sin (x y : ) :
sin x - sin y = 2 * sin ((x - y) / 2) * cos ((x + y) / 2)
theorem Real.cos_sub_cos (x y : ) :
cos x - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)
theorem Real.cos_add_cos (x y : ) :
cos x + cos y = 2 * cos ((x + y) / 2) * cos ((x - y) / 2)
theorem Real.two_mul_sin_mul_sin (x y : ) :
2 * sin x * sin y = cos (x - y) - cos (x + y)
theorem Real.two_mul_cos_mul_cos (x y : ) :
2 * cos x * cos y = cos (x - y) + cos (x + y)
theorem Real.two_mul_sin_mul_cos (x y : ) :
2 * sin x * cos y = sin (x - y) + sin (x + y)
theorem Real.tan_mul_cos {x : } (hx : cos x 0) :
tan x * cos x = sin x
@[simp]
theorem Real.tan_zero :
tan 0 = 0
@[simp]
theorem Real.tan_neg (x : ) :
tan (-x) = -tan x
@[simp]
theorem Real.sin_sq_add_cos_sq (x : ) :
sin x ^ 2 + cos x ^ 2 = 1
@[simp]
theorem Real.cos_sq_add_sin_sq (x : ) :
cos x ^ 2 + sin x ^ 2 = 1
theorem Real.sin_sq_le_one (x : ) :
sin x ^ 2 1
theorem Real.cos_sq_le_one (x : ) :
cos x ^ 2 1
theorem Real.sin_le_one (x : ) :
sin x 1
theorem Real.cos_le_one (x : ) :
cos x 1
theorem Real.neg_one_le_sin (x : ) :
-1 sin x
theorem Real.neg_one_le_cos (x : ) :
-1 cos x
theorem Real.cos_two_mul (x : ) :
cos (2 * x) = 2 * cos x ^ 2 - 1
theorem Real.cos_two_mul' (x : ) :
cos (2 * x) = cos x ^ 2 - sin x ^ 2
theorem Real.sin_two_mul (x : ) :
sin (2 * x) = 2 * sin x * cos x
theorem Real.cos_sq (x : ) :
cos x ^ 2 = 1 / 2 + cos (2 * x) / 2
theorem Real.cos_sq' (x : ) :
cos x ^ 2 = 1 - sin x ^ 2
theorem Real.sin_sq (x : ) :
sin x ^ 2 = 1 - cos x ^ 2
theorem Real.sin_sq_eq_half_sub (x : ) :
sin x ^ 2 = 1 / 2 - cos (2 * x) / 2
theorem Real.inv_one_add_tan_sq {x : } (hx : cos x 0) :
(1 + tan x ^ 2)⁻¹ = cos x ^ 2
theorem Real.tan_sq_div_one_add_tan_sq {x : } (hx : cos x 0) :
tan x ^ 2 / (1 + tan x ^ 2) = sin x ^ 2
theorem Real.inv_sqrt_one_add_tan_sq {x : } (hx : 0 < cos x) :
((1 + tan x ^ 2))⁻¹ = cos x
theorem Real.tan_div_sqrt_one_add_tan_sq {x : } (hx : 0 < cos x) :
tan x / (1 + tan x ^ 2) = sin x
theorem Real.cos_three_mul (x : ) :
cos (3 * x) = 4 * cos x ^ 3 - 3 * cos x
theorem Real.sin_three_mul (x : ) :
sin (3 * x) = 3 * sin x - 4 * sin x ^ 3
theorem Real.sinh_eq (x : ) :
sinh x = (exp x - exp (-x)) / 2

The definition of sinh in terms of exp.

@[simp]
theorem Real.sinh_zero :
sinh 0 = 0
@[simp]
theorem Real.sinh_neg (x : ) :
sinh (-x) = -sinh x
theorem Real.sinh_add (x y : ) :
sinh (x + y) = sinh x * cosh y + cosh x * sinh y
theorem Real.cosh_eq (x : ) :
cosh x = (exp x + exp (-x)) / 2

The definition of cosh in terms of exp.

@[simp]
theorem Real.cosh_zero :
cosh 0 = 1
@[simp]
theorem Real.cosh_neg (x : ) :
cosh (-x) = cosh x
@[simp]
theorem Real.cosh_abs (x : ) :
theorem Real.cosh_add (x y : ) :
cosh (x + y) = cosh x * cosh y + sinh x * sinh y
theorem Real.sinh_sub (x y : ) :
sinh (x - y) = sinh x * cosh y - cosh x * sinh y
theorem Real.cosh_sub (x y : ) :
cosh (x - y) = cosh x * cosh y - sinh x * sinh y
@[simp]
theorem Real.tanh_zero :
tanh 0 = 0
@[simp]
theorem Real.tanh_neg (x : ) :
tanh (-x) = -tanh x
@[simp]
theorem Real.cosh_add_sinh (x : ) :
cosh x + sinh x = exp x
@[simp]
theorem Real.sinh_add_cosh (x : ) :
sinh x + cosh x = exp x
@[simp]
theorem Real.exp_sub_cosh (x : ) :
exp x - cosh x = sinh x
@[simp]
theorem Real.exp_sub_sinh (x : ) :
exp x - sinh x = cosh x
@[simp]
theorem Real.cosh_sub_sinh (x : ) :
cosh x - sinh x = exp (-x)
@[simp]
theorem Real.sinh_sub_cosh (x : ) :
sinh x - cosh x = -exp (-x)
@[simp]
theorem Real.cosh_sq_sub_sinh_sq (x : ) :
cosh x ^ 2 - sinh x ^ 2 = 1
theorem Real.cosh_sq (x : ) :
cosh x ^ 2 = sinh x ^ 2 + 1
theorem Real.cosh_sq' (x : ) :
cosh x ^ 2 = 1 + sinh x ^ 2
theorem Real.sinh_sq (x : ) :
sinh x ^ 2 = cosh x ^ 2 - 1
theorem Real.cosh_two_mul (x : ) :
cosh (2 * x) = cosh x ^ 2 + sinh x ^ 2
theorem Real.sinh_two_mul (x : ) :
sinh (2 * x) = 2 * sinh x * cosh x
theorem Real.cosh_three_mul (x : ) :
cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x
theorem Real.sinh_three_mul (x : ) :
sinh (3 * x) = 4 * sinh x ^ 3 + 3 * sinh x
theorem Real.cosh_pos (x : ) :
0 < cosh x

Real.cosh is always positive

theorem Real.cos_bound {x : } (hx : |x| 1) :
|cos x - (1 - x ^ 2 / 2)| |x| ^ 4 * (5 / 96)
theorem Real.sin_bound {x : } (hx : |x| 1) :
|sin x - (x - x ^ 3 / 6)| |x| ^ 4 * (5 / 96)
theorem Real.cos_pos_of_le_one {x : } (hx : |x| 1) :
0 < cos x
theorem Real.sin_pos_of_pos_of_le_one {x : } (hx0 : 0 < x) (hx : x 1) :
0 < sin x
theorem Real.sin_pos_of_pos_of_le_two {x : } (hx0 : 0 < x) (hx : x 2) :
0 < sin x
theorem Real.cos_one_le :
cos 1 5 / 9

Extension for the positivity tactic: Real.cosh is always positive.

@[simp]
theorem Complex.norm_cos_add_sin_mul_I (x : ) :
cos x + sin x * I = 1
@[simp]
@[deprecated Complex.norm_cos_add_sin_mul_I (since := "2025-02-16")]
theorem Complex.abs_cos_add_sin_mul_I (x : ) :
cos x + sin x * I = 1

Alias of Complex.norm_cos_add_sin_mul_I.

@[deprecated Complex.norm_exp_ofReal_mul_I (since := "2025-02-16")]
theorem Complex.abs_exp_ofReal_mul_I (x : ) :
exp (x * I) = 1

Alias of Complex.norm_exp_ofReal_mul_I.

@[deprecated Complex.norm_exp (since := "2025-02-16")]

Alias of Complex.norm_exp.

@[deprecated Complex.norm_exp_eq_iff_re_eq (since := "2025-02-16")]

Alias of Complex.norm_exp_eq_iff_re_eq.