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

@[deprecated Complex.tendsto_norm_tan_of_cos_eq_zero (since := "2025-02-17")]

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

Alias of Complex.tendsto_norm_tan_of_cos_eq_zero.

@[deprecated Complex.tendsto_norm_tan_atTop (since := "2025-02-17")]

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

Alias of Complex.tendsto_norm_tan_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