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 {θ : ℂ} :

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.continuous_on_tan :

continuous_on complex.tan {x : ℂ | complex.cos x ≠ 0}

@[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 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