mathlib3 documentation

data.real.sqrt

Square root of a real number #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define

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_eq_iff_sq_eq {x y : nnreal} :
nnreal.sqrt x = y y ^ 2 = x
theorem nnreal.sqrt_le_iff {x y : nnreal} :
theorem nnreal.le_sqrt_iff {x y : nnreal} :
@[simp]
theorem nnreal.sqrt_eq_zero {x : nnreal} :
@[simp]
@[simp]
theorem nnreal.sqrt_one  :
@[simp]
theorem nnreal.sq_sqrt (x : nnreal) :
@[simp]
theorem nnreal.sqrt_sq (x : nnreal) :
@[simp]
theorem nnreal.sqrt_mul_self (x : nnreal) :

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

Equations
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) :
x = 0
theorem real.sqrt_nonneg (x : ) :
0 x
@[simp]
theorem real.mul_self_sqrt {x : } (h : 0 x) :
x * x = x
@[simp]
theorem real.sqrt_mul_self {x : } (h : 0 x) :
(x * x) = x
theorem real.sqrt_eq_cases {x y : } :
x = 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) :
x = y y * y = x
theorem real.sqrt_eq_iff_mul_self_eq_of_pos {x y : } (h : 0 < y) :
x = y y * y = x
@[simp]
theorem real.sqrt_eq_one {x : } :
x = 1 x = 1
@[simp]
theorem real.sq_sqrt {x : } (h : 0 x) :
x ^ 2 = x
@[simp]
theorem real.sqrt_sq {x : } (h : 0 x) :
(x ^ 2) = x
theorem real.sqrt_eq_iff_sq_eq {x y : } (hx : 0 x) (hy : 0 y) :
x = y y ^ 2 = x
theorem real.sqrt_mul_self_eq_abs (x : ) :
(x * x) = |x|
theorem real.sqrt_sq_eq_abs (x : ) :
(x ^ 2) = |x|
@[simp]
theorem real.sqrt_zero  :
0 = 0
@[simp]
theorem real.sqrt_one  :
1 = 1
@[simp]
theorem real.sqrt_le_sqrt_iff {x y : } (hy : 0 y) :
x y x y
@[simp]
theorem real.sqrt_lt_sqrt_iff {x y : } (hx : 0 x) :
x < y x < y
theorem real.sqrt_lt_sqrt_iff_of_pos {x y : } (hy : 0 < y) :
x < y x < y
theorem real.sqrt_le_sqrt {x y : } (h : x y) :
x y
theorem real.sqrt_lt_sqrt {x y : } (hx : 0 x) (h : x < y) :
x < y
theorem real.sqrt_le_left {x y : } (hy : 0 y) :
x y x y ^ 2
theorem real.sqrt_le_iff {x y : } :
x y 0 y x y ^ 2
theorem real.sqrt_lt {x y : } (hx : 0 x) (hy : 0 y) :
x < y x < y ^ 2
theorem real.sqrt_lt' {x y : } (hy : 0 < y) :
x < y x < y ^ 2
theorem real.le_sqrt {x y : } (hx : 0 x) (hy : 0 y) :
x y x ^ 2 y
theorem real.le_sqrt' {x y : } (hx : 0 < x) :
x y 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 - y x x y
theorem real.neg_sqrt_le_of_sq_le {x y : } (h : x ^ 2 y) :
- y x
theorem real.le_sqrt_of_sq_le {x y : } (h : x ^ 2 y) :
x y
@[simp]
theorem real.sqrt_inj {x y : } (hx : 0 x) (hy : 0 y) :
x = y x = y
@[simp]
theorem real.sqrt_eq_zero {x : } (h : 0 x) :
x = 0 x = 0
theorem real.sqrt_eq_zero' {x : } :
x = 0 x 0
theorem real.sqrt_ne_zero {x : } (h : 0 x) :
x 0 x 0
theorem real.sqrt_ne_zero' {x : } :
x 0 0 < x
@[simp]
theorem real.sqrt_pos {x : } :
0 < x 0 < x
theorem real.sqrt_pos_of_pos {x : } :
0 < x 0 < x

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 : ) :
(x * y) = x * y
@[simp]
theorem real.sqrt_mul' (x : ) {y : } (hy : 0 y) :
(x * y) = x * y
@[simp]
theorem real.sqrt_inv (x : ) :
@[simp]
theorem real.sqrt_div {x : } (hx : 0 x) (y : ) :
(x / y) = x / y
@[simp]
theorem real.sqrt_div' (x : ) {y : } (hy : 0 y) :
(x / y) = x / y
@[simp]
theorem real.div_sqrt {x : } :
x / x = x
theorem real.sqrt_div_self' {x : } :
x / x = 1 / x
theorem real.sqrt_div_self {x : } :
x / x = ( x)⁻¹
theorem real.lt_sqrt {x y : } (hx : 0 x) :
x < y x ^ 2 < y
theorem real.sq_lt {x y : } :
x ^ 2 < y - y < x x < y
theorem real.neg_sqrt_lt_of_sq_lt {x y : } (h : x ^ 2 < y) :
- y < x
theorem real.lt_sqrt_of_sq_lt {x y : } (h : x ^ 2 < y) :
x < y
theorem real.lt_sq_of_sqrt_lt {x y : } (h : x < 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 : filter.tendsto f l (nhds x)) :
filter.tendsto (λ (x : α), (f x)) l (nhds ( x))
theorem continuous_within_at.sqrt {α : Type u_1} [topological_space α] {f : α } {s : set α} {x : α} (h : continuous_within_at f s x) :
continuous_within_at (λ (x : α), (f x)) s x
theorem continuous_at.sqrt {α : Type u_1} [topological_space α] {f : α } {x : α} (h : continuous_at f x) :
continuous_at (λ (x : α), (f x)) x
theorem continuous_on.sqrt {α : Type u_1} [topological_space α] {f : α } {s : set α} (h : continuous_on f s) :
continuous_on (λ (x : α), (f x)) s
@[continuity]
theorem continuous.sqrt {α : Type u_1} [topological_space α] {f : α } (h : continuous f) :
continuous (λ (x : α), (f x))