Fungrim entry: ed210c

Symbol: Log —

\log(z)

— Natural logarithm

The principal branch of the natural logarithm

\log(z)

is a function of one complex variable

z

It has a branch point singularity at

z = 0

and a branch cut on

\left(-\infty, 0\right]

where the value on

\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 \in \left\{1\right\}$	$\log(z) \in \left\{0\right\}$
$z \in \left(0, \infty\right)$	$\log(z) \in \mathbb{R}$
$z \in \mathbb{C} \setminus \left\{0\right\}$	$\log(z) \in \mathbb{C}$
Infinities
$z \in \left\{\infty\right\}$	$\log(z) \in \left\{\infty\right\}$
Formal power series
$z \in \mathbb{Q}[[x]] \;\mathbin{\operatorname{and}}\; [{x}^{0}] z = 1$	$\log(z) \in \mathbb{Q}[[x]] \;\mathbin{\operatorname{and}}\; [{x}^{0}] \log(z) = 0$
$z \in \mathbb{R}[[x]] \;\mathbin{\operatorname{and}}\; [{x}^{0}] z \in \left(0, \infty\right)$	$\log(z) \in \mathbb{R}[[x]]$
$z \in \mathbb{C}[[x]] \;\mathbin{\operatorname{and}}\; [{x}^{0}] z \ne 0$	$\log(z) \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
`Log`	$\log(z)$	Natural logarithm
`OpenClosedInterval`	$\left(a, b\right]$	Open-closed interval
`Infinity`	$\infty$	Positive infinity
`OpenInterval`	$\left(a, b\right)$	Open interval
`RR`	$\mathbb{R}$	Real numbers
`CC`	$\mathbb{C}$	Complex numbers
`PowerSeries`	$K[[x]]$	Formal power series
`QQ`	$\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, PowerSeries(QQ, x)), Equal(SeriesCoefficient(z, x, 0), 1)), And(Element(Log(z), PowerSeries(QQ, x)), Equal(SeriesCoefficient(Log(z), x, 0), 0))), Tuple(And(Element(z, PowerSeries(RR, x)), Element(SeriesCoefficient(z, x, 0), OpenInterval(0, Infinity))), And(Element(Log(z), PowerSeries(RR, x)))), Tuple(And(Element(z, PowerSeries(CC, x)), NotEqual(SeriesCoefficient(z, x, 0), 0)), And(Element(Log(z), PowerSeries(CC, x)))))))

Topics using this entry

Natural logarithm