Complex trigonometric functions

Basic facts and derivatives for the complex trigonometric functions.

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Complex.tendsto_tan_div_nhdsNE_zero : Filter.Tendsto (fun (z : ℂ) => tan z / z) (nhdsWithin 0 {0}ᶜ) (nhds 1)

The limit lim_{z → 0} (tan z) / z = 1, for the complex tangent.