Complex.hasDerivAt_tan
theorem Complex.hasDerivAt_tan : ∀ {x : ℂ}, x.cos ≠ 0 → HasDerivAt Complex.tan (1 / x.cos ^ 2) x
The theorem `Complex.hasDerivAt_tan` states that for all complex numbers `x`, if the cosine of `x` is not equal to zero, then the complex tangent function has a derivative at `x`, and this derivative is given by `1/(cos(x))^2`. In mathematical terms, it says that if `cos(x) ≠ 0`, then the derivative of `tan(x)` is `1/(cos(x))^2`, where the derivative is taken with respect to `x`.
More concisely: If the cosine of a complex number `x` is non-zero, then the complex tangent function `tan(x)` has a derivative equal to `1/(cos(x))^2`.
|
Complex.tendsto_abs_tan_of_cos_eq_zero
theorem Complex.tendsto_abs_tan_of_cos_eq_zero :
∀ {x : ℂ}, x.cos = 0 → Filter.Tendsto (fun x => Complex.abs x.tan) (nhdsWithin x {x}ᶜ) Filter.atTop
This theorem asserts that for all complex numbers `x` where the complex cosine of `x` equals zero, the absolute value of the complex tangent function, when applied to `x`, tends to infinity. In other words, if you take a sequence of complex numbers converging to `x` and avoid `x` itself (this is what `nhdsWithin x {x}ᶜ` denotes), then the absolute values of their tangents increase without bound (indicated by `Filter.atTop`). This behavior is similar to the real tangent function, which also tends to infinity at the points where the cosine function equals zero.
More concisely: For complex numbers `x` with cosine equal to zero, the absolute value of the tangent function approaches infinity in the neighborhood of `x`.
|