data.real.sqrt

# 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 order_iso, so for nnreal numbers we get continuity as well as theorems like sqrt x ≤ y ↔ x ≤ y * y for free.

Then we define real.sqrt x to be nnreal.sqrt (real.to_nnreal x). We also define a Cauchy sequence 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).

## Tags #

square root

noncomputable def nnreal.sqrt  :

Square root of a nonnegative real number.

Equations
theorem nnreal.sqrt_le_sqrt_iff {x y : nnreal} :
x y
theorem nnreal.sqrt_lt_sqrt_iff {x y : nnreal} :
x < y
theorem nnreal.sqrt_eq_iff_sq_eq {x y : nnreal} :
y * y = x
theorem nnreal.sqrt_le_iff {x y : nnreal} :
x y * y
theorem nnreal.le_sqrt_iff {x y : nnreal} :
x * x y
@[simp]
theorem nnreal.sqrt_eq_zero {x : nnreal} :
x = 0
@[simp]
theorem nnreal.sqrt_zero  :
@[simp]
theorem nnreal.sqrt_one  :
@[simp]
theorem nnreal.mul_self_sqrt (x : nnreal) :
= x
@[simp]
theorem nnreal.sqrt_mul_self (x : nnreal) :
@[simp]
theorem nnreal.sq_sqrt (x : nnreal) :
= x
@[simp]
theorem nnreal.sqrt_sq (x : nnreal) :
theorem nnreal.sqrt_mul (x y : nnreal) :
noncomputable def nnreal.sqrt_hom  :

nnreal.sqrt as a monoid_with_zero_hom.

Equations
theorem nnreal.sqrt_inv (x : nnreal) :
theorem nnreal.sqrt_div (x y : nnreal) :
def real.sqrt_aux (f : has_abs.abs) :

An auxiliary sequence of rational numbers that converges to real.sqrt (mk f). Currently this sequence is not used in mathlib.

Equations
theorem real.sqrt_aux_nonneg (f : has_abs.abs) (i : ) :
0
noncomputable def real.sqrt (x : ) :

The square root of a real number. This returns 0 for negative inputs.

Equations
@[simp, norm_cast]
theorem real.coe_sqrt {x : nnreal} :
@[continuity]
theorem real.sqrt_eq_zero_of_nonpos {x : } (h : x 0) :
= 0
theorem real.sqrt_nonneg (x : ) :
0
@[simp]
theorem real.mul_self_sqrt {x : } (h : 0 x) :
= x
@[simp]
theorem real.sqrt_mul_self {x : } (h : 0 x) :
real.sqrt (x * x) = x
theorem real.sqrt_eq_cases {x y : } :
= y y * y = x 0 y x < 0 y = 0
theorem real.sqrt_eq_iff_mul_self_eq {x y : } (hx : 0 x) (hy : 0 y) :
= y y * y = x
theorem real.sqrt_eq_iff_mul_self_eq_of_pos {x y : } (h : 0 < y) :
= y y * y = x
@[simp]
theorem real.sqrt_eq_one {x : } :
= 1 x = 1
@[simp]
theorem real.sq_sqrt {x : } (h : 0 x) :
^ 2 = x
@[simp]
theorem real.sqrt_sq {x : } (h : 0 x) :
real.sqrt (x ^ 2) = x
theorem real.sqrt_eq_iff_sq_eq {x y : } (hx : 0 x) (hy : 0 y) :
= y y ^ 2 = x
theorem real.sqrt_mul_self_eq_abs (x : ) :
real.sqrt (x * x) = |x|
theorem real.sqrt_sq_eq_abs (x : ) :
real.sqrt (x ^ 2) = |x|
@[simp]
theorem real.sqrt_zero  :
= 0
@[simp]
theorem real.sqrt_one  :
= 1
@[simp]
theorem real.sqrt_le_sqrt_iff {x y : } (hy : 0 y) :
x y
@[simp]
theorem real.sqrt_lt_sqrt_iff {x y : } (hx : 0 x) :
x < y
theorem real.sqrt_lt_sqrt_iff_of_pos {x y : } (hy : 0 < y) :
x < y
theorem real.sqrt_le_sqrt {x y : } (h : x y) :
theorem real.sqrt_lt_sqrt {x y : } (hx : 0 x) (h : x < y) :
theorem real.sqrt_le_left {x y : } (hy : 0 y) :
y x y ^ 2
theorem real.sqrt_le_iff {x y : } :
y 0 y x y ^ 2
theorem real.sqrt_lt {x y : } (hx : 0 x) (hy : 0 y) :
< y x < y ^ 2
theorem real.sqrt_lt' {x y : } (hy : 0 < y) :
< y x < y ^ 2
theorem real.le_sqrt {x y : } (hx : 0 x) (hy : 0 y) :
x x ^ 2 y
theorem real.le_sqrt' {x y : } (hx : 0 < x) :
x x ^ 2 y
theorem real.abs_le_sqrt {x y : } (h : x ^ 2 y) :
theorem real.sq_le {x y : } (h : 0 y) :
x ^ 2 y x x
theorem real.neg_sqrt_le_of_sq_le {x y : } (h : x ^ 2 y) :
x
theorem real.le_sqrt_of_sq_le {x y : } (h : x ^ 2 y) :
x
@[simp]
theorem real.sqrt_inj {x y : } (hx : 0 x) (hy : 0 y) :
x = y
@[simp]
theorem real.sqrt_eq_zero {x : } (h : 0 x) :
= 0 x = 0
theorem real.sqrt_eq_zero' {x : } :
= 0 x 0
theorem real.sqrt_ne_zero {x : } (h : 0 x) :
0 x 0
theorem real.sqrt_ne_zero' {x : } :
0 0 < x
@[simp]
theorem real.sqrt_pos {x : } :
0 < 0 < x
theorem real.sqrt_pos_of_pos {x : } :
0 < x0 <

