Fungrim home page

Fungrim entry: 21d9b8

Symbol: Sqrt z\sqrt{z} Principal square root
The principal square root z\sqrt{z} 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 Sqrt(z) is defined in Fungrim.
Domain Codomain
Numbers
z[0,)z \in \left[0, \infty\right) z[0,)\sqrt{z} \in \left[0, \infty\right)
zCz \in \mathbb{C} zC\sqrt{z} \in \mathbb{C}
Infinities
z{~}z \in \left\{{\tilde \infty}\right\} z{~}\sqrt{z} \in \left\{{\tilde \infty}\right\}
z{eiθ:θ(π,π]}z \in \left\{ {e}^{i \theta} \infty : \theta \in \left(-\pi, \pi\right] \right\} z{eiθ:θ(π2,π2]}\sqrt{z} \in \left\{ {e}^{i \theta} \infty : \theta \in \left(\frac{-\pi}{2}, \frac{\pi}{2}\right] \right\}
Formal power series
zR[[x]]and[x0]z(0,)z \in \mathbb{R}[[x]] \,\mathbin{\operatorname{and}}\, [{x}^{0}] z \in \left(0, \infty\right) zR[[x]]\sqrt{z} \in \mathbb{R}[[x]]
zC[[x]]and[x0]z0z \in \mathbb{C}[[x]] \,\mathbin{\operatorname{and}}\, [{x}^{0}] z \ne 0 zC[[x]]\sqrt{z} \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
Sqrtz\sqrt{z} Principal square root
OpenClosedInterval(a,b]\left(a, b\right] Open-closed interval
Infinity\infty Positive infinity
OpenInterval(a,b)\left(a, b\right) Open interval
ClosedOpenInterval[a,b)\left[a, b\right) Closed-open interval
CCC\mathbb{C} Complex numbers
UnsignedInfinity~{\tilde \infty} Unsigned infinity
SetBuilder{f ⁣(x):P ⁣(x)}\left\{ f\!\left(x\right) : P\!\left(x\right) \right\} Set comprehension
Expez{e}^{z} Exponential function
ConstIii Imaginary unit
ConstPiπ\pi The constant pi (3.14...)
FormalPowerSeriesK[[x]]K[[x]] Formal power series
RRR\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

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