Inverse tangent

Symbol: Atan —

\operatorname{atan}\!\left(z\right)

— Inverse tangent

The inverse tangent function

\operatorname{atan}\!\left(z\right)

(denoted by Atan(z) in the Fungrim formula language) is a function of a single variable. The following table lists conditions such that Atan(z) is defined in Fungrim.

Domain	Codomain
Numbers
$z \in \mathbb{R}$	$\operatorname{atan}\!\left(z\right) \in \left(-\frac{\pi}{2}, \frac{\pi}{2}\right)$
$z \in \mathbb{C} \setminus \left\{-i, +i\right\}$	$\operatorname{atan}\!\left(z\right) \in \mathbb{C}$
Infinities
$z \in \left\{-\infty, \infty\right\}$	$\operatorname{atan}\!\left(z\right) \in \left\{-\frac{\pi}{2}, \frac{\pi}{2}\right\}$
$z \in \left\{-i, +i\right\}$	$\operatorname{atan}\!\left(z\right) \in \left\{-i \infty, +i \infty\right\}$
Formal power series
$z \in \mathbb{R}[[x]]$	$\operatorname{atan}\!\left(z\right) \in \mathbb{R}[[x]]$
$z \in \mathbb{C}[[x]] \,\mathbin{\operatorname{and}}\, [{x}^{0}] z \notin \left\{-i, +i\right\}$	$\operatorname{atan}\!\left(z\right) \in \mathbb{C}[[x]]$

Table data:

\left(P, Q\right)

such that

\left(P\right) \implies \left(Q\right)

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`RR`	$\mathbb{R}$	Real numbers
`OpenInterval`	$\left(a, b\right)$	Open interval
`ConstPi`	$\pi$	The constant pi (3.14...)
`CC`	$\mathbb{C}$	Complex numbers
`ConstI`	$i$	Imaginary unit
`Infinity`	$\infty$	Positive infinity
`FormalPowerSeries`	$K[[x]]$	Formal power series

Source code for this entry:

Entry(ID("b120b9"),
    SymbolDefinition(Atan, Atan(z), "Inverse tangent"),
    Description("The inverse tangent function", Atan(z), "(denoted by", SourceForm(Atan(z)), "in the Fungrim formula language)", "is a function of a single variable.", "The following table lists conditions such that", SourceForm(Atan(z)), "is defined in Fungrim."),
    Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(TableSection("Numbers"), Tuple(Element(z, RR), Element(Atan(z), OpenInterval(Neg(Div(ConstPi, 2)), Div(ConstPi, 2)))), Tuple(Element(z, SetMinus(CC, Set(Neg(ConstI), Pos(ConstI)))), Element(Atan(z), CC)), TableSection("Infinities"), Tuple(Element(z, Set(Neg(Infinity), Infinity)), Element(Atan(z), Set(Neg(Div(ConstPi, 2)), Div(ConstPi, 2)))), Tuple(Element(z, Set(Neg(ConstI), Pos(ConstI))), Element(Atan(z), Set(Mul(Neg(ConstI), Infinity), Mul(Pos(ConstI), Infinity)))), TableSection("Formal power series"), Tuple(Element(z, FormalPowerSeries(RR, x)), Element(Atan(z), FormalPowerSeries(RR, x))), Tuple(And(Element(z, FormalPowerSeries(CC, x)), NotElement(SeriesCoefficient(z, x, 0), Set(Neg(ConstI), Pos(ConstI)))), Element(Atan(z), FormalPowerSeries(CC, x))))))

ce3a8e

Symbol: Atan2 —

\operatorname{atan2}\!\left(y, x\right)

— Two-argument inverse tangent

The inverse tangent function

\operatorname{atan2}\!\left(y, x\right)

(denoted by Atan2(y, x) in the Fungrim formula language) is a function of two variables. The following table lists conditions such that Atan2(y, x) is defined in Fungrim.

Domain	Codomain
Numbers
$y \in \mathbb{R} \,\mathbin{\operatorname{and}}\, x \in \mathbb{R}$	$\operatorname{atan2}\!\left(y, x\right) \in \left(-\pi, \pi\right]$

Table data:

\left(P, Q\right)

such that

\left(P\right) \implies \left(Q\right)

Definitions:

Fungrim symbol	Notation	Short description
`Atan2`	$\operatorname{atan2}\!\left(y, x\right)$	Two-argument inverse tangent
`RR`	$\mathbb{R}$	Real numbers
`OpenClosedInterval`	$\left(a, b\right]$	Open-closed interval
`ConstPi`	$\pi$	The constant pi (3.14...)

Source code for this entry:

Entry(ID("ce3a8e"),
    SymbolDefinition(Atan2, Atan2(y, x), "Two-argument inverse tangent"),
    Description("The inverse tangent function", Atan2(y, x), "(denoted by", SourceForm(Atan2(y, x)), "in the Fungrim formula language)", "is a function of two variables.", "The following table lists conditions such that", SourceForm(Atan2(y, x)), "is defined in Fungrim."),
    Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(TableSection("Numbers"), Tuple(And(Element(y, RR), Element(x, RR)), Element(Atan2(y, x), OpenClosedInterval(Neg(ConstPi), ConstPi))))))

8bb3d8

Image: X-ray of

\operatorname{atan}\!\left(z\right)

on

z \in \left[-2, 2\right] + \left[-2, 2\right] i

Download: png (small) — png (medium) — png (large) — pdf (small) — pdf (medium/large) — svg (small) — svg (medium/large)

An X-ray plot illustrates the geometry of a complex analytic function

f\!\left(z\right)

. Thick black curves show where

\operatorname{Im}\!\left(f\!\left(z\right)\right) = 0

(the function is pure real). Thick red curves show where

\operatorname{Re}\!\left(f\!\left(z\right)\right) = 0

(the function is pure imaginary). Points where black and red curves intersect are zeros or poles. Magnitude level curves

\left|f\!\left(z\right)\right| = C

are rendered as thin gray curves, with brighter shades corresponding to larger

C

. Blue lines show branch cuts. The value of the function is continuous with the branch cut on the side indicated with a solid line, and discontinuous on the side indicated with a dashed line. Yellow is used to highlight important regions.

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`ClosedInterval`	$\left[a, b\right]$	Closed interval
`ConstI`	$i$	Imaginary unit
`Im`	$\operatorname{Im}\!\left(z\right)$	Imaginary part
`Re`	$\operatorname{Re}\!\left(z\right)$	Real part
`Abs`	$\left\|z\right\|$	Absolute value

Source code for this entry:

Entry(ID("8bb3d8"),
    Image(Description("X-ray of", Atan(z), "on", Element(z, Add(ClosedInterval(-2, 2), Mul(ClosedInterval(-2, 2), ConstI)))), ImageSource("xray_atan")),
    Description("An X-ray plot illustrates the geometry of a complex analytic function", f(z), ".", "Thick black curves show where", Equal(Im(f(z)), 0), "(the function is pure real).", "Thick red curves show where", Equal(Re(f(z)), 0), "(the function is pure imaginary).", "Points where black and red curves intersect are zeros or poles.", "Magnitude level curves", Equal(Abs(f(z)), C), "are rendered as thin gray curves, with brighter shades corresponding to larger", C, ".", "Blue lines show branch cuts.", "The value of the function is continuous with the branch cut on the side indicated with a solid line, and discontinuous on the side indicated with a dashed line.", "Yellow is used to highlight important regions."))

1f026d

\tan\!\left(\operatorname{atan}\!\left(z\right)\right) = z

Assumptions:

z \in \mathbb{C}

TeX:

\tan\!\left(\operatorname{atan}\!\left(z\right)\right) = z

z \in \mathbb{C}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`CC`	$\mathbb{C}$	Complex numbers

Source code for this entry:

Entry(ID("1f026d"),
    Formula(Equal(Tan(Atan(z)), z)),
    Variables(z),
    Assumptions(Element(z, CC)))

d4b0b6

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

Assumptions:

z \in \mathbb{C} \setminus \left\{-i, i\right\}

TeX:

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

z \in \mathbb{C} \setminus \left\{-i, i\right\}

Definitions:

Fungrim symbol	Notation	Short description
`Sin`	$\sin\!\left(z\right)$	Sine
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Sqrt`	$\sqrt{z}$	Principal square root
`Pow`	${a}^{b}$	Power
`CC`	$\mathbb{C}$	Complex numbers
`ConstI`	$i$	Imaginary unit

Source code for this entry:

Entry(ID("d4b0b6"),
    Formula(Equal(Sin(Atan(z)), Div(z, Sqrt(Add(1, Pow(z, 2)))))),
    Variables(z),
    Assumptions(Element(z, SetMinus(CC, Set(Neg(ConstI), ConstI)))))

0b829e

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

Assumptions:

z \in \mathbb{C} \setminus \left\{-i, i\right\}

TeX:

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

z \in \mathbb{C} \setminus \left\{-i, i\right\}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Sqrt`	$\sqrt{z}$	Principal square root
`Pow`	${a}^{b}$	Power
`CC`	$\mathbb{C}$	Complex numbers
`ConstI`	$i$	Imaginary unit

Source code for this entry:

Entry(ID("0b829e"),
    Formula(Equal(Cos(Atan(z)), Div(1, Sqrt(Add(1, Pow(z, 2)))))),
    Variables(z),
    Assumptions(Element(z, SetMinus(CC, Set(Neg(ConstI), ConstI)))))

f516e3

\operatorname{atan}\!\left(\tan\!\left(\theta\right)\right) = \theta

Assumptions:

\theta \in \mathbb{C} \,\mathbin{\operatorname{and}}\, -\frac{\pi}{2} \lt \operatorname{Re}\!\left(\theta\right) \lt \frac{\pi}{2}

TeX:

\operatorname{atan}\!\left(\tan\!\left(\theta\right)\right) = \theta

\theta \in \mathbb{C} \,\mathbin{\operatorname{and}}\, -\frac{\pi}{2} \lt \operatorname{Re}\!\left(\theta\right) \lt \frac{\pi}{2}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`CC`	$\mathbb{C}$	Complex numbers
`ConstPi`	$\pi$	The constant pi (3.14...)
`Re`	$\operatorname{Re}\!\left(z\right)$	Real part

Source code for this entry:

Entry(ID("f516e3"),
    Formula(Equal(Atan(Tan(theta)), theta)),
    Variables(theta),
    Assumptions(And(Element(theta, CC), Less(Neg(Div(ConstPi, 2)), Re(theta), Div(ConstPi, 2)))))

cbce7f

