mathlib3 documentation

analysis.special_functions.trigonometric.complex_deriv

Complex trigonometric functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Basic facts and derivatives for the complex trigonometric functions.

source
theorem complex.has_strict_deriv_at_tan {x : ℂ} (h : complex.cos x ≠ 0) :
has_strict_deriv_at complex.tan (1 / complex.cos x ^ 2) x
source
theorem complex.has_deriv_at_tan {x : ℂ} (h : complex.cos x ≠ 0) :
has_deriv_at complex.tan (1 / complex.cos x ^ 2) x
source
theorem complex.tendsto_abs_tan_of_cos_eq_zero {x : ℂ} (hx : complex.cos x = 0) :
filter.tendsto (λ (x : ℂ), ⇑complex.abs (complex.tan x)) (nhds_within x {x}ᶜ) filter.at_top
source
theorem complex.tendsto_abs_tan_at_top (k : ℤ) :
filter.tendsto (λ (x : ℂ), ⇑complex.abs (complex.tan x)) (nhds_within ((2 * ↑k + 1) * ↑real.pi / 2) {(2 * ↑k + 1) * ↑real.pi / 2}ᶜ) filter.at_top
source
@[simp]
theorem complex.continuous_at_tan {x : ℂ} :
continuous_at complex.tan x ↔ complex.cos x ≠ 0
source
@[simp]
theorem complex.differentiable_at_tan {x : ℂ} :
differentiable_at ℂ complex.tan x ↔ complex.cos x ≠ 0
source
@[simp]
theorem complex.deriv_tan (x : ℂ) :
deriv complex.tan x = 1 / complex.cos x ^ 2
source
@[simp]
theorem complex.cont_diff_at_tan {x : ℂ} {n : ℕ∞} :
cont_diff_at ℂ n complex.tan x ↔ complex.cos x ≠ 0