mathlib documentation

data.real.sqrt

Square root of a real number #

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 * x ≤ 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

Square root of a nonnegative real number.

Equations
theorem nnreal.sqrt_eq_iff_sq_eq {x y : ℝ≥0} :
nnreal.sqrt x = y y * y = x
theorem nnreal.sqrt_le_iff {x y : ℝ≥0} :
theorem nnreal.le_sqrt_iff {x y : ℝ≥0} :
@[simp]
theorem nnreal.sqrt_eq_zero {x : ℝ≥0} :
@[simp]
@[simp]
theorem nnreal.sqrt_one  :
@[simp]
theorem nnreal.sqrt_mul_self (x : ℝ≥0) :
@[simp]
theorem nnreal.sq_sqrt (x : ℝ≥0) :
@[simp]
theorem nnreal.sqrt_sq (x : ℝ≥0) :
def real.sqrt_aux (f : cau_seq abs) :

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

Equations
def real.sqrt (x : ) :

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

Equations
@[simp]
theorem real.sqrt_eq_zero_of_nonpos {x : } (h : x 0) :
theorem real.sqrt_nonneg (x : ) :
@[simp]
theorem real.mul_self_sqrt {x : } (h : 0 x) :
@[simp]
theorem real.sqrt_mul_self {x : } (h : 0 x) :
real.sqrt (x * x) = x
theorem real.sqrt_eq_iff_mul_self_eq {x y : } (hx : 0 x) (hy : 0 y) :
real.sqrt x = y y * y = x
@[simp]
theorem real.sq_sqrt {x : } (h : 0 x) :
real.sqrt 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) :
real.sqrt x = 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  :
@[simp]
theorem real.sqrt_one  :
@[simp]
theorem real.sqrt_le_sqrt_iff {x y : } (hy : 0 y) :
@[simp]
theorem real.sqrt_lt_sqrt_iff {x y : } (hx : 0 x) :
theorem real.sqrt_lt_sqrt_iff_of_pos {x y : } (hy : 0 < 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) :
real.sqrt x y x y ^ 2
theorem real.sqrt_le_iff {x y : } :
real.sqrt x y 0 y x y ^ 2
theorem real.le_sqrt {x y : } (hx : 0 x) (hy : 0 y) :
x real.sqrt y x ^ 2 y
theorem real.le_sqrt' {x y : } (hx : 0 < x) :
x real.sqrt y x ^ 2 y
theorem real.abs_le_sqrt {x y : } (h : x ^ 2 y) :
theorem real.sq_le {x y : } (h : 0 y) :
theorem real.neg_sqrt_le_of_sq_le {x y : } (h : x ^ 2 y) :
theorem real.le_sqrt_of_sq_le {x y : } (h : x ^ 2 y) :
@[simp]
theorem real.sqrt_inj {x y : } (hx : 0 x) (hy : 0 y) :
@[simp]
theorem real.sqrt_eq_zero {x : } (h : 0 x) :
real.sqrt x = 0 x = 0
theorem real.sqrt_eq_zero' {x : } :
real.sqrt x = 0 x 0
theorem real.sqrt_ne_zero {x : } (h : 0 x) :
theorem real.sqrt_ne_zero' {x : } :
real.sqrt x 0 0 < x
@[simp]
theorem real.sqrt_pos {x : } :
0 < real.sqrt x 0 < x
@[simp]
theorem real.sqrt_mul {x : } (hx : 0 x) (y : ) :
@[simp]
theorem real.sqrt_mul' (x : ) {y : } (hy : 0 y) :
@[simp]
@[simp]
theorem real.sqrt_div {x : } (hx : 0 x) (y : ) :
@[simp]
theorem real.div_sqrt {x : } :
theorem real.lt_sqrt {x y : } (hx : 0 x) (hy : 0 y) :
x < real.sqrt y x ^ 2 < y
theorem real.sq_lt {x y : } :
x ^ 2 < y -real.sqrt y < x x < real.sqrt y
theorem real.neg_sqrt_lt_of_sq_lt {x y : } (h : x ^ 2 < y) :
theorem real.lt_sqrt_of_sq_lt {x y : } (h : x ^ 2 < y) :
theorem filter.tendsto.sqrt {α : Type u_1} {f : α → } {l : filter α} {x : } (h : filter.tendsto f l (𝓝 x)) :
filter.tendsto (λ (x : α), real.sqrt (f x)) l (𝓝 (real.sqrt 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 : α), real.sqrt (f x)) s x
theorem continuous_at.sqrt {α : Type u_1} [topological_space α] {f : α → } {x : α} (h : continuous_at f x) :
continuous_at (λ (x : α), real.sqrt (f x)) x
theorem continuous_on.sqrt {α : Type u_1} [topological_space α] {f : α → } {s : set α} (h : continuous_on f s) :
continuous_on (λ (x : α), real.sqrt (f x)) s
theorem continuous.sqrt {α : Type u_1} [topological_space α] {f : α → } (h : continuous f) :
continuous (λ (x : α), real.sqrt (f x))