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 = θ

The tangent of a complex number is equal to zero iff this number is equal to k * π / 2 for an integer k.

Note that this lemma takes into account that we use zero as the junk value for division by zero. See also Complex.tan_eq_zero_iff'.

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.tan_eq_zero_iff' {θ : ℂ} (hθ : Complex.cos θ ≠ 0) : Complex.tan θ = 0 ↔ ∃ (k : ℤ), ↑k * ↑Real.pi = θ

If the tangent of a complex number is well-defined, then it is equal to zero iff the number is equal to k * π for an integer k.

See also Complex.tan_eq_zero_iff for a version that takes into account junk values of θ.

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.cos_eq_one_iff {x : ℂ} : Complex.cos x = 1 ↔ ∃ (k : ℤ), ↑k * (2 * ↑Real.pi) = x

theorem Complex.cos_eq_neg_one_iff {x : ℂ} : Complex.cos x = -1 ↔ ∃ (k : ℤ), ↑Real.pi + ↑k * (2 * ↑Real.pi) = x

theorem Complex.sin_eq_one_iff {x : ℂ} : Complex.sin x = 1 ↔ ∃ (k : ℤ), ↑Real.pi / 2 + ↑k * (2 * ↑Real.pi) = x

theorem Complex.sin_eq_neg_one_iff {x : ℂ} : Complex.sin x = -1 ↔ ∃ (k : ℤ), -(↑Real.pi / 2) + ↑k * (2 * ↑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 : ↑{x : ℂ | Complex.cos x ≠ 0}) => 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.cos_eq_neg_one_iff {x : ℝ} : Real.cos x = -1 ↔ ∃ (k : ℤ), Real.pi + ↑k * (2 * Real.pi) = x

theorem Real.sin_eq_one_iff {x : ℝ} : Real.sin x = 1 ↔ ∃ (k : ℤ), Real.pi / 2 + ↑k * (2 * Real.pi) = x

theorem Real.sin_eq_neg_one_iff {x : ℝ} : Real.sin x = -1 ↔ ∃ (k : ℤ), -(Real.pi / 2) + ↑k * (2 * Real.pi) = x

theorem Real.tan_eq_zero_iff {θ : ℝ} : Real.tan θ = 0 ↔ ∃ (k : ℤ), ↑k * Real.pi / 2 = θ

theorem Real.tan_eq_zero_iff' {θ : ℝ} (hθ : Real.cos θ ≠ 0) : Real.tan θ = 0 ↔ ∃ (k : ℤ), ↑k * Real.pi = θ

theorem Real.tan_ne_zero_iff {θ : ℝ} : Real.tan θ ≠ 0 ↔ ∀ (k : ℤ), ↑k * Real.pi / 2 ≠ θ

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