Fungrim home page

Fungrim entry: b120b9

Symbol: Atan atan ⁣(z)\operatorname{atan}\!\left(z\right) Inverse tangent
The inverse tangent function atan ⁣(z)\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
zRz \in \mathbb{R} atan ⁣(z)(π2,π2)\operatorname{atan}\!\left(z\right) \in \left(-\frac{\pi}{2}, \frac{\pi}{2}\right)
zC{i,+i}z \in \mathbb{C} \setminus \left\{-i, +i\right\} atan ⁣(z)C\operatorname{atan}\!\left(z\right) \in \mathbb{C}
Infinities
z{,}z \in \left\{-\infty, \infty\right\} atan ⁣(z){π2,π2}\operatorname{atan}\!\left(z\right) \in \left\{-\frac{\pi}{2}, \frac{\pi}{2}\right\}
z{i,+i}z \in \left\{-i, +i\right\} atan ⁣(z){i,+i}\operatorname{atan}\!\left(z\right) \in \left\{-i \infty, +i \infty\right\}
Formal power series
zR[[x]]z \in \mathbb{R}[[x]] atan ⁣(z)R[[x]]\operatorname{atan}\!\left(z\right) \in \mathbb{R}[[x]]
zC[[x]]and[x0]z{i,+i}z \in \mathbb{C}[[x]] \,\mathbin{\operatorname{and}}\, [{x}^{0}] z \notin \left\{-i, +i\right\} atan ⁣(z)C[[x]]\operatorname{atan}\!\left(z\right) \in \mathbb{C}[[x]]
Table data: (P,Q)\left(P, Q\right) such that (P)    (Q)\left(P\right) \implies \left(Q\right)
Definitions:
Fungrim symbol Notation Short description
Atanatan ⁣(z)\operatorname{atan}\!\left(z\right) Inverse tangent
RRR\mathbb{R} Real numbers
OpenInterval(a,b)\left(a, b\right) Open interval
ConstPiπ\pi The constant pi (3.14...)
CCC\mathbb{C} Complex numbers
ConstIii Imaginary unit
Infinity\infty Positive infinity
FormalPowerSeriesK[[x]]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

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

2019-06-18 07:49:59.356594 UTC