Fungrim home page

Fungrim entry: ed210c

Symbol: Log log ⁣(z)\log\!\left(z\right) Natural logarithm
The principal branch of the natural logarithm log ⁣(z)\log\!\left(z\right) is a function of one complex variable zz.
It has a branch point singularity at z=0z = 0 and a branch cut on (,0]\left(-\infty, 0\right] where the value on (,0)\left(-\infty, 0\right) is taken to be continuous with the upper half plane.
The following table lists all conditions such that Log(z) is defined in Fungrim.
Domain Codomain
Numbers
z{1}z \in \left\{1\right\} log ⁣(z){0}\log\!\left(z\right) \in \left\{0\right\}
z(0,)z \in \left(0, \infty\right) log ⁣(z)R\log\!\left(z\right) \in \mathbb{R}
zC{0}z \in \mathbb{C} \setminus \left\{0\right\} log ⁣(z)C\log\!\left(z\right) \in \mathbb{C}
Infinities
z{}z \in \left\{\infty\right\} log ⁣(z){}\log\!\left(z\right) \in \left\{\infty\right\}
Formal power series
zQ[[x]]and[x0]z=1z \in \mathbb{Q}[[x]] \,\mathbin{\operatorname{and}}\, [{x}^{0}] z = 1 log ⁣(z)Q[[x]]and[x0]log ⁣(z)=0\log\!\left(z\right) \in \mathbb{Q}[[x]] \,\mathbin{\operatorname{and}}\, [{x}^{0}] \log\!\left(z\right) = 0
zR[[x]]and[x0]z(0,)z \in \mathbb{R}[[x]] \,\mathbin{\operatorname{and}}\, [{x}^{0}] z \in \left(0, \infty\right) log ⁣(z)R[[x]]\log\!\left(z\right) \in \mathbb{R}[[x]]
zC[[x]]and[x0]z0z \in \mathbb{C}[[x]] \,\mathbin{\operatorname{and}}\, [{x}^{0}] z \ne 0 log ⁣(z)C[[x]]\log\!\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
Loglog ⁣(z)\log\!\left(z\right) Natural logarithm
OpenClosedInterval(a,b]\left(a, b\right] Open-closed interval
Infinity\infty Positive infinity
OpenInterval(a,b)\left(a, b\right) Open interval
RRR\mathbb{R} Real numbers
CCC\mathbb{C} Complex numbers
FormalPowerSeriesK[[x]]K[[x]] Formal power series
QQQ\mathbb{Q} Rational numbers
Source code for this entry:
Entry(ID("ed210c"),
    SymbolDefinition(Log, Log(z), "Natural logarithm"),
    Description("The principal branch of the natural logarithm", Log(z), "is a function of one complex variable", z, "."),
    Description("It has a branch point singularity at", Equal(z, 0), "and a branch cut on", OpenClosedInterval(Neg(Infinity), 0), "where the value on", OpenInterval(Neg(Infinity), 0), "is taken to be continuous with the upper half plane."),
    Description("The following table lists all conditions such that", SourceForm(Log(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(1)), Element(Log(z), Set(0))), Tuple(Element(z, OpenInterval(0, Infinity)), Element(Log(z), RR)), Tuple(Element(z, SetMinus(CC, Set(0))), Element(Log(z), CC)), TableSection("Infinities"), Tuple(Element(z, Set(Infinity)), Element(Log(z), Set(Infinity))), TableSection("Formal power series"), Tuple(And(Element(z, FormalPowerSeries(QQ, x)), Equal(SeriesCoefficient(z, x, 0), 1)), And(Element(Log(z), FormalPowerSeries(QQ, x)), Equal(SeriesCoefficient(Log(z), x, 0), 0))), Tuple(And(Element(z, FormalPowerSeries(RR, x)), Element(SeriesCoefficient(z, x, 0), OpenInterval(0, Infinity))), And(Element(Log(z), FormalPowerSeries(RR, x)))), Tuple(And(Element(z, FormalPowerSeries(CC, x)), Unequal(SeriesCoefficient(z, x, 0), 0)), And(Element(Log(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