Complex trigonometric functions

Basic facts and derivatives for the complex trigonometric functions.

theorem Complex.hasStrictDerivAt_tan {x : ℂ} (h : Complex.cos x ≠ 0) : HasStrictDerivAt Complex.tan (1 / Complex.cos x ^ 2) x

theorem Complex.hasDerivAt_tan {x : ℂ} (h : Complex.cos x ≠ 0) : HasDerivAt Complex.tan (1 / Complex.cos x ^ 2) x

theorem Complex.tendsto_abs_tan_of_cos_eq_zero {x : ℂ} (hx : Complex.cos x = 0) : Filter.Tendsto (fun (x : ℂ) => Complex.abs (Complex.tan x)) (nhdsWithin x {x}ᶜ) Filter.atTop

theorem Complex.tendsto_abs_tan_atTop (k : ℤ) : Filter.Tendsto (fun (x : ℂ) => Complex.abs (Complex.tan x)) (nhdsWithin ((2 * ↑k + 1) * ↑Real.pi / 2) {(2 * ↑k + 1) * ↑Real.pi / 2}ᶜ) Filter.atTop

@[simp]

theorem Complex.continuousAt_tan {x : ℂ} : ContinuousAt Complex.tan x ↔ Complex.cos x ≠ 0

@[simp]

theorem Complex.differentiableAt_tan {x : ℂ} : DifferentiableAt ℂ Complex.tan x ↔ Complex.cos x ≠ 0

@[simp]

theorem Complex.deriv_tan (x : ℂ) : deriv Complex.tan x = 1 / Complex.cos x ^ 2

@[simp]

theorem Complex.contDiffAt_tan {x : ℂ} {n : WithTop ℕ∞} : ContDiffAt ℂ n Complex.tan x ↔ Complex.cos x ≠ 0