Assumptions:
TeX:
\operatorname{atan}''(z) = -\frac{2 z}{{\left(1 + {z}^{2}\right)}^{2}} z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; i z \notin \left(-\infty, -1\right] \cup \left[1, \infty\right)
Definitions:
Fungrim symbol | Notation | Short description |
---|---|---|
ComplexDerivative | Complex derivative | |
Atan | Inverse tangent | |
Pow | Power | |
CC | Complex numbers | |
ConstI | Imaginary unit | |
OpenClosedInterval | Open-closed interval | |
Infinity | Positive infinity | |
ClosedOpenInterval | Closed-open interval |
Source code for this entry:
Entry(ID("a4eb86"), Formula(Equal(ComplexDerivative(Atan(z), For(z, z, 2)), Neg(Div(Mul(2, z), Pow(Add(1, Pow(z, 2)), 2))))), Variables(z), Assumptions(And(Element(z, CC), NotElement(Mul(ConstI, z), Union(OpenClosedInterval(Neg(Infinity), -1), ClosedOpenInterval(1, Infinity))))))