Fungrim home page

Fungrim entry: dfbcd9

Symbol: Exp ez{e}^{z} Exponential function
The exponential function ez{e}^{z} is a function of one complex variable zz. It can be defined by the Taylor series 1635f5.
In rendered formulas, Exp(z) is shown as ez{e}^{z} or as exp ⁣(z)\exp\!\left(z\right) depending on the typographical requirements; no semantic difference is implied.
The following table lists all conditions such that Exp(z) is defined in Fungrim.
Domain Codomain
z{0}z \in \left\{0\right\} ez{1}{e}^{z} \in \left\{1\right\}
zRz \in \mathbb{R} ez(0,){e}^{z} \in \left(0, \infty\right)
zCz \in \mathbb{C} ezC{0}{e}^{z} \in \mathbb{C} \setminus \left\{0\right\}
z{}z \in \left\{\infty\right\} ez{}{e}^{z} \in \left\{\infty\right\}
z{}z \in \left\{-\infty\right\} ez{0}{e}^{z} \in \left\{0\right\}
Formal power series
zQ[[x]]and[x0]z=0z \in \mathbb{Q}[[x]] \,\mathbin{\operatorname{and}}\, [{x}^{0}] z = 0 ezQ[[x]]and[x0]ez=1{e}^{z} \in \mathbb{Q}[[x]] \,\mathbin{\operatorname{and}}\, [{x}^{0}] {e}^{z} = 1
zR[[x]]z \in \mathbb{R}[[x]] ezR[[x]]and[x0]ez0{e}^{z} \in \mathbb{R}[[x]] \,\mathbin{\operatorname{and}}\, [{x}^{0}] {e}^{z} \ne 0
zC[[x]]z \in \mathbb{C}[[x]] ezC[[x]]and[x0]ez0{e}^{z} \in \mathbb{C}[[x]] \,\mathbin{\operatorname{and}}\, [{x}^{0}] {e}^{z} \ne 0
Table data: (P,Q)\left(P, Q\right) such that (P)    (Q)\left(P\right) \implies \left(Q\right)
Fungrim symbol Notation Short description
Expez{e}^{z} Exponential function
RRR\mathbb{R} Real numbers
OpenInterval(a,b)\left(a, b\right) Open interval
Infinity\infty Positive infinity
CCC\mathbb{C} Complex numbers
FormalPowerSeriesK[[x]]K[[x]] Formal power series
QQQ\mathbb{Q} Rational numbers
Source code for this entry:
    SymbolDefinition(Exp, Exp(z), "Exponential function"),
    Description("The exponential function", Exp(z), "is a function of one complex variable", z, ".", "It can be defined by the Taylor series", EntryReference("1635f5"), "."),
    Description("In rendered formulas,", SourceForm(Exp(z)), "is shown as", Exp(z), "or as", Call(Exp, z), "depending on the typographical requirements; no semantic difference is implied."),
    Description("The following table lists all conditions such that", SourceForm(Exp(z)), "is defined in Fungrim."),
    Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(TableSection("Numbers"), Tuple(Element(z, Set(0)), Element(Exp(z), Set(1))), Tuple(Element(z, RR), Element(Exp(z), OpenInterval(0, Infinity))), Tuple(Element(z, CC), Element(Exp(z), SetMinus(CC, Set(0)))), TableSection("Infinities"), Tuple(Element(z, Set(Infinity)), Element(Exp(z), Set(Infinity))), Tuple(Element(z, Set(Neg(Infinity))), Element(Exp(z), Set(0))), TableSection("Formal power series"), Tuple(And(Element(z, FormalPowerSeries(QQ, x)), Equal(SeriesCoefficient(z, x, 0), 0)), And(Element(Exp(z), FormalPowerSeries(QQ, x)), Equal(SeriesCoefficient(Exp(z), x, 0), 1))), Tuple(Element(z, FormalPowerSeries(RR, x)), And(Element(Exp(z), FormalPowerSeries(RR, x)), Unequal(SeriesCoefficient(Exp(z), x, 0), 0))), Tuple(Element(z, FormalPowerSeries(CC, x)), And(Element(Exp(z), FormalPowerSeries(CC, x)), Unequal(SeriesCoefficient(Exp(z), x, 0), 0))))))

Topics using this entry

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

2019-08-21 11:44:15.926409 UTC