\mathop{\operatorname{solutions}\,}\limits_{w \in \mathbb{C}} \left[\tan\!\left(w\right) = z\right] = \left\{ \operatorname{atan}\!\left(z\right) + \pi n : n \in \mathbb{Z} \right\}

Assumptions:

z \in \mathbb{C} \setminus \left\{-i, i\right\}

TeX:

\mathop{\operatorname{solutions}\,}\limits_{w \in \mathbb{C}} \left[\tan\!\left(w\right) = z\right] = \left\{ \operatorname{atan}\!\left(z\right) + \pi n : n \in \mathbb{Z} \right\}

z \in \mathbb{C} \setminus \left\{-i, i\right\}

Definitions:

Fungrim symbol	Notation	Short description
`CC`	$\mathbb{C}$	Complex numbers
`SetBuilder`	$\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}$	Set comprehension
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`ConstPi`	$\pi$	The constant pi (3.14...)
`ZZ`	$\mathbb{Z}$	Integers
`ConstI`	$i$	Imaginary unit

Source code for this entry:

Entry(ID("cbce7f"),
    Formula(Equal(Solutions(Brackets(Equal(Tan(w), z)), w, Element(w, CC)), SetBuilder(Add(Atan(z), Mul(ConstPi, n)), n, Element(n, ZZ)))),
    Variables(z),
    Assumptions(Element(z, SetMinus(CC, Set(Neg(ConstI), ConstI)))))

a2af66

\operatorname{atan2}\!\left(y, x\right) = \mathop{\operatorname{solution}\,}\limits_{\theta \in \left(-\pi, \pi\right]} \left[\left(x, y\right) = \left(r \cos\!\left(\theta\right), r \sin\!\left(\theta\right)\right)\; \text{ where } r = \sqrt{{x}^{2} + {y}^{2}}\right]

Assumptions:

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} \,\mathbin{\operatorname{and}}\, \left(x \ne 0 \,\mathbin{\operatorname{or}}\, y \ne 0\right)

TeX:

\operatorname{atan2}\!\left(y, x\right) = \mathop{\operatorname{solution}\,}\limits_{\theta \in \left(-\pi, \pi\right]} \left[\left(x, y\right) = \left(r \cos\!\left(\theta\right), r \sin\!\left(\theta\right)\right)\; \text{ where } r = \sqrt{{x}^{2} + {y}^{2}}\right]

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} \,\mathbin{\operatorname{and}}\, \left(x \ne 0 \,\mathbin{\operatorname{or}}\, y \ne 0\right)

Definitions:

Fungrim symbol	Notation	Short description
`Atan2`	$\operatorname{atan2}\!\left(y, x\right)$	Two-argument inverse tangent
`Sin`	$\sin\!\left(z\right)$	Sine
`Sqrt`	$\sqrt{z}$	Principal square root
`Pow`	${a}^{b}$	Power
`OpenClosedInterval`	$\left(a, b\right]$	Open-closed interval
`ConstPi`	$\pi$	The constant pi (3.14...)
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("a2af66"),
    Formula(Equal(Atan2(y, x), UniqueSolution(Brackets(Where(Equal(Tuple(x, y), Tuple(Mul(r, Cos(theta)), Mul(r, Sin(theta)))), Equal(r, Sqrt(Add(Pow(x, 2), Pow(y, 2)))))), theta, Element(theta, OpenClosedInterval(Neg(ConstPi), ConstPi))))),
    Variables(x, y),
    Assumptions(And(Element(x, RR), Element(y, RR), Or(Unequal(x, 0), Unequal(y, 0)))))

61d8f3

\left(1 + {z}^{2}\right) y''(z) + 2 z y'(z) = 0\; \text{ where } y\!\left(z\right) = {c}_{1} + {c}_{2} \operatorname{atan}\!\left(z\right)

Assumptions:

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, {c}_{1} \in \mathbb{C} \,\mathbin{\operatorname{and}}\, {c}_{2} \in \mathbb{C} \,\mathbin{\operatorname{and}}\, i z \notin \left(-\infty, -1\right] \cup \left[1, \infty\right)

TeX:

\left(1 + {z}^{2}\right) y''(z) + 2 z y'(z) = 0\; \text{ where } y\!\left(z\right) = {c}_{1} + {c}_{2} \operatorname{atan}\!\left(z\right)

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, {c}_{1} \in \mathbb{C} \,\mathbin{\operatorname{and}}\, {c}_{2} \in \mathbb{C} \,\mathbin{\operatorname{and}}\, i z \notin \left(-\infty, -1\right] \cup \left[1, \infty\right)

Definitions:

Fungrim symbol	Notation	Short description
`Pow`	${a}^{b}$	Power
`Derivative`	$\frac{d}{d z}\, f\!\left(z\right)$	Derivative
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`CC`	$\mathbb{C}$	Complex numbers
`ConstI`	$i$	Imaginary unit
`OpenClosedInterval`	$\left(a, b\right]$	Open-closed interval
`Infinity`	$\infty$	Positive infinity
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval

Source code for this entry:

Entry(ID("61d8f3"),
    Formula(Where(Equal(Add(Mul(Add(1, Pow(z, 2)), Derivative(y(z), Tuple(z, z, 2))), Mul(Mul(2, z), Derivative(y(z), Tuple(z, z, 1)))), 0), Equal(y(z), Add(Subscript(c, 1), Mul(Subscript(c, 2), Atan(z)))))),
    Variables(z, Subscript(c, 1), Subscript(c, 2)),
    Assumptions(And(Element(z, CC), Element(Subscript(c, 1), CC), Element(Subscript(c, 2), CC), NotElement(Mul(ConstI, z), Union(OpenClosedInterval(Neg(Infinity), -1), ClosedOpenInterval(1, Infinity))))))

90a864

\operatorname{atan}\!\left(z\right) = \int_{0}^{z} \frac{1}{1 + {t}^{2}} \, dt

Assumptions:

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, i z \notin \left(-\infty, -1\right] \cup \left[1, \infty\right)

TeX:

\operatorname{atan}\!\left(z\right) = \int_{0}^{z} \frac{1}{1 + {t}^{2}} \, dt

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
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Pow`	${a}^{b}$	Power
`CC`	$\mathbb{C}$	Complex numbers
`ConstI`	$i$	Imaginary unit
`OpenClosedInterval`	$\left(a, b\right]$	Open-closed interval
`Infinity`	$\infty$	Positive infinity
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval

Source code for this entry:

Entry(ID("90a864"),
    Formula(Equal(Atan(z), Integral(Div(1, Add(1, Pow(t, 2))), Tuple(t, 0, z)))),
    Variables(z),
    Assumptions(And(Element(z, CC), NotElement(Mul(ConstI, z), Union(OpenClosedInterval(Neg(Infinity), -1), ClosedOpenInterval(1, Infinity))))))

645e30

\operatorname{atan}\!\left(0\right) = 0

TeX:

\operatorname{atan}\!\left(0\right) = 0

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent

Source code for this entry:

Entry(ID("645e30"),
    Formula(Equal(Atan(0), 0)))

d418d3

\operatorname{atan}\!\left(+\infty\right) = \frac{\pi}{2}

TeX:

\operatorname{atan}\!\left(+\infty\right) = \frac{\pi}{2}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Infinity`	$\infty$	Positive infinity
`ConstPi`	$\pi$	The constant pi (3.14...)

Source code for this entry:

Entry(ID("d418d3"),
    Formula(Equal(Atan(Pos(Infinity)), Div(ConstPi, 2))))

7295b5

\operatorname{atan}\!\left(-\infty\right) = -\frac{\pi}{2}

TeX:

\operatorname{atan}\!\left(-\infty\right) = -\frac{\pi}{2}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Infinity`	$\infty$	Positive infinity
`ConstPi`	$\pi$	The constant pi (3.14...)

Source code for this entry:

Entry(ID("7295b5"),
    Formula(Equal(Atan(Neg(Infinity)), Neg(Div(ConstPi, 2)))))

a2d208

\operatorname{atan}\!\left(+i\right) = +i \infty

TeX:

\operatorname{atan}\!\left(+i\right) = +i \infty

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`ConstI`	$i$	Imaginary unit
`Infinity`	$\infty$	Positive infinity

Source code for this entry:

Entry(ID("a2d208"),
    Formula(Equal(Atan(Pos(ConstI)), Mul(Pos(ConstI), Infinity))))

9b0994

\operatorname{atan}\!\left(-i\right) = -i \infty

TeX:

\operatorname{atan}\!\left(-i\right) = -i \infty

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`ConstI`	$i$	Imaginary unit
`Infinity`	$\infty$	Positive infinity

Source code for this entry:

Entry(ID("9b0994"),
    Formula(Equal(Atan(Neg(ConstI)), Mul(Neg(ConstI), Infinity))))

157c6c

\operatorname{atan}\!\left(1\right) = \frac{\pi}{4}

TeX:

\operatorname{atan}\!\left(1\right) = \frac{\pi}{4}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`ConstPi`	$\pi$	The constant pi (3.14...)

Source code for this entry:

Entry(ID("157c6c"),
    Formula(Equal(Atan(1), Div(ConstPi, 4))))

706783

\operatorname{atan}\!\left(\sqrt{3}\right) = \frac{\pi}{3}

TeX:

\operatorname{atan}\!\left(\sqrt{3}\right) = \frac{\pi}{3}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Sqrt`	$\sqrt{z}$	Principal square root
`ConstPi`	$\pi$	The constant pi (3.14...)

Source code for this entry:

Entry(ID("706783"),
    Formula(Equal(Atan(Sqrt(3)), Div(ConstPi, 3))))

3c1021

\operatorname{atan}\!\left(\frac{1}{\sqrt{3}}\right) = \frac{\pi}{6}

TeX:

\operatorname{atan}\!\left(\frac{1}{\sqrt{3}}\right) = \frac{\pi}{6}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Sqrt`	$\sqrt{z}$	Principal square root
`ConstPi`	$\pi$	The constant pi (3.14...)

Source code for this entry:

Entry(ID("3c1021"),
    Formula(Equal(Atan(Div(1, Sqrt(3))), Div(ConstPi, 6))))

a9ecff

\operatorname{atan}\!\left(\sqrt{2} - 1\right) = \frac{\pi}{8}

TeX:

\operatorname{atan}\!\left(\sqrt{2} - 1\right) = \frac{\pi}{8}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Sqrt`	$\sqrt{z}$	Principal square root
`ConstPi`	$\pi$	The constant pi (3.14...)

Source code for this entry:

Entry(ID("a9ecff"),
    Formula(Equal(Atan(Sub(Sqrt(2), 1)), Div(ConstPi, 8))))

