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.tan_int_mul_pi_div_two (n : ℤ) : Complex.tan (↑n * ↑Real.pi / 2) = 0

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) : Complex.tan (x + y) = (Complex.tan x + Complex.tan y) / (1 - Complex.tan x * Complex.tan y)

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) = (Complex.tan x + Complex.tan y) / (1 - Complex.tan x * Complex.tan y)

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) : Complex.tan (x + y * Complex.I) = (Complex.tan x + Complex.tanh y * Complex.I) / (1 - Complex.tan x * Complex.tanh y * Complex.I)

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) : Complex.tan z = (Complex.tan ↑z.re + Complex.tanh ↑z.im * Complex.I) / (1 - Complex.tan ↑z.re * Complex.tanh ↑z.im * Complex.I)

theorem Complex.continuousOn_tan : ContinuousOn Complex.tan {x | Complex.cos x ≠ 0}

theorem Complex.continuous_tan : Continuous fun x => Complex.tan ↑x

theorem Complex.cos_eq_iff_quadratic {z : ℂ} {w : ℂ} : Complex.cos z = w ↔ Complex.exp (z * Complex.I) ^ 2 - 2 * w * Complex.exp (z * Complex.I) + 1 = 0

theorem Complex.cos_surjective : Function.Surjective Complex.cos

@[simp]

theorem Complex.range_cos : Set.range Complex.cos = Set.univ

theorem Complex.sin_surjective : Function.Surjective Complex.sin

@[simp]

theorem Complex.range_sin : Set.range Complex.sin = Set.univ

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) : x ≤ Real.sin (Real.pi / 2 * x)

theorem Real.mul_lt_sin {x : ℝ} (hx : 0 < x) (hx' : x < Real.pi / 2) : 2 / Real.pi * x < Real.sin x

theorem Real.mul_le_sin {x : ℝ} (hx : 0 ≤ x) (hx' : x ≤ Real.pi / 2) : 2 / Real.pi * x ≤ Real.sin 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