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