# Documentation

Mathlib.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 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). We also define a Cauchy sequence Real.sqrtAux (f : CauSeq ℚ abs) which converges to Real.sqrt (mk f) but do not prove (yet) that this sequence actually converges to Real.sqrt (mk f).

## Tags #

square root

noncomputable def NNReal.sqrt :

Square root of a nonnegative real number.

Instances For
theorem NNReal.sqrt_lt_sqrt_iff {x : NNReal} {y : NNReal} :
< x < y
theorem NNReal.sqrt_eq_iff_sq_eq {x : NNReal} {y : NNReal} :
= y y ^ 2 = x
theorem NNReal.sqrt_le_iff {x : NNReal} {y : NNReal} :
y x y ^ 2
theorem NNReal.le_sqrt_iff {x : NNReal} {y : NNReal} :
x x ^ 2 y
@[simp]
theorem NNReal.sqrt_eq_zero {x : NNReal} :
= 0 x = 0
@[simp]
theorem NNReal.sqrt_zero :
= 0
@[simp]
theorem NNReal.sqrt_one :
= 1
@[simp]
theorem NNReal.sq_sqrt (x : NNReal) :
^ 2 = x
@[simp]
theorem NNReal.mul_self_sqrt (x : NNReal) :
* = x
@[simp]
theorem NNReal.sqrt_sq (x : NNReal) :
NNReal.sqrt (x ^ 2) = x
@[simp]
theorem NNReal.sqrt_mul_self (x : NNReal) :
NNReal.sqrt (x * x) = x
theorem NNReal.sqrt_mul (x : NNReal) (y : NNReal) :
NNReal.sqrt (x * y) = *
noncomputable def NNReal.sqrtHom :

NNReal.sqrt as a MonoidWithZeroHom.

Instances For
theorem NNReal.sqrt_div (x : NNReal) (y : NNReal) :
NNReal.sqrt (x / y) = /
@[simp]
theorem NNReal.sqrt_pos {x : NNReal} :
0 < 0 < x
theorem NNReal.sqrt_pos_of_pos {x : NNReal} :
0 < x0 <

Alias of the reverse direction of NNReal.sqrt_pos.

def Real.sqrtAux (f : CauSeq abs) :

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

Equations
Instances For
theorem Real.sqrtAux_nonneg (f : CauSeq abs) (i : ) :
0
noncomputable def Real.sqrt (x : ) :

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

Instances For
@[simp]
theorem Real.coe_sqrt {x : NNReal} :
↑() =
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_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

Note: if you want to conclude x ≤ Real.sqrt y, then use Real.le_sqrt_of_sq_le. If you have x > 0, consider using Real.le_sqrt'

theorem Real.le_sqrt' {x : } {y : } (hx : 0 < x) :
x x ^ 2 y
theorem Real.abs_le_sqrt {x : } {y : } (h : x ^ 2 y) :
|x|
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 of a strictly positive nonnegative real is positive.

Instances For

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

Instances For
@[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.sqrt_div' (x : ) {y : } (hy : 0 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 : } :
/ 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
theorem Real.nat_sqrt_le_real_sqrt {a : } :
↑()

The natural square root is at most the real square root

theorem Real.real_sqrt_le_nat_sqrt_succ {a : } :
↑() + 1

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

Although the instance IsROrC.toStarOrderedRing exists, it is locked behind the ComplexOrder scope because currently the order on ℂ is not enabled globally. But we want StarOrderedRing ℝ to be available globally, so we include this instance separately. In addition, providing this instance here makes it available earlier in the import hierarchy; otherwise in order to access it we would need to import Data.IsROrC.Basic

theorem Filter.Tendsto.sqrt {α : Type u_1} {f : α} {l : } {x : } (h : Filter.Tendsto f l (nhds x)) :
Filter.Tendsto (fun x => Real.sqrt (f x)) l (nhds ())
theorem ContinuousWithinAt.sqrt {α : Type u_1} [] {f : α} {s : Set α} {x : α} (h : ) :
ContinuousWithinAt (fun x => Real.sqrt (f x)) s x
theorem ContinuousAt.sqrt {α : Type u_1} [] {f : α} {x : α} (h : ) :
ContinuousAt (fun x => Real.sqrt (f x)) x
theorem ContinuousOn.sqrt {α : Type u_1} [] {f : α} {s : Set α} (h : ) :
ContinuousOn (fun x => Real.sqrt (f x)) s
theorem Continuous.sqrt {α : Type u_1} [] {f : α} (h : ) :
Continuous fun x => Real.sqrt (f x)