Fungrim entry: 21d9b8

Symbol: Sqrt —

\sqrt{z}

— Principal square root

The principal square root

\sqrt{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 Sqrt(z) is defined in Fungrim.

Domain	Codomain
Numbers
$z \in \left[0, \infty\right)$	$\sqrt{z} \in \left[0, \infty\right)$
$z \in \mathbb{C}$	$\sqrt{z} \in \mathbb{C}$
Infinities
$z \in \left\{{\tilde \infty}\right\}$	$\sqrt{z} \in \left\{{\tilde \infty}\right\}$
$z \in \left\{ {e}^{i \theta} \infty : \theta \in \left(-\pi, \pi\right] \right\}$	$\sqrt{z} \in \left\{ {e}^{i \theta} \infty : \theta \in \left(\frac{-\pi}{2}, \frac{\pi}{2}\right] \right\}$
Formal power series
$z \in \mathbb{R}[[x]] \,\mathbin{\operatorname{and}}\, [{x}^{0}] z \in \left(0, \infty\right)$	$\sqrt{z} \in \mathbb{R}[[x]]$
$z \in \mathbb{C}[[x]] \,\mathbin{\operatorname{and}}\, [{x}^{0}] z \ne 0$	$\sqrt{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
`Sqrt`	$\sqrt{z}$	Principal square root
`OpenClosedInterval`	$\left(a, b\right]$	Open-closed interval
`Infinity`	$\infty$	Positive infinity
`OpenInterval`	$\left(a, b\right)$	Open interval
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval
`CC`	$\mathbb{C}$	Complex numbers
`UnsignedInfinity`	${\tilde \infty}$	Unsigned infinity
`SetBuilder`	$\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}$	Set comprehension
`Exp`	${e}^{z}$	Exponential function
`ConstI`	$i$	Imaginary unit
`ConstPi`	$\pi$	The constant pi (3.14...)
`FormalPowerSeries`	$K[[x]]$	Formal power series
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("21d9b8"),
    SymbolDefinition(Sqrt, Sqrt(z), "Principal square root"),
    Description("The principal square root", Sqrt(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(Sqrt(z)), "is defined in Fungrim."),
    Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(TableSection("Numbers"), Tuple(Element(z, ClosedOpenInterval(0, Infinity)), Element(Sqrt(z), ClosedOpenInterval(0, Infinity))), Tuple(Element(z, CC), Element(Sqrt(z), CC)), TableSection("Infinities"), Tuple(Element(z, Set(UnsignedInfinity)), Element(Sqrt(z), Set(UnsignedInfinity))), Tuple(Element(z, SetBuilder(Mul(Exp(Mul(ConstI, theta)), Infinity), theta, Element(theta, OpenClosedInterval(Neg(ConstPi), ConstPi)))), Element(Sqrt(z), SetBuilder(Mul(Exp(Mul(ConstI, theta)), Infinity), theta, Element(theta, OpenClosedInterval(Div(Neg(ConstPi), 2), Div(ConstPi, 2)))))), TableSection("Formal power series"), Tuple(And(Element(z, FormalPowerSeries(RR, x)), Element(SeriesCoefficient(z, x, 0), OpenInterval(0, Infinity))), And(Element(Sqrt(z), FormalPowerSeries(RR, x)))), Tuple(And(Element(z, FormalPowerSeries(CC, x)), Unequal(SeriesCoefficient(z, x, 0), 0)), And(Element(Sqrt(z), FormalPowerSeries(CC, x)))))))

Topics using this entry

Square roots