Documentation

Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Complex trigonometric functions #

Basic facts and derivatives for the complex trigonometric functions.

Several facts about the real trigonometric functions have the proofs deferred here, rather than Analysis.SpecialFunctions.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 {θ : } :
Complex.sin θ = 0 k, θ = k * Real.pi
theorem Complex.sin_ne_zero_iff {θ : } :
Complex.sin θ 0 ∀ (k : ), θ k * Real.pi
theorem Complex.tan_eq_zero_iff {θ : } :
Complex.tan θ = 0 k, θ = k * Real.pi / 2
theorem Complex.tan_ne_zero_iff {θ : } :
Complex.tan θ 0 ∀ (k : ), θ k * Real.pi / 2
theorem Complex.cos_eq_cos_iff {x : } {y : } :
Complex.cos x = Complex.cos y k, y = 2 * k * Real.pi + x y = 2 * k * Real.pi - x
theorem Complex.sin_eq_sin_iff {x : } {y : } :
Complex.sin x = Complex.sin 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) :
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_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) :
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