mathlib3 documentation

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 {θ : } :
complex.cos θ = 0 (k : ), θ = (2 * k + 1) * real.pi / 2
theorem complex.cos_ne_zero_iff {θ : } :
complex.cos θ 0 (k : ), θ (2 * k + 1) * real.pi / 2
theorem complex.sin_eq_zero_iff {θ : } :
theorem complex.tan_eq_zero_iff {θ : } :
complex.tan θ = 0 (k : ), θ = k * real.pi / 2
theorem complex.tan_ne_zero_iff {θ : } :
theorem complex.sin_eq_sin_iff {x y : } :
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) :
theorem complex.tan_add' {x y : } (h : ( (k : ), x (2 * k + 1) * real.pi / 2) (l : ), y (2 * l + 1) * real.pi / 2) :
theorem complex.tan_two_mul {z : } :
complex.tan (2 * z) = 2 * complex.tan z / (1 - complex.tan z ^ 2)
theorem complex.tan_add_mul_I {x y : } (h : (( (k : ), x (2 * k + 1) * real.pi / 2) (l : ), y * complex.I (2 * l + 1) * real.pi / 2) ( (k : ), x = (2 * k + 1) * real.pi / 2) (l : ), y * complex.I = (2 * l + 1) * real.pi / 2) :
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) :
@[continuity]
theorem complex.continuous_tan  :
continuous (λ (x : {x : | complex.cos x 0}), complex.tan x)
theorem complex.cos_eq_iff_quadratic {z w : } :
complex.cos z = w cexp (z * complex.I) ^ 2 - 2 * w * cexp (z * complex.I) + 1 = 0
theorem real.cos_eq_zero_iff {θ : } :
real.cos θ = 0 (k : ), θ = (2 * k + 1) * real.pi / 2
theorem real.cos_ne_zero_iff {θ : } :
real.cos θ 0 (k : ), θ (2 * k + 1) * real.pi / 2
theorem real.cos_eq_cos_iff {x y : } :
real.cos x = real.cos y (k : ), y = 2 * k * real.pi + x y = 2 * k * real.pi - x
theorem real.sin_eq_sin_iff {x y : } :
real.sin x = real.sin 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 < real.pi / 2) :
theorem real.mul_le_sin {x : } (hx : 0 x) (hx' : x real.pi / 2) :

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