Fungrim entry: 14f8c2

\operatorname{atan}\!\left(2 z\right) = \operatorname{atan}\!\left(z\right) + \operatorname{atan}\!\left(\frac{z}{1 + 2 {z}^{2}}\right)

Assumptions:

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \operatorname{not} \left(\operatorname{Re}\!\left(z\right) = 0 \,\mathbin{\operatorname{and}}\, \left|\operatorname{Im}\!\left(z\right)\right| \in \left[\frac{\sqrt{2}}{2}, 1\right]\right)

TeX:

\operatorname{atan}\!\left(2 z\right) = \operatorname{atan}\!\left(z\right) + \operatorname{atan}\!\left(\frac{z}{1 + 2 {z}^{2}}\right)

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\,  \operatorname{not} \left(\operatorname{Re}\!\left(z\right) = 0 \,\mathbin{\operatorname{and}}\, \left|\operatorname{Im}\!\left(z\right)\right| \in \left[\frac{\sqrt{2}}{2}, 1\right]\right)

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Pow`	${a}^{b}$	Power
`CC`	$\mathbb{C}$	Complex numbers
`Re`	$\operatorname{Re}\!\left(z\right)$	Real part
`Abs`	$\left\|z\right\|$	Absolute value
`Im`	$\operatorname{Im}\!\left(z\right)$	Imaginary part
`ClosedInterval`	$\left[a, b\right]$	Closed interval
`Sqrt`	$\sqrt{z}$	Principal square root

Source code for this entry:

Entry(ID("14f8c2"),
    Formula(Equal(Atan(Mul(2, z)), Add(Atan(z), Atan(Div(z, Add(1, Mul(2, Pow(z, 2)))))))),
    Variables(z),
    Assumptions(And(Element(z, CC), Not(And(Equal(Re(z), 0), Element(Abs(Im(z)), ClosedInterval(Div(Sqrt(2), 2), 1)))))))

Topics using this entry

Inverse tangent