Fungrim home page

Fungrim entry: 14f8c2

atan ⁣(2z)=atan ⁣(z)+atan ⁣(z1+2z2)\operatorname{atan}\!\left(2 z\right) = \operatorname{atan}\!\left(z\right) + \operatorname{atan}\!\left(\frac{z}{1 + 2 {z}^{2}}\right)
Assumptions:zCandnot(Re ⁣(z)=0andIm ⁣(z)[22,1])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
Atanatan ⁣(z)\operatorname{atan}\!\left(z\right) Inverse tangent
Powab{a}^{b} Power
CCC\mathbb{C} Complex numbers
ReRe ⁣(z)\operatorname{Re}\!\left(z\right) Real part
Absz\left|z\right| Absolute value
ImIm ⁣(z)\operatorname{Im}\!\left(z\right) Imaginary part
ClosedInterval[a,b]\left[a, b\right] Closed interval
Sqrtz\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

Copyright (C) Fredrik Johansson and contributors. Fungrim is provided under the MIT license. The source code is on GitHub.

2019-09-16 21:17:18.797188 UTC