Alias of the reverse direction of real.sqrt_pos.

Extension for the positivity tactic: a square root is nonnegative, and is strictly positive if its input is.

@[simp]
theorem real.sqrt_mul {x : } (hx : 0 x) (y : ) :
real.sqrt (x * y) =
@[simp]
theorem real.sqrt_mul' (x : ) {y : } (hy : 0 y) :
real.sqrt (x * y) =
@[simp]
theorem real.sqrt_inv (x : ) :
@[simp]
theorem real.sqrt_div {x : } (hx : 0 x) (y : ) :
real.sqrt (x / y) =
@[simp]
theorem real.div_sqrt {x : } :
x / =
theorem real.sqrt_div_self' {x : } :
/ x = 1 /
theorem real.sqrt_div_self {x : } :
theorem real.lt_sqrt {x y : } (hx : 0 x) :
x < x ^ 2 < y
theorem real.sq_lt {x y : } :
x ^ 2 < y < x x <
theorem real.neg_sqrt_lt_of_sq_lt {x y : } (h : x ^ 2 < y) :
< x
theorem real.lt_sqrt_of_sq_lt {x y : } (h : x ^ 2 < y) :
x <
theorem real.lt_sq_of_sqrt_lt {x y : } (h : < y) :
x < y ^ 2

The natural square root is at most the real square root

The real square root is at most the natural square root plus one

@[protected, instance]
Equations
theorem filter.tendsto.sqrt {α : Type u_1} {f : α → } {l : filter α} {x : } (h : (nhds x)) :
filter.tendsto (λ (x : α), real.sqrt (f x)) l (nhds (real.sqrt x))
theorem continuous_within_at.sqrt {α : Type u_1} {f : α → } {s : set α} {x : α} (h : x) :
continuous_within_at (λ (x : α), real.sqrt (f x)) s x
theorem continuous_at.sqrt {α : Type u_1} {f : α → } {x : α} (h : x) :
continuous_at (λ (x : α), real.sqrt (f x)) x
theorem continuous_on.sqrt {α : Type u_1} {f : α → } {s : set α} (h : s) :
continuous_on (λ (x : α), real.sqrt (f x)) s
@[continuity]
theorem continuous.sqrt {α : Type u_1} {f : α → } (h : continuous f) :
continuous (λ (x : α), real.sqrt (f x))