c6c92a

\operatorname{atan}\!\left(\sqrt{2} + 1\right) = \frac{3 \pi}{8}

TeX:

\operatorname{atan}\!\left(\sqrt{2} + 1\right) = \frac{3 \pi}{8}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Sqrt`	$\sqrt{z}$	Principal square root
`ConstPi`	$\pi$	The constant pi (3.14...)

Source code for this entry:

Entry(ID("c6c92a"),
    Formula(Equal(Atan(Add(Sqrt(2), 1)), Div(Mul(3, ConstPi), 8))))

7dd050

\operatorname{atan}\!\left(2 - \sqrt{3}\right) = \frac{\pi}{12}

TeX:

\operatorname{atan}\!\left(2 - \sqrt{3}\right) = \frac{\pi}{12}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Sqrt`	$\sqrt{z}$	Principal square root
`ConstPi`	$\pi$	The constant pi (3.14...)

Source code for this entry:

Entry(ID("7dd050"),
    Formula(Equal(Atan(Sub(2, Sqrt(3))), Div(ConstPi, 12))))

b0049f

\operatorname{atan}\!\left(2 + \sqrt{3}\right) = \frac{5 \pi}{12}

TeX:

\operatorname{atan}\!\left(2 + \sqrt{3}\right) = \frac{5 \pi}{12}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Sqrt`	$\sqrt{z}$	Principal square root
`ConstPi`	$\pi$	The constant pi (3.14...)

Source code for this entry:

Entry(ID("b0049f"),
    Formula(Equal(Atan(Add(2, Sqrt(3))), Div(Mul(5, ConstPi), 12))))

a6cd13

\operatorname{HolomorphicDomain}\!\left(\operatorname{atan}\!\left(z\right), z, \mathbb{C} \cup \left\{{\tilde \infty}\right\}\right) = \mathbb{C} \setminus \left(-\infty, -1\right] \cup \left[1, \infty\right)

TeX:

\operatorname{HolomorphicDomain}\!\left(\operatorname{atan}\!\left(z\right), z, \mathbb{C} \cup \left\{{\tilde \infty}\right\}\right) = \mathbb{C} \setminus \left(-\infty, -1\right] \cup \left[1, \infty\right)

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`CC`	$\mathbb{C}$	Complex numbers
`UnsignedInfinity`	${\tilde \infty}$	Unsigned infinity
`OpenClosedInterval`	$\left(a, b\right]$	Open-closed interval
`Infinity`	$\infty$	Positive infinity
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval

Source code for this entry:

Entry(ID("a6cd13"),
    Formula(Equal(HolomorphicDomain(Atan(z), z, Union(CC, Set(UnsignedInfinity))), SetMinus(CC, Union(OpenClosedInterval(Neg(Infinity), -1), ClosedOpenInterval(1, Infinity))))))

30ba67

\operatorname{EssentialSingularities}\!\left(\operatorname{atan}\!\left(z\right), z, \mathbb{C} \cup \left\{{\tilde \infty}\right\}\right) = \left\{\right\}

TeX:

\operatorname{EssentialSingularities}\!\left(\operatorname{atan}\!\left(z\right), z, \mathbb{C} \cup \left\{{\tilde \infty}\right\}\right) = \left\{\right\}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`CC`	$\mathbb{C}$	Complex numbers
`UnsignedInfinity`	${\tilde \infty}$	Unsigned infinity

Source code for this entry:

Entry(ID("30ba67"),
    Formula(Equal(EssentialSingularities(Atan(z), z, Union(CC, Set(UnsignedInfinity))), Set())))

48031d

\operatorname{Poles}\!\left(\operatorname{atan}\!\left(z\right), z, \mathbb{C} \cup \left\{{\tilde \infty}\right\}\right) = \left\{\right\}

TeX:

\operatorname{Poles}\!\left(\operatorname{atan}\!\left(z\right), z, \mathbb{C} \cup \left\{{\tilde \infty}\right\}\right) = \left\{\right\}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`CC`	$\mathbb{C}$	Complex numbers
`UnsignedInfinity`	${\tilde \infty}$	Unsigned infinity

Source code for this entry:

Entry(ID("48031d"),
    Formula(Equal(Poles(Atan(z), z, Union(CC, Set(UnsignedInfinity))), Set())))

26c47c

\operatorname{BranchPoints}\!\left(\operatorname{atan}\!\left(z\right), z, \mathbb{C} \cup \left\{{\tilde \infty}\right\}\right) = \left\{-i, i, {\tilde \infty}\right\}

TeX:

\operatorname{BranchPoints}\!\left(\operatorname{atan}\!\left(z\right), z, \mathbb{C} \cup \left\{{\tilde \infty}\right\}\right) = \left\{-i, i, {\tilde \infty}\right\}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`CC`	$\mathbb{C}$	Complex numbers
`UnsignedInfinity`	${\tilde \infty}$	Unsigned infinity
`ConstI`	$i$	Imaginary unit

Source code for this entry:

Entry(ID("26c47c"),
    Formula(Equal(BranchPoints(Atan(z), z, Union(CC, Set(UnsignedInfinity))), Set(Neg(ConstI), ConstI, UnsignedInfinity))))

3b11d3

\operatorname{BranchCuts}\!\left(\operatorname{atan}\!\left(z\right), z, \mathbb{C}\right) = \left\{\left(-\infty, -1\right] i, \left[1, \infty\right) i\right\}

TeX:

\operatorname{BranchCuts}\!\left(\operatorname{atan}\!\left(z\right), z, \mathbb{C}\right) = \left\{\left(-\infty, -1\right] i, \left[1, \infty\right) i\right\}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`CC`	$\mathbb{C}$	Complex numbers
`OpenClosedInterval`	$\left(a, b\right]$	Open-closed interval
`Infinity`	$\infty$	Positive infinity
`ConstI`	$i$	Imaginary unit
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval

Source code for this entry:

Entry(ID("3b11d3"),
    Formula(Equal(BranchCuts(Atan(z), z, CC), Set(Mul(OpenClosedInterval(Neg(Infinity), -1), ConstI), Mul(ClosedOpenInterval(1, Infinity), ConstI)))))

718a9b

\mathop{\operatorname{zeros}\,}\limits_{z \in \mathbb{C}} \operatorname{atan}\!\left(z\right) = \left\{0\right\}

TeX:

\mathop{\operatorname{zeros}\,}\limits_{z \in \mathbb{C}} \operatorname{atan}\!\left(z\right) = \left\{0\right\}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`CC`	$\mathbb{C}$	Complex numbers

Source code for this entry:

Entry(ID("718a9b"),
    Formula(Equal(Zeros(Atan(z), z, Element(z, CC)), Set(0))))

0ee626

\operatorname{atan}\!\left(-z\right) = -\operatorname{atan}\!\left(z\right)

Assumptions:

z \in \mathbb{C} \cup \left\{-\infty, \infty\right\}

TeX:

\operatorname{atan}\!\left(-z\right) = -\operatorname{atan}\!\left(z\right)

z \in \mathbb{C} \cup \left\{-\infty, \infty\right\}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`CC`	$\mathbb{C}$	Complex numbers
`Infinity`	$\infty$	Positive infinity

Source code for this entry:

Entry(ID("0ee626"),
    Formula(Equal(Atan(Neg(z)), Neg(Atan(z)))),
    Variables(z),
    Assumptions(Element(z, Union(CC, Set(Neg(Infinity), Infinity)))))

632063

\operatorname{atan}\!\left(\overline{z}\right) = \overline{\operatorname{atan}\!\left(z\right)}

Assumptions:

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, i z \notin \left(-\infty, -1\right) \cup \left(1, \infty\right)

TeX:

\operatorname{atan}\!\left(\overline{z}\right) = \overline{\operatorname{atan}\!\left(z\right)}

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
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Conjugate`	$\overline{z}$	Complex conjugate
`CC`	$\mathbb{C}$	Complex numbers
`ConstI`	$i$	Imaginary unit
`OpenInterval`	$\left(a, b\right)$	Open interval
`Infinity`	$\infty$	Positive infinity

Source code for this entry:

Entry(ID("632063"),
    Formula(Equal(Atan(Conjugate(z)), Conjugate(Atan(z)))),
    Variables(z),
    Assumptions(And(Element(z, CC), NotElement(Mul(ConstI, z), Union(OpenInterval(Neg(Infinity), -1), OpenInterval(1, Infinity))))))

e3d274

\operatorname{atan}\!\left(\frac{1}{z}\right) = \frac{\pi}{2} - \operatorname{atan}\!\left(z\right)

Assumptions:

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \left(\operatorname{Re}\!\left(z\right) \gt 0 \,\mathbin{\operatorname{or}}\, \left(\operatorname{Re}\!\left(z\right) = 0 \,\mathbin{\operatorname{and}}\, \operatorname{Im}\!\left(z\right) \in \left(-1, 0\right) \cup \left(1, \infty\right)\right)\right)

TeX:

\operatorname{atan}\!\left(\frac{1}{z}\right) = \frac{\pi}{2} - \operatorname{atan}\!\left(z\right)

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \left(\operatorname{Re}\!\left(z\right) \gt 0 \,\mathbin{\operatorname{or}}\, \left(\operatorname{Re}\!\left(z\right) = 0 \,\mathbin{\operatorname{and}}\, \operatorname{Im}\!\left(z\right) \in \left(-1, 0\right) \cup \left(1, \infty\right)\right)\right)

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`ConstPi`	$\pi$	The constant pi (3.14...)
`CC`	$\mathbb{C}$	Complex numbers
`Re`	$\operatorname{Re}\!\left(z\right)$	Real part
`Im`	$\operatorname{Im}\!\left(z\right)$	Imaginary part
`OpenInterval`	$\left(a, b\right)$	Open interval
`Infinity`	$\infty$	Positive infinity

Source code for this entry:

Entry(ID("e3d274"),
    Formula(Equal(Atan(Div(1, z)), Sub(Div(ConstPi, 2), Atan(z)))),
    Variables(z),
    Assumptions(And(Element(z, CC), Or(Greater(Re(z), 0), And(Equal(Re(z), 0), Element(Im(z), Union(OpenInterval(-1, 0), OpenInterval(1, Infinity))))))))

073e1a

\operatorname{atan}\!\left(\frac{1}{z}\right) = -\frac{\pi}{2} - \operatorname{atan}\!\left(z\right)

Assumptions:

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \left(\operatorname{Re}\!\left(z\right) \lt 0 \,\mathbin{\operatorname{or}}\, \left(\operatorname{Re}\!\left(z\right) = 0 \,\mathbin{\operatorname{and}}\, \operatorname{Im}\!\left(z\right) \in \left(-\infty, -1\right) \cup \left(0, 1\right)\right)\right)

