Square root of a real number #
In this file we define
NNReal.sqrt
to be the square root of a nonnegative real number.Real.sqrt
to be the square root of a real number, defined to be zero on negative numbers.
Then we prove some basic properties of these functions.
Implementation notes #
We define NNReal.sqrt
as the noncomputable inverse to the function x ↦ x * x
. We use general
theory of inverses of strictly monotone functions to prove that NNReal.sqrt x
exists. As a side
effect, NNReal.sqrt
is a bundled OrderIso
, so for NNReal
numbers we get continuity as well as
theorems like NNReal.sqrt x ≤ y ↔ x ≤ y * y
for free.
Then we define Real.sqrt x
to be NNReal.sqrt (Real.toNNReal x)
.
Tags #
square root
Square root of a nonnegative real number.
Equations
Instances For
Alias of the reverse direction of NNReal.sqrt_pos
.
The square root of a real number. This returns 0 for negative inputs.
This has notation √x
. Note that √x⁻¹
is parsed as √(x⁻¹)
.
Equations
Instances For
Note: if you want to conclude x ≤ √y
, then use Real.le_sqrt_of_sq_le
.
If you have x > 0
, consider using Real.le_sqrt'
Alias of the reverse direction of Real.sqrt_pos
.
Extension for the positivity
tactic: a square root of a strictly positive nonnegative real is
positive.
Equations
Instances For
Extension for the positivity
tactic: a square root is nonnegative, and is strictly positive if
its input is.