mathlib3documentation

analysis.special_functions.trigonometric.complex

Complex trigonometric functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Basic facts and derivatives for the complex trigonometric functions.

Several facts about the real trigonometric functions have the proofs deferred here, rather than analysis.special_functions.trigonometric.basic, as they are most easily proved by appealing to the corresponding fact for complex trigonometric functions, or require additional imports which are not available in that file.

theorem complex.cos_eq_zero_iff {θ : } :
= 0 (k : ), θ = (2 * k + 1) * real.pi / 2
theorem complex.cos_ne_zero_iff {θ : } :
0 (k : ), θ (2 * k + 1) * real.pi / 2
theorem complex.sin_eq_zero_iff {θ : } :
= 0 (k : ), θ =
theorem complex.sin_ne_zero_iff {θ : } :
0 (k : ), θ
theorem complex.tan_eq_zero_iff {θ : } :
= 0 (k : ), θ = / 2
theorem complex.tan_ne_zero_iff {θ : } :
0 (k : ), θ / 2
theorem complex.cos_eq_cos_iff {x y : } :
(k : ), y = 2 * k * real.pi + x y = 2 * k * real.pi - x
theorem complex.sin_eq_sin_iff {x y : } :
(k : ), y = 2 * k * real.pi + x y = (2 * k + 1) * real.pi - x
theorem complex.tan_add {x y : } (h : (( (k : ), x (2 * k + 1) * real.pi / 2) (l : ), y (2 * l + 1) * real.pi / 2) ( (k : ), x = (2 * k + 1) * real.pi / 2) (l : ), y = (2 * l + 1) * real.pi / 2) :
complex.tan (x + y) = + / (1 -
theorem complex.tan_add' {x y : } (h : ( (k : ), x (2 * k + 1) * real.pi / 2) (l : ), y (2 * l + 1) * real.pi / 2) :
complex.tan (x + y) = + / (1 -
theorem complex.tan_two_mul {z : } :
complex.tan (2 * z) = 2 * / (1 - ^ 2)
theorem complex.tan_add_mul_I {x y : } (h : (( (k : ), x (2 * k + 1) * real.pi / 2) (l : ), (2 * l + 1) * real.pi / 2) ( (k : ), x = (2 * k + 1) * real.pi / 2) (l : ), = (2 * l + 1) * real.pi / 2) :
complex.tan (x + = / (1 -
theorem complex.tan_eq {z : } (h : (( (k : ), (z.re) (2 * k + 1) * real.pi / 2) (l : ), (z.im) * complex.I (2 * l + 1) * real.pi / 2) ( (k : ), (z.re) = (2 * k + 1) * real.pi / 2) (l : ), (z.im) * complex.I = (2 * l + 1) * real.pi / 2) :
theorem complex.continuous_on_tan  :
{x : | 0}
@[continuity]
theorem complex.continuous_tan  :
continuous (λ (x : {x : | 0}),
theorem complex.cos_eq_iff_quadratic {z w : } :
= w cexp (z * complex.I) ^ 2 - 2 * w * cexp (z * complex.I) + 1 = 0
@[simp]
@[simp]
theorem real.cos_eq_zero_iff {θ : } :
= 0 (k : ), θ = (2 * k + 1) * real.pi / 2
theorem real.cos_ne_zero_iff {θ : } :
0 (k : ), θ (2 * k + 1) * real.pi / 2
theorem real.cos_eq_cos_iff {x y : } :
(k : ), y = 2 * k * real.pi + x y = 2 * k * real.pi - x
theorem real.sin_eq_sin_iff {x y : } :
(k : ), y = 2 * k * real.pi + x y = (2 * k + 1) * real.pi - x
theorem real.lt_sin_mul {x : } (hx : 0 < x) (hx' : x < 1) :
x < real.sin (real.pi / 2 * x)
theorem real.le_sin_mul {x : } (hx : 0 x) (hx' : x 1) :
theorem real.mul_lt_sin {x : } (hx : 0 < x) (hx' : x < ) :
* x <
theorem real.mul_le_sin {x : } (hx : 0 x) (hx' : x ) :
* x

In the range [0, π / 2], we have a linear lower bound on sin. This inequality forms one half of Jordan's inequality, the other half is real.sin_lt