TeX:

\operatorname{atan}\!\left(\frac{1}{z}\right) = -\frac{\pi}{2} - \operatorname{atan}\!\left(z\right)

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \left(\operatorname{Re}\!\left(z\right) \lt 0 \,\mathbin{\operatorname{or}}\, \left(\operatorname{Re}\!\left(z\right) = 0 \,\mathbin{\operatorname{and}}\, \operatorname{Im}\!\left(z\right) \in \left(-\infty, -1\right) \cup \left(0, 1\right)\right)\right)

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`ConstPi`	$\pi$	The constant pi (3.14...)
`CC`	$\mathbb{C}$	Complex numbers
`Re`	$\operatorname{Re}\!\left(z\right)$	Real part
`Im`	$\operatorname{Im}\!\left(z\right)$	Imaginary part
`OpenInterval`	$\left(a, b\right)$	Open interval
`Infinity`	$\infty$	Positive infinity

Source code for this entry:

Entry(ID("073e1a"),
    Formula(Equal(Atan(Div(1, z)), Sub(Neg(Div(ConstPi, 2)), Atan(z)))),
    Variables(z),
    Assumptions(And(Element(z, CC), Or(Less(Re(z), 0), And(Equal(Re(z), 0), Element(Im(z), Union(OpenInterval(Neg(Infinity), -1), OpenInterval(0, 1))))))))

bfc13f

\operatorname{atan}\!\left(\frac{1}{z}\right) = \frac{\pi}{2} \operatorname{csgn}\!\left(\frac{1}{z}\right) - \operatorname{atan}\!\left(z\right)

Assumptions:

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, i z \notin \left\{0\right\} \cup \left(-\infty, -1\right] \cup \left[1, \infty\right)

TeX:

\operatorname{atan}\!\left(\frac{1}{z}\right) = \frac{\pi}{2} \operatorname{csgn}\!\left(\frac{1}{z}\right) - \operatorname{atan}\!\left(z\right)

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, i z \notin \left\{0\right\} \cup \left(-\infty, -1\right] \cup \left[1, \infty\right)

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`ConstPi`	$\pi$	The constant pi (3.14...)
`CC`	$\mathbb{C}$	Complex numbers
`ConstI`	$i$	Imaginary unit
`OpenClosedInterval`	$\left(a, b\right]$	Open-closed interval
`Infinity`	$\infty$	Positive infinity
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval

Source code for this entry:

Entry(ID("bfc13f"),
    Formula(Equal(Atan(Div(1, z)), Sub(Mul(Div(ConstPi, 2), Csgn(Div(1, z))), Atan(z)))),
    Variables(z),
    Assumptions(And(Element(z, CC), NotElement(Mul(ConstI, z), Union(Set(0), OpenClosedInterval(Neg(Infinity), -1), ClosedOpenInterval(1, Infinity))))))

072166

\operatorname{atan}\!\left(i z\right) = i \operatorname{atanh}\!\left(z\right)

Assumptions:

z \in \mathbb{C}

TeX:

\operatorname{atan}\!\left(i z\right) = i \operatorname{atanh}\!\left(z\right)

z \in \mathbb{C}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`ConstI`	$i$	Imaginary unit
`CC`	$\mathbb{C}$	Complex numbers

Source code for this entry:

Entry(ID("072166"),
    Formula(Equal(Atan(Mul(ConstI, z)), Mul(ConstI, Atanh(z)))),
    Variables(z),
    Assumptions(Element(z, CC)))

268c9e

\operatorname{atan}\!\left(x + y\right) = \operatorname{atan}\!\left(x\right) + \operatorname{atan}\!\left(\frac{y}{1 + x \left(x + y\right)}\right)

Assumptions:

x \in \mathbb{C} \,\mathbin{\operatorname{and}}\, y \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \left|x + y\right| \lt 1 \,\mathbin{\operatorname{and}}\, \left|x\right| \lt 1

Alternative assumptions:

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} \,\mathbin{\operatorname{and}}\, x \left(x + y\right) \gt -1

TeX:

\operatorname{atan}\!\left(x + y\right) = \operatorname{atan}\!\left(x\right) + \operatorname{atan}\!\left(\frac{y}{1 + x \left(x + y\right)}\right)

x \in \mathbb{C} \,\mathbin{\operatorname{and}}\, y \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \left|x + y\right| \lt 1 \,\mathbin{\operatorname{and}}\, \left|x\right| \lt 1

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} \,\mathbin{\operatorname{and}}\, x \left(x + y\right) \gt -1

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`CC`	$\mathbb{C}$	Complex numbers
`Abs`	$\left\|z\right\|$	Absolute value
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("268c9e"),
    Formula(Equal(Atan(Add(x, y)), Add(Atan(x), Atan(Div(y, Add(1, Mul(x, Add(x, y)))))))),
    Variables(x, y),
    Assumptions(And(Element(x, CC), Element(y, CC), Less(Abs(Add(x, y)), 1), Less(Abs(x), 1)), And(Element(x, RR), Element(y, RR), Greater(Mul(x, Add(x, y)), -1))))

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)))))))

67c0be

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

Assumptions:

z \in \mathbb{C}

TeX:

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

z \in \mathbb{C}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Sqrt`	$\sqrt{z}$	Principal square root
`Pow`	${a}^{b}$	Power
`CC`	$\mathbb{C}$	Complex numbers

Source code for this entry:

Entry(ID("67c0be"),
    Formula(Equal(Atan(z), Mul(2, Atan(Div(z, Add(1, Sqrt(Add(1, Pow(z, 2))))))))),
    Variables(z),
    Assumptions(Element(z, CC)))

cf64b3

\operatorname{atan}\!\left(x\right) + \operatorname{atan}\!\left(y\right) = \operatorname{atan2}\!\left(x + y, 1 - x y\right)

Assumptions:

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R}

TeX:

\operatorname{atan}\!\left(x\right) + \operatorname{atan}\!\left(y\right) = \operatorname{atan2}\!\left(x + y, 1 - x y\right)

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Atan2`	$\operatorname{atan2}\!\left(y, x\right)$	Two-argument inverse tangent
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("cf64b3"),
    Formula(Equal(Add(Atan(x), Atan(y)), Atan2(Add(x, y), Sub(1, Mul(x, y))))),
    Variables(x, y),
    Assumptions(And(Element(x, RR), Element(y, RR))))

00e608

\operatorname{atan}\!\left(x\right) - \operatorname{atan}\!\left(y\right) = \operatorname{atan2}\!\left(x - y, 1 + x y\right)

Assumptions:

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R}

TeX:

