Complex trigonometric functions

Basic facts and derivatives for the complex trigonometric functions.

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

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

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

theorem Complex.tendsto_abs_tan_atTop (k : ℤ) : Filter.Tendsto (fun (x : ℂ) => Complex.abs x.tan) (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 ↔ x.cos ≠ 0

@[simp]

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

@[simp]

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

@[simp]

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