Square root of a real number #
In this file we define
nnreal.sqrtto be the square root of a nonnegative real number.
real.sqrtto 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 #
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
nnreal.sqrt is a bundled
order_iso, so for
nnreal numbers we get continuity as well as
sqrt x ≤ y ↔ x * x ≤ y for free.
Then we define
real.sqrt x to be
nnreal.sqrt (nnreal.of_real x). We also define a Cauchy
real.sqrt_aux (f : cau_seq ℚ abs) which converges to
sqrt (mk f) but do not prove (yet)
that this sequence actually converges to
sqrt (mk f).
An auxiliary sequence of rational numbers that converges to
real.sqrt (mk f).
Currently this sequence is not used in