\operatorname{atan}\!\left(x\right) - \operatorname{atan}\!\left(y\right) = \operatorname{atan2}\!\left(x - y, 1 + x y\right)

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Atan2`	$\operatorname{atan2}\!\left(y, x\right)$	Two-argument inverse tangent
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("00e608"),
    Formula(Equal(Sub(Atan(x), Atan(y)), Atan2(Sub(x, y), Add(1, Mul(x, y))))),
    Variables(x, y),
    Assumptions(And(Element(x, RR), Element(y, RR))))

3ea11b

\operatorname{atan}\!\left(x\right) + \operatorname{atan}\!\left(y\right) = \operatorname{atan}\!\left(\frac{x + y}{1 - x y}\right)

Assumptions:

x \in \mathbb{C} \,\mathbin{\operatorname{and}}\, y \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \left|x\right| \lt 1 \,\mathbin{\operatorname{and}}\, \left|y\right| \lt 1

Alternative assumptions:

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} \,\mathbin{\operatorname{and}}\, x y \lt 1

TeX:

\operatorname{atan}\!\left(x\right) + \operatorname{atan}\!\left(y\right) = \operatorname{atan}\!\left(\frac{x + y}{1 - x y}\right)

x \in \mathbb{C} \,\mathbin{\operatorname{and}}\, y \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \left|x\right| \lt 1 \,\mathbin{\operatorname{and}}\, \left|y\right| \lt 1

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} \,\mathbin{\operatorname{and}}\, x y \lt 1

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`CC`	$\mathbb{C}$	Complex numbers
`Abs`	$\left\|z\right\|$	Absolute value
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("3ea11b"),
    Formula(Equal(Add(Atan(x), Atan(y)), Atan(Div(Add(x, y), Sub(1, Mul(x, y)))))),
    Variables(x, y),
    Assumptions(And(Element(x, CC), Element(y, CC), Less(Abs(x), 1), Less(Abs(y), 1)), And(Element(x, RR), Element(y, RR), Less(Mul(x, y), 1))))

503d4d

\operatorname{atan}\!\left(x\right) - \operatorname{atan}\!\left(y\right) = \operatorname{atan}\!\left(\frac{x - y}{1 + x y}\right)

Assumptions:

x \in \mathbb{C} \,\mathbin{\operatorname{and}}\, y \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \left|x\right| \lt 1 \,\mathbin{\operatorname{and}}\, \left|y\right| \lt 1

Alternative assumptions:

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} \,\mathbin{\operatorname{and}}\, x y \gt -1

TeX:

\operatorname{atan}\!\left(x\right) - \operatorname{atan}\!\left(y\right) = \operatorname{atan}\!\left(\frac{x - y}{1 + x y}\right)

x \in \mathbb{C} \,\mathbin{\operatorname{and}}\, y \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \left|x\right| \lt 1 \,\mathbin{\operatorname{and}}\, \left|y\right| \lt 1

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} \,\mathbin{\operatorname{and}}\, x y \gt -1

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`CC`	$\mathbb{C}$	Complex numbers
`Abs`	$\left\|z\right\|$	Absolute value
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("503d4d"),
    Formula(Equal(Sub(Atan(x), Atan(y)), Atan(Div(Sub(x, y), Add(1, Mul(x, y)))))),
    Variables(x, y),
    Assumptions(And(Element(x, CC), Element(y, CC), Less(Abs(x), 1), Less(Abs(y), 1)), And(Element(x, RR), Element(y, RR), Greater(Mul(x, y), -1))))

a020e9

\operatorname{atan2}\!\left({y}_{1}, {x}_{1}\right) + \operatorname{atan2}\!\left({y}_{2}, {x}_{2}\right) = \operatorname{atan2}\!\left({y}_{1} {x}_{2} + {y}_{2} {x}_{1}, {x}_{1} {x}_{2} - {y}_{1} {y}_{2}\right)

Assumptions:

{x}_{1} \in \mathbb{R} \,\mathbin{\operatorname{and}}\, {x}_{2} \in \mathbb{R} \,\mathbin{\operatorname{and}}\, {y}_{1} \in \mathbb{R} \,\mathbin{\operatorname{and}}\, {y}_{2} \in \mathbb{R} \,\mathbin{\operatorname{and}}\, \operatorname{atan2}\!\left({y}_{1}, {x}_{1}\right) + \operatorname{atan2}\!\left({y}_{2}, {x}_{2}\right) \in \left(-\pi, \pi\right] \,\mathbin{\operatorname{and}}\, \operatorname{not} \left({x}_{1} = {y}_{1} = 0\right) \,\mathbin{\operatorname{and}}\, \operatorname{not} \left({x}_{2} = {y}_{2} = 0\right)

TeX:

\operatorname{atan2}\!\left({y}_{1}, {x}_{1}\right) + \operatorname{atan2}\!\left({y}_{2}, {x}_{2}\right) = \operatorname{atan2}\!\left({y}_{1} {x}_{2} + {y}_{2} {x}_{1}, {x}_{1} {x}_{2} - {y}_{1} {y}_{2}\right)

{x}_{1} \in \mathbb{R} \,\mathbin{\operatorname{and}}\, {x}_{2} \in \mathbb{R} \,\mathbin{\operatorname{and}}\, {y}_{1} \in \mathbb{R} \,\mathbin{\operatorname{and}}\, {y}_{2} \in \mathbb{R} \,\mathbin{\operatorname{and}}\, \operatorname{atan2}\!\left({y}_{1}, {x}_{1}\right) + \operatorname{atan2}\!\left({y}_{2}, {x}_{2}\right) \in \left(-\pi, \pi\right] \,\mathbin{\operatorname{and}}\,  \operatorname{not} \left({x}_{1} = {y}_{1} = 0\right) \,\mathbin{\operatorname{and}}\,  \operatorname{not} \left({x}_{2} = {y}_{2} = 0\right)

Definitions:

Fungrim symbol	Notation	Short description
`Atan2`	$\operatorname{atan2}\!\left(y, x\right)$	Two-argument inverse tangent
`RR`	$\mathbb{R}$	Real numbers
`OpenClosedInterval`	$\left(a, b\right]$	Open-closed interval
`ConstPi`	$\pi$	The constant pi (3.14...)

Source code for this entry:

Entry(ID("a020e9"),
    Formula(Equal(Add(Atan2(Subscript(y, 1), Subscript(x, 1)), Atan2(Subscript(y, 2), Subscript(x, 2))), Atan2(Add(Mul(Subscript(y, 1), Subscript(x, 2)), Mul(Subscript(y, 2), Subscript(x, 1))), Sub(Mul(Subscript(x, 1), Subscript(x, 2)), Mul(Subscript(y, 1), Subscript(y, 2)))))),
    Variables(x, y),
    Assumptions(And(Element(Subscript(x, 1), RR), Element(Subscript(x, 2), RR), Element(Subscript(y, 1), RR), Element(Subscript(y, 2), RR), Element(Add(Atan2(Subscript(y, 1), Subscript(x, 1)), Atan2(Subscript(y, 2), Subscript(x, 2))), OpenClosedInterval(Neg(ConstPi), ConstPi)), Not(Equal(Subscript(x, 1), Subscript(y, 1), 0)), Not(Equal(Subscript(x, 2), Subscript(y, 2), 0)))))

1d730a

\operatorname{atan2}\!\left({y}_{1}, {x}_{1}\right) - \operatorname{atan2}\!\left({y}_{2}, {x}_{2}\right) = \operatorname{atan2}\!\left({y}_{1} {x}_{2} - {y}_{2} {x}_{1}, {x}_{1} {x}_{2} + {y}_{1} {y}_{2}\right)

Assumptions:

{x}_{1} \in \mathbb{R} \,\mathbin{\operatorname{and}}\, {x}_{2} \in \mathbb{R} \,\mathbin{\operatorname{and}}\, {y}_{1} \in \mathbb{R} \,\mathbin{\operatorname{and}}\, {y}_{2} \in \mathbb{R} \,\mathbin{\operatorname{and}}\, \operatorname{atan2}\!\left({y}_{1}, {x}_{1}\right) - \operatorname{atan2}\!\left({y}_{2}, {x}_{2}\right) \in \left(-\pi, \pi\right] \,\mathbin{\operatorname{and}}\, \operatorname{not} \left({x}_{1} = {y}_{1} = 0\right) \,\mathbin{\operatorname{and}}\, \operatorname{not} \left({x}_{2} = {y}_{2} = 0\right)

TeX:

\operatorname{atan2}\!\left({y}_{1}, {x}_{1}\right) - \operatorname{atan2}\!\left({y}_{2}, {x}_{2}\right) = \operatorname{atan2}\!\left({y}_{1} {x}_{2} - {y}_{2} {x}_{1}, {x}_{1} {x}_{2} + {y}_{1} {y}_{2}\right)

{x}_{1} \in \mathbb{R} \,\mathbin{\operatorname{and}}\, {x}_{2} \in \mathbb{R} \,\mathbin{\operatorname{and}}\, {y}_{1} \in \mathbb{R} \,\mathbin{\operatorname{and}}\, {y}_{2} \in \mathbb{R} \,\mathbin{\operatorname{and}}\, \operatorname{atan2}\!\left({y}_{1}, {x}_{1}\right) - \operatorname{atan2}\!\left({y}_{2}, {x}_{2}\right) \in \left(-\pi, \pi\right] \,\mathbin{\operatorname{and}}\,  \operatorname{not} \left({x}_{1} = {y}_{1} = 0\right) \,\mathbin{\operatorname{and}}\,  \operatorname{not} \left({x}_{2} = {y}_{2} = 0\right)

Definitions:

Fungrim symbol	Notation	Short description
`Atan2`	$\operatorname{atan2}\!\left(y, x\right)$	Two-argument inverse tangent
`RR`	$\mathbb{R}$	Real numbers
`OpenClosedInterval`	$\left(a, b\right]$	Open-closed interval
`ConstPi`	$\pi$	The constant pi (3.14...)

Source code for this entry:

Entry(ID("1d730a"),
    Formula(Equal(Sub(Atan2(Subscript(y, 1), Subscript(x, 1)), Atan2(Subscript(y, 2), Subscript(x, 2))), Atan2(Sub(Mul(Subscript(y, 1), Subscript(x, 2)), Mul(Subscript(y, 2), Subscript(x, 1))), Add(Mul(Subscript(x, 1), Subscript(x, 2)), Mul(Subscript(y, 1), Subscript(y, 2)))))),
    Variables(x, y),
    Assumptions(And(Element(Subscript(x, 1), RR), Element(Subscript(x, 2), RR), Element(Subscript(y, 1), RR), Element(Subscript(y, 2), RR), Element(Sub(Atan2(Subscript(y, 1), Subscript(x, 1)), Atan2(Subscript(y, 2), Subscript(x, 2))), OpenClosedInterval(Neg(ConstPi), ConstPi)), Not(Equal(Subscript(x, 1), Subscript(y, 1), 0)), Not(Equal(Subscript(x, 2), Subscript(y, 2), 0)))))

a18b77

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

Assumptions:

z \in \mathbb{C}

TeX:

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

z \in \mathbb{C}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`ConstI`	$i$	Imaginary unit
`Log`	$\log\!\left(z\right)$	Natural logarithm
`CC`	$\mathbb{C}$	Complex numbers

Source code for this entry:

Entry(ID("a18b77"),
    Formula(Equal(Atan(z), Mul(Div(ConstI, 2), Sub(Log(Sub(1, Mul(ConstI, z))), Log(Add(1, Mul(ConstI, z))))))),
    Variables(z),
    Assumptions(Element(z, CC)))

500c0a

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

Assumptions:

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, -z i \notin \left[1, \infty\right)

TeX:

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

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, -z i \notin \left[1, \infty\right)

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`ConstI`	$i$	Imaginary unit
`Log`	$\log\!\left(z\right)$	Natural logarithm
`CC`	$\mathbb{C}$	Complex numbers
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval
`Infinity`	$\infty$	Positive infinity

Source code for this entry:

Entry(ID("500c0a"),
    Formula(Equal(Atan(z), Mul(Div(ConstI, 2), Log(Div(Sub(1, Mul(ConstI, z)), Add(1, Mul(ConstI, z))))))),
    Variables(z),
    Assumptions(And(Element(z, CC), NotElement(Mul(Neg(z), ConstI), ClosedOpenInterval(1, Infinity)))))

12765e

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

Assumptions:

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, z i \notin \left[1, \infty\right)

TeX:

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

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, z i \notin \left[1, \infty\right)

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`ConstI`	$i$	Imaginary unit
`Log`	$\log\!\left(z\right)$	Natural logarithm
`CC`	$\mathbb{C}$	Complex numbers
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval
`Infinity`	$\infty$	Positive infinity

Source code for this entry:

Entry(ID("12765e"),
    Formula(Equal(Atan(z), Mul(Neg(Div(ConstI, 2)), Log(Div(Add(1, Mul(ConstI, z)), Sub(1, Mul(ConstI, z))))))),
    Variables(z),
    Assumptions(And(Element(z, CC), NotElement(Mul(z, ConstI), ClosedOpenInterval(1, Infinity)))))

9dec3e

\operatorname{atan2}\!\left(y, x\right) = -i \log\!\left(\operatorname{sgn}\!\left(x + y i\right)\right)

Assumptions:

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} \,\mathbin{\operatorname{and}}\, x + y i \ne 0

TeX:

\operatorname{atan2}\!\left(y, x\right) = -i \log\!\left(\operatorname{sgn}\!\left(x + y i\right)\right)

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} \,\mathbin{\operatorname{and}}\, x + y i \ne 0

Definitions:

Fungrim symbol	Notation	Short description
`Atan2`	$\operatorname{atan2}\!\left(y, x\right)$	Two-argument inverse tangent
`ConstI`	$i$	Imaginary unit
`Log`	$\log\!\left(z\right)$	Natural logarithm
`Sign`	$\operatorname{sgn}\!\left(z\right)$	Sign function
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("9dec3e"),
    Formula(Equal(Atan2(y, x), Mul(Neg(ConstI), Log(Sign(Add(x, Mul(y, ConstI))))))),
    Variables(x, y),
    Assumptions(And(Element(x, RR), Element(y, RR), Unequal(Add(x, Mul(y, ConstI)), 0))))

eca4ce

\operatorname{atan2}\!\left(y, x\right) = \operatorname{Im}\!\left(\log\!\left(x + y i\right)\right)

Assumptions:

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} \,\mathbin{\operatorname{and}}\, x + y i \ne 0

TeX:

\operatorname{atan2}\!\left(y, x\right) = \operatorname{Im}\!\left(\log\!\left(x + y i\right)\right)

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} \,\mathbin{\operatorname{and}}\, x + y i \ne 0

Definitions:

Fungrim symbol	Notation	Short description
`Atan2`	$\operatorname{atan2}\!\left(y, x\right)$	Two-argument inverse tangent
`Im`	$\operatorname{Im}\!\left(z\right)$	Imaginary part
`Log`	$\log\!\left(z\right)$	Natural logarithm
`ConstI`	$i$	Imaginary unit
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("eca4ce"),
    Formula(Equal(Atan2(y, x), Im(Log(Add(x, Mul(y, ConstI)))))),
    Variables(x, y),
    Assumptions(And(Element(x, RR), Element(y, RR), Unequal(Add(x, Mul(y, ConstI)), 0))))

c580f4

\operatorname{atan}\!\left(z\right) = \operatorname{acot}\!\left(\frac{1}{z}\right)

Assumptions:

z \in \mathbb{C}

TeX:

\operatorname{atan}\!\left(z\right) = \operatorname{acot}\!\left(\frac{1}{z}\right)

z \in \mathbb{C}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`CC`	$\mathbb{C}$	Complex numbers

Source code for this entry:

Entry(ID("c580f4"),
    Formula(Equal(Atan(z), Acot(Div(1, z)))),
    Variables(z),
    Assumptions(Element(z, CC)))

7954ad

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

Assumptions:

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, i z \notin \left(-\infty, -1\right] \cup \left[1, \infty\right)

TeX:

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

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
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Sqrt`	$\sqrt{z}$	Principal square root
`Pow`	${a}^{b}$	Power
`CC`	$\mathbb{C}$	Complex numbers
`ConstI`	$i$	Imaginary unit
`OpenClosedInterval`	$\left(a, b\right]$	Open-closed interval
`Infinity`	$\infty$	Positive infinity
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval

Source code for this entry:

Entry(ID("7954ad"),
    Formula(Equal(Atan(z), Asin(Div(z, Sqrt(Add(1, Pow(z, 2))))))),
    Variables(z),
    Assumptions(And(Element(z, CC), NotElement(Mul(ConstI, z), Union(OpenClosedInterval(Neg(Infinity), -1), ClosedOpenInterval(1, Infinity))))))

ec7f2d

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

Assumptions:

z \in \mathbb{C} \setminus \left\{-i, i\right\}

TeX:

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

z \in \mathbb{C} \setminus \left\{-i, i\right\}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Sqrt`	$\sqrt{z}$	Principal square root
`Pow`	${a}^{b}$	Power
`CC`	$\mathbb{C}$	Complex numbers
`ConstI`	$i$	Imaginary unit

Source code for this entry:

Entry(ID("ec7f2d"),
    Formula(Equal(Atan(z), Mul(Csgn(z), Acos(Div(1, Sqrt(Add(1, Pow(z, 2)))))))),
    Variables(z),
    Assumptions(Element(z, SetMinus(CC, Set(Neg(ConstI), ConstI)))))

34ff28

\operatorname{atan}\!\left(z\right) = z \,{}_2F_1\!\left(1, \frac{1}{2}, \frac{3}{2}, -{z}^{2}\right)

Assumptions:

z \in \mathbb{C} \setminus \left\{-i, i\right\}

TeX:

\operatorname{atan}\!\left(z\right) = z \,{}_2F_1\!\left(1, \frac{1}{2}, \frac{3}{2}, -{z}^{2}\right)

z \in \mathbb{C} \setminus \left\{-i, i\right\}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Hypergeometric2F1`	$\,{}_2F_1\!\left(a, b, c, z\right)$	Gauss hypergeometric function
`Pow`	${a}^{b}$	Power
`CC`	$\mathbb{C}$	Complex numbers
`ConstI`	$i$	Imaginary unit

Source code for this entry:

Entry(ID("34ff28"),
    Formula(Equal(Atan(z), Mul(z, Hypergeometric2F1(1, Div(1, 2), Div(3, 2), Neg(Pow(z, 2)))))),
    Variables(z),
    Assumptions(Element(z, SetMinus(CC, Set(Neg(ConstI), ConstI)))))

df52fc

\operatorname{Re}\!\left(\operatorname{atan}\!\left(x + y i\right)\right) = \frac{1}{2} \operatorname{atan2}\!\left(2 x, 1 - {x}^{2} - {y}^{2}\right)

Assumptions:

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} \,\mathbin{\operatorname{and}}\, \operatorname{not} \left(x = 0 \,\mathbin{\operatorname{and}}\, y \in \left(-\infty, -1\right] \cup \left\{1\right\}\right)

TeX:

\operatorname{Re}\!\left(\operatorname{atan}\!\left(x + y i\right)\right) = \frac{1}{2} \operatorname{atan2}\!\left(2 x, 1 - {x}^{2} - {y}^{2}\right)

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} \,\mathbin{\operatorname{and}}\,  \operatorname{not} \left(x = 0 \,\mathbin{\operatorname{and}}\, y \in \left(-\infty, -1\right] \cup \left\{1\right\}\right)

Definitions:

Fungrim symbol	Notation	Short description
`Re`	$\operatorname{Re}\!\left(z\right)$	Real part
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`ConstI`	$i$	Imaginary unit
`Atan2`	$\operatorname{atan2}\!\left(y, x\right)$	Two-argument inverse tangent
`Pow`	${a}^{b}$	Power
`RR`	$\mathbb{R}$	Real numbers
`OpenClosedInterval`	$\left(a, b\right]$	Open-closed interval
`Infinity`	$\infty$	Positive infinity

Source code for this entry:

Entry(ID("df52fc"),
    Formula(Equal(Re(Atan(Add(x, Mul(y, ConstI)))), Mul(Div(1, 2), Atan2(Mul(2, x), Sub(Sub(1, Pow(x, 2)), Pow(y, 2)))))),
    Variables(x, y),
    Assumptions(And(Element(x, RR), Element(y, RR), Not(And(Equal(x, 0), Element(y, Union(OpenClosedInterval(Neg(Infinity), -1), Set(1))))))))

b65d19

\operatorname{Im}\!\left(\operatorname{atan}\!\left(x + y i\right)\right) = \frac{1}{4} \log\!\left(\frac{{x}^{2} + {\left(1 + y\right)}^{2}}{{x}^{2} + {\left(1 - y\right)}^{2}}\right)

Assumptions:

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} \,\mathbin{\operatorname{and}}\, x + y i \notin \left\{-i, i\right\}

TeX:

\operatorname{Im}\!\left(\operatorname{atan}\!\left(x + y i\right)\right) = \frac{1}{4} \log\!\left(\frac{{x}^{2} + {\left(1 + y\right)}^{2}}{{x}^{2} + {\left(1 - y\right)}^{2}}\right)

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} \,\mathbin{\operatorname{and}}\, x + y i \notin \left\{-i, i\right\}

Definitions:

Fungrim symbol	Notation	Short description
`Im`	$\operatorname{Im}\!\left(z\right)$	Imaginary part
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`ConstI`	$i$	Imaginary unit
`Log`	$\log\!\left(z\right)$	Natural logarithm
`Pow`	${a}^{b}$	Power
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("b65d19"),
    Formula(Equal(Im(Atan(Add(x, Mul(y, ConstI)))), Mul(Div(1, 4), Log(Div(Add(Pow(x, 2), Pow(Add(1, y), 2)), Add(Pow(x, 2), Pow(Sub(1, y), 2))))))),
    Variables(x, y),
    Assumptions(And(Element(x, RR), Element(y, RR), NotElement(Add(x, Mul(y, ConstI)), Set(Neg(ConstI), ConstI)))))

8fbf69

\operatorname{atan}'(z) = \frac{1}{1 + {z}^{2}}

Assumptions:

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, i z \notin \left(-\infty, -1\right] \cup \left[1, \infty\right)

TeX:

\operatorname{atan}'(z) = \frac{1}{1 + {z}^{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
`Derivative`	$\frac{d}{d z}\, f\!\left(z\right)$	Derivative
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Pow`	${a}^{b}$	Power
`CC`	$\mathbb{C}$	Complex numbers
`ConstI`	$i$	Imaginary unit
`OpenClosedInterval`	$\left(a, b\right]$	Open-closed interval
`Infinity`	$\infty$	Positive infinity
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval

Source code for this entry:

Entry(ID("8fbf69"),
    Formula(Equal(Derivative(Atan(z), Tuple(z, z, 1)), Div(1, Add(1, Pow(z, 2))))),
    Variables(z),
    Assumptions(And(Element(z, CC), NotElement(Mul(ConstI, z), Union(OpenClosedInterval(Neg(Infinity), -1), ClosedOpenInterval(1, Infinity))))))

a4eb86

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

Assumptions:

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, i z \notin \left(-\infty, -1\right] \cup \left[1, \infty\right)

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
`Derivative`	$\frac{d}{d z}\, f\!\left(z\right)$	Derivative
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Pow`	${a}^{b}$	Power
`CC`	$\mathbb{C}$	Complex numbers
`ConstI`	$i$	Imaginary unit
`OpenClosedInterval`	$\left(a, b\right]$	Open-closed interval
`Infinity`	$\infty$	Positive infinity
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval

Source code for this entry:

Entry(ID("a4eb86"),
    Formula(Equal(Derivative(Atan(z), Tuple(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))))))

90631b

{\operatorname{atan}}^{(n)}(z) = \frac{\left(n - 1\right)!}{{\left(1 + {z}^{2}\right)}^{\left( n + 1 \right) / 2}} U_{n - 1}\!\left(-\frac{z}{\sqrt{1 + {z}^{2}}}\right)

Assumptions:

n \in \mathbb{Z}_{\ge 1} \,\mathbin{\operatorname{and}}\, z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, i z \notin \left(-\infty, -1\right] \cup \left[1, \infty\right)

References:

M. A. Boutiche and M. Rahmani (2017), On the higher derivatives of the inverse tangent function, https://arxiv.org/abs/1712.03521, Theorem 9

TeX:

{\operatorname{atan}}^{(n)}(z) = \frac{\left(n - 1\right)!}{{\left(1 + {z}^{2}\right)}^{\left( n + 1 \right) / 2}} U_{n - 1}\!\left(-\frac{z}{\sqrt{1 + {z}^{2}}}\right)

n \in \mathbb{Z}_{\ge 1} \,\mathbin{\operatorname{and}}\, 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
`Derivative`	$\frac{d}{d z}\, f\!\left(z\right)$	Derivative
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Factorial`	$n !$	Factorial
`Pow`	${a}^{b}$	Power
`ChebyshevU`	$U_{n}\!\left(x\right)$	Chebyshev polynomial of the second kind
`Sqrt`	$\sqrt{z}$	Principal square root
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n
`CC`	$\mathbb{C}$	Complex numbers
`ConstI`	$i$	Imaginary unit
`OpenClosedInterval`	$\left(a, b\right]$	Open-closed interval
`Infinity`	$\infty$	Positive infinity
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval

Source code for this entry:

Entry(ID("90631b"),
    Formula(Equal(Derivative(Atan(z), Tuple(z, z, n)), Mul(Div(Factorial(Sub(n, 1)), Pow(Add(1, Pow(z, 2)), Div(Add(n, 1), 2))), ChebyshevU(Sub(n, 1), Neg(Div(z, Sqrt(Add(1, Pow(z, 2))))))))),
    Variables(z, n),
    Assumptions(And(Element(n, ZZGreaterEqual(1)), Element(z, CC), NotElement(Mul(ConstI, z), Union(OpenClosedInterval(Neg(Infinity), -1), ClosedOpenInterval(1, Infinity))))),
    References("M. A. Boutiche and M. Rahmani (2017), On the higher derivatives of the inverse tangent function, https://arxiv.org/abs/1712.03521, Theorem 9"))

36171f

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

Assumptions:

n \in \mathbb{Z}_{\ge 1} \,\mathbin{\operatorname{and}}\, z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, i z \notin \left(-\infty, -1\right] \cup \left[1, \infty\right)

TeX:

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

n \in \mathbb{Z}_{\ge 1} \,\mathbin{\operatorname{and}}\, 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
`Derivative`	$\frac{d}{d z}\, f\!\left(z\right)$	Derivative
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Pow`	${a}^{b}$	Power
`Factorial`	$n !$	Factorial
`ConstI`	$i$	Imaginary unit
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n
`CC`	$\mathbb{C}$	Complex numbers
`OpenClosedInterval`	$\left(a, b\right]$	Open-closed interval
`Infinity`	$\infty$	Positive infinity
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval

Source code for this entry:

Entry(ID("36171f"),
    Formula(Equal(Derivative(Atan(z), Tuple(z, z, n)), Mul(Div(Mul(Pow(-1, n), Factorial(Sub(n, 1))), Mul(2, ConstI)), Sub(Div(1, Pow(Add(z, ConstI), n)), Div(1, Pow(Sub(z, ConstI), n)))))),
    Variables(z, n),
    Assumptions(And(Element(n, ZZGreaterEqual(1)), Element(z, CC), NotElement(Mul(ConstI, z), Union(OpenClosedInterval(Neg(Infinity), -1), ClosedOpenInterval(1, Infinity))))))

6b8963

\frac{d}{d x}\, \operatorname{atan2}\!\left(y, x\right) = -\frac{y}{{x}^{2} + {y}^{2}}

Assumptions:

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} \,\mathbin{\operatorname{and}}\, \left(x \gt 0 \,\mathbin{\operatorname{or}}\, y \ne 0\right)

TeX:

\frac{d}{d x}\, \operatorname{atan2}\!\left(y, x\right) = -\frac{y}{{x}^{2} + {y}^{2}}

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} \,\mathbin{\operatorname{and}}\, \left(x \gt 0 \,\mathbin{\operatorname{or}}\, y \ne 0\right)

Definitions:

Fungrim symbol	Notation	Short description
`Derivative`	$\frac{d}{d z}\, f\!\left(z\right)$	Derivative
`Atan2`	$\operatorname{atan2}\!\left(y, x\right)$	Two-argument inverse tangent
`Pow`	${a}^{b}$	Power
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("6b8963"),
    Formula(Equal(Derivative(Atan2(y, x), Tuple(x, x, 1)), Neg(Div(y, Add(Pow(x, 2), Pow(y, 2)))))),
    Variables(x, y),
    Assumptions(And(Element(x, RR), Element(y, RR), Or(Greater(x, 0), Unequal(y, 0)))))

1d3fd7

\frac{d}{d y}\, \operatorname{atan2}\!\left(y, x\right) = \frac{x}{{x}^{2} + {y}^{2}}

Assumptions:

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} \,\mathbin{\operatorname{and}}\, \left(x \gt 0 \,\mathbin{\operatorname{or}}\, y \ne 0\right)

TeX:

\frac{d}{d y}\, \operatorname{atan2}\!\left(y, x\right) = \frac{x}{{x}^{2} + {y}^{2}}

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} \,\mathbin{\operatorname{and}}\, \left(x \gt 0 \,\mathbin{\operatorname{or}}\, y \ne 0\right)

Definitions:

Fungrim symbol	Notation	Short description
`Derivative`	$\frac{d}{d z}\, f\!\left(z\right)$	Derivative
`Atan2`	$\operatorname{atan2}\!\left(y, x\right)$	Two-argument inverse tangent
`Pow`	${a}^{b}$	Power
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("1d3fd7"),
    Formula(Equal(Derivative(Atan2(y, x), Tuple(y, y, 1)), Div(x, Add(Pow(x, 2), Pow(y, 2))))),
    Variables(x, y),
    Assumptions(And(Element(x, RR), Element(y, RR), Or(Greater(x, 0), Unequal(y, 0)))))

4e5947

\operatorname{atan}\!\left(z\right) = \sum_{k=0}^{\infty} \frac{{\left(-1\right)}^{k} {z}^{2 k + 1}}{2 k + 1}

Assumptions:

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \left|z\right| \lt 1

TeX:

\operatorname{atan}\!\left(z\right) = \sum_{k=0}^{\infty} \frac{{\left(-1\right)}^{k} {z}^{2 k + 1}}{2 k + 1}

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \left|z\right| \lt 1

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Pow`	${a}^{b}$	Power
`Infinity`	$\infty$	Positive infinity
`CC`	$\mathbb{C}$	Complex numbers
`Abs`	$\left\|z\right\|$	Absolute value

Source code for this entry:

Entry(ID("4e5947"),
    Formula(Equal(Atan(z), Sum(Div(Mul(Pow(-1, k), Pow(z, Add(Mul(2, k), 1))), Add(Mul(2, k), 1)), Tuple(k, 0, Infinity)))),
    Variables(z),
    Assumptions(And(Element(z, CC), Less(Abs(z), 1))))

e7a9b1

\left|\operatorname{atan}\!\left(x\right)\right| \lt \frac{\pi}{2}

Assumptions:

x \in \mathbb{R}

TeX:

\left|\operatorname{atan}\!\left(x\right)\right| \lt \frac{\pi}{2}

x \in \mathbb{R}

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`ConstPi`	$\pi$	The constant pi (3.14...)
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("e7a9b1"),
    Formula(Less(Abs(Atan(x)), Div(ConstPi, 2))),
    Variables(x),
    Assumptions(Element(x, RR)))

5d6f74

\left|\operatorname{atan}\!\left(x\right)\right| \le \frac{\pi}{2}

Assumptions:

x \in \mathbb{R} \cup \left\{-\infty, \infty\right\}

TeX:

\left|\operatorname{atan}\!\left(x\right)\right| \le \frac{\pi}{2}

x \in \mathbb{R} \cup \left\{-\infty, \infty\right\}

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`ConstPi`	$\pi$	The constant pi (3.14...)
`RR`	$\mathbb{R}$	Real numbers
`Infinity`	$\infty$	Positive infinity

Source code for this entry:

Entry(ID("5d6f74"),
    Formula(LessEqual(Abs(Atan(x)), Div(ConstPi, 2))),
    Variables(x),
    Assumptions(Element(x, Union(RR, Set(Neg(Infinity), Infinity)))))

466095

\left|\operatorname{atan}\!\left(x\right)\right| \le \left|x\right|

Assumptions:

x \in \mathbb{R} \cup \left\{-\infty, \infty\right\}

TeX:

\left|\operatorname{atan}\!\left(x\right)\right| \le \left|x\right|

x \in \mathbb{R} \cup \left\{-\infty, \infty\right\}

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`RR`	$\mathbb{R}$	Real numbers
`Infinity`	$\infty$	Positive infinity

Source code for this entry:

Entry(ID("466095"),
    Formula(LessEqual(Abs(Atan(x)), Abs(x))),
    Variables(x),
    Assumptions(Element(x, Union(RR, Set(Neg(Infinity), Infinity)))))

3478af

\operatorname{atan}\!\left(x\right) \le \sum_{k=0}^{2 N} \frac{{\left(-1\right)}^{k} {x}^{2 k + 1}}{2 k + 1}

Assumptions:

x \in \left[0, \infty\right) \,\mathbin{\operatorname{and}}\, N \in \mathbb{Z}_{\ge 0}

TeX:

\operatorname{atan}\!\left(x\right) \le \sum_{k=0}^{2 N} \frac{{\left(-1\right)}^{k} {x}^{2 k + 1}}{2 k + 1}

x \in \left[0, \infty\right) \,\mathbin{\operatorname{and}}\, N \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Pow`	${a}^{b}$	Power
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval
`Infinity`	$\infty$	Positive infinity
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("3478af"),
    Formula(LessEqual(Atan(x), Sum(Div(Mul(Pow(-1, k), Pow(x, Add(Mul(2, k), 1))), Add(Mul(2, k), 1)), Tuple(k, 0, Mul(2, N))))),
    Variables(x, N),
    Assumptions(And(Element(x, ClosedOpenInterval(0, Infinity)), Element(N, ZZGreaterEqual(0)))))

1eeccf

\operatorname{atan}\!\left(x\right) \ge \sum_{k=0}^{2 N + 1} \frac{{\left(-1\right)}^{k} {x}^{2 k + 1}}{2 k + 1}

Assumptions:

x \in \left[0, \infty\right) \,\mathbin{\operatorname{and}}\, N \in \mathbb{Z}_{\ge 0}

TeX:

\operatorname{atan}\!\left(x\right) \ge \sum_{k=0}^{2 N + 1} \frac{{\left(-1\right)}^{k} {x}^{2 k + 1}}{2 k + 1}

x \in \left[0, \infty\right) \,\mathbin{\operatorname{and}}\, N \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Pow`	${a}^{b}$	Power
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval
`Infinity`	$\infty$	Positive infinity
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("1eeccf"),
    Formula(GreaterEqual(Atan(x), Sum(Div(Mul(Pow(-1, k), Pow(x, Add(Mul(2, k), 1))), Add(Mul(2, k), 1)), Tuple(k, 0, Add(Mul(2, N), 1))))),
    Variables(x, N),
    Assumptions(And(Element(x, ClosedOpenInterval(0, Infinity)), Element(N, ZZGreaterEqual(0)))))

efebb8

\operatorname{atan}\!\left(x\right) \le {\left(\frac{\pi}{2}\right)}^{2} \frac{x}{1 + \frac{\pi}{2} x}

Assumptions:

x \in \left[0, \infty\right)

TeX:

\operatorname{atan}\!\left(x\right) \le {\left(\frac{\pi}{2}\right)}^{2} \frac{x}{1 + \frac{\pi}{2} x}

x \in \left[0, \infty\right)

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Pow`	${a}^{b}$	Power
`ConstPi`	$\pi$	The constant pi (3.14...)
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval
`Infinity`	$\infty$	Positive infinity

Source code for this entry:

Entry(ID("efebb8"),
    Formula(LessEqual(Atan(x), Mul(Pow(Div(ConstPi, 2), 2), Div(x, Add(1, Mul(Div(ConstPi, 2), x)))))),
    Variables(x),
    Assumptions(Element(x, ClosedOpenInterval(0, Infinity))))

a42212

\operatorname{atan}\!\left(x\right) \ge \frac{x}{1 + x}

Assumptions:

x \in \left[0, \infty\right)

TeX:

\operatorname{atan}\!\left(x\right) \ge \frac{x}{1 + x}

x \in \left[0, \infty\right)

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval
`Infinity`	$\infty$	Positive infinity

Source code for this entry:

Entry(ID("a42212"),
    Formula(GreaterEqual(Atan(x), Div(x, Add(1, x)))),
    Variables(x),
    Assumptions(Element(x, ClosedOpenInterval(0, Infinity))))

3fe47b

\operatorname{atan}\!\left(x\right) \ge \frac{\pi x}{\pi + 2 x}

Assumptions:

x \in \left[0, \infty\right)

TeX:

\operatorname{atan}\!\left(x\right) \ge \frac{\pi x}{\pi + 2 x}

x \in \left[0, \infty\right)

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`ConstPi`	$\pi$	The constant pi (3.14...)
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval
`Infinity`	$\infty$	Positive infinity

Source code for this entry:

Entry(ID("3fe47b"),
    Formula(GreaterEqual(Atan(x), Div(Mul(ConstPi, x), Add(ConstPi, Mul(2, x))))),
    Variables(x),
    Assumptions(Element(x, ClosedOpenInterval(0, Infinity))))

f5d28c

\operatorname{atan}\!\left(x\right) \le \frac{\pi}{2} \frac{x}{\sqrt{1 + {x}^{2}}}

Assumptions:

x \in \left[0, \infty\right)

TeX:

\operatorname{atan}\!\left(x\right) \le \frac{\pi}{2} \frac{x}{\sqrt{1 + {x}^{2}}}

x \in \left[0, \infty\right)

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`ConstPi`	$\pi$	The constant pi (3.14...)
`Sqrt`	$\sqrt{z}$	Principal square root
`Pow`	${a}^{b}$	Power
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval
`Infinity`	$\infty$	Positive infinity

Source code for this entry:

Entry(ID("f5d28c"),
    Formula(LessEqual(Atan(x), Mul(Div(ConstPi, 2), Div(x, Sqrt(Add(1, Pow(x, 2))))))),
    Variables(x),
    Assumptions(Element(x, ClosedOpenInterval(0, Infinity))))

b0a4e9

\operatorname{atan}\!\left(x\right) \ge \frac{x}{\sqrt{1 + {x}^{2}}}

Assumptions:

x \in \left[0, \infty\right)

TeX:

\operatorname{atan}\!\left(x\right) \ge \frac{x}{\sqrt{1 + {x}^{2}}}

x \in \left[0, \infty\right)

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Sqrt`	$\sqrt{z}$	Principal square root
`Pow`	${a}^{b}$	Power
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval
`Infinity`	$\infty$	Positive infinity

Source code for this entry:

Entry(ID("b0a4e9"),
    Formula(GreaterEqual(Atan(x), Div(x, Sqrt(Add(1, Pow(x, 2)))))),
    Variables(x),
    Assumptions(Element(x, ClosedOpenInterval(0, Infinity))))

d04a5b

\operatorname{atan}\!\left(x\right) \le \frac{\pi}{2} \tanh\!\left(x\right)

Assumptions:

x \in \left[0, \infty\right)

TeX:

\operatorname{atan}\!\left(x\right) \le \frac{\pi}{2} \tanh\!\left(x\right)

x \in \left[0, \infty\right)

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`ConstPi`	$\pi$	The constant pi (3.14...)
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval
`Infinity`	$\infty$	Positive infinity

Source code for this entry:

Entry(ID("d04a5b"),
    Formula(LessEqual(Atan(x), Mul(Div(ConstPi, 2), Tanh(x)))),
    Variables(x),
    Assumptions(Element(x, ClosedOpenInterval(0, Infinity))))

b971fe

\operatorname{atan}\!\left(x\right) \ge \tanh\!\left(x\right)

Assumptions:

x \in \left[0, \infty\right)

TeX:

\operatorname{atan}\!\left(x\right) \ge \tanh\!\left(x\right)

x \in \left[0, \infty\right)

Definitions:

Fungrim symbol	Notation	Short description
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval
`Infinity`	$\infty$	Positive infinity

Source code for this entry:

Entry(ID("b971fe"),
    Formula(GreaterEqual(Atan(x), Tanh(x))),
    Variables(x),
    Assumptions(Element(x, ClosedOpenInterval(0, Infinity))))

7272a8

\left|\operatorname{atan}\!\left(z\right)\right| \le \left|\operatorname{atanh}\!\left(\left|z\right|\right)\right|

Assumptions:

z \in \mathbb{C}

TeX:

\left|\operatorname{atan}\!\left(z\right)\right| \le \left|\operatorname{atanh}\!\left(\left|z\right|\right)\right|

z \in \mathbb{C}

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`CC`	$\mathbb{C}$	Complex numbers

Source code for this entry:

Entry(ID("7272a8"),
    Formula(LessEqual(Abs(Atan(z)), Abs(Atanh(Abs(z))))),
    Variables(z),
    Assumptions(Element(z, CC)))

fa9b71

\left|\operatorname{atan}\!\left(z\right)\right| \le -\log\!\left(1 - \left|z\right|\right)

Assumptions:

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \left|z\right| \le 1

TeX:

\left|\operatorname{atan}\!\left(z\right)\right| \le -\log\!\left(1 - \left|z\right|\right)

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \left|z\right| \le 1

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Log`	$\log\!\left(z\right)$	Natural logarithm
`CC`	$\mathbb{C}$	Complex numbers

Source code for this entry:

Entry(ID("fa9b71"),
    Formula(LessEqual(Abs(Atan(z)), Neg(Log(Sub(1, Abs(z)))))),
    Variables(z),
    Assumptions(And(Element(z, CC), LessEqual(Abs(z), 1))))

47331d

\left|\operatorname{atan}\!\left(x + y\right) - \operatorname{atan}\!\left(x\right)\right| = \operatorname{atan2}\!\left(\left|y\right|, 1 + x \left(x + y\right)\right)

Assumptions:

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R}

TeX:

\left|\operatorname{atan}\!\left(x + y\right) - \operatorname{atan}\!\left(x\right)\right| = \operatorname{atan2}\!\left(\left|y\right|, 1 + x \left(x + y\right)\right)

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R}

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Atan2`	$\operatorname{atan2}\!\left(y, x\right)$	Two-argument inverse tangent
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("47331d"),
    Formula(Equal(Abs(Sub(Atan(Add(x, y)), Atan(x))), Atan2(Abs(y), Add(1, Mul(x, Add(x, y)))))),
    Variables(x, y),
    Assumptions(And(Element(x, RR), Element(y, RR))))

96289e

\left|\operatorname{atan}\!\left(x + y\right) - \operatorname{atan}\!\left(x\right)\right| \le \left|y\right|

Assumptions:

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R}

TeX:

\left|\operatorname{atan}\!\left(x + y\right) - \operatorname{atan}\!\left(x\right)\right| \le \left|y\right|

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R}

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("96289e"),
    Formula(LessEqual(Abs(Sub(Atan(Add(x, y)), Atan(x))), Abs(y))),
    Variables(x, y),
    Assumptions(And(Element(x, RR), Element(y, RR))))

fa30c7

\left|\operatorname{atan}\!\left(x + y\right) - \operatorname{atan}\!\left(x\right)\right| \le \frac{\left|y\right|}{1 + {\left(\max\!\left(0, \left|x\right| - \left|y\right|\right)\right)}^{2}}

Assumptions:

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R}

TeX:

\left|\operatorname{atan}\!\left(x + y\right) - \operatorname{atan}\!\left(x\right)\right| \le \frac{\left|y\right|}{1 + {\left(\max\!\left(0, \left|x\right| - \left|y\right|\right)\right)}^{2}}

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R}

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`Pow`	${a}^{b}$	Power
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("fa30c7"),
    Formula(LessEqual(Abs(Sub(Atan(Add(x, y)), Atan(x))), Div(Abs(y), Add(1, Pow(Max(0, Sub(Abs(x), Abs(y))), 2))))),
    Variables(x, y),
    Assumptions(And(Element(x, RR), Element(y, RR))))

4d2168

\left|\operatorname{atan}\!\left(x + y\right) - \operatorname{atan}\!\left(x\right)\right| \lt \pi

Assumptions:

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R}

TeX:

\left|\operatorname{atan}\!\left(x + y\right) - \operatorname{atan}\!\left(x\right)\right| \lt \pi

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R}

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`Atan`	$\operatorname{atan}\!\left(z\right)$	Inverse tangent
`ConstPi`	$\pi$	The constant pi (3.14...)
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("4d2168"),
    Formula(Less(Abs(Sub(Atan(Add(x, y)), Atan(x))), ConstPi)),
    Variables(x, y),
    Assumptions(And(Element(x, RR), Element(y, RR))))

Definitions

Illustrations

Transcendental equations

Differential equations

Integral representations

Specific values

Analytic properties

Argument transformations

Symmetries

Addition and multiplication formulas

Algebraic transformations

Sums and products

Representations through other functions

Logarithms

Inverse trigonometric functions

Hypergeometric functions

Complex parts

Derivatives and integrals

Series expansions

Bounds and inequalities

Real arguments

Complex arguments

Perturbations