Fungrim entry: b120b9

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

Topics using this entry

Inverse tangent