mathlib documentation

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

noncomputable def nnreal.sqrt :

ℝ≥0 ≃o ℝ≥0

Square root of a nonnegative real number.

Equations

nnreal.sqrt = (strict_mono.order_iso_of_surjective (λ (x : ℝ≥0), x * x) nnreal.sqrt._proof_1 nnreal.sqrt._proof_2).symm

theorem nnreal.sqrt_le_sqrt_iff {x y : ℝ≥0} :

⇑nnreal.sqrt x ≤ ⇑nnreal.sqrt y ↔ x ≤ y

theorem nnreal.sqrt_lt_sqrt_iff {x y : ℝ≥0} :

⇑nnreal.sqrt x < ⇑nnreal.sqrt y ↔ x < y

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} :

⇑nnreal.sqrt x ≤ y ↔ x ≤ y * y

theorem nnreal.le_sqrt_iff {x y : ℝ≥0} :

x ≤ ⇑nnreal.sqrt y ↔ x * x ≤ y

@[simp]

theorem nnreal.sqrt_eq_zero {x : ℝ≥0} :

⇑nnreal.sqrt x = 0 ↔ x = 0

@[simp]

theorem nnreal.sqrt_zero :

⇑nnreal.sqrt 0 = 0

@[simp]

theorem nnreal.sqrt_one :

⇑nnreal.sqrt 1 = 1

@[simp]

theorem nnreal.mul_self_sqrt (x : ℝ≥0) :

(⇑nnreal.sqrt x) * ⇑nnreal.sqrt x = x

@[simp]

theorem nnreal.sqrt_mul_self (x : ℝ≥0) :

⇑nnreal.sqrt (x * x) = x

@[simp]

theorem nnreal.sq_sqrt (x : ℝ≥0) :

⇑nnreal.sqrt x ^ 2 = x

@[simp]

theorem nnreal.sqrt_sq (x : ℝ≥0) :

⇑nnreal.sqrt (x ^ 2) = x

theorem nnreal.sqrt_mul (x y : ℝ≥0) :

⇑nnreal.sqrt (x * y) = (⇑nnreal.sqrt x) * ⇑nnreal.sqrt y

noncomputable def nnreal.sqrt_hom :

ℝ≥0 →*₀ ℝ≥0

nnreal.sqrt as a monoid_with_zero_hom.

Equations

nnreal.sqrt_hom = {to_fun := ⇑nnreal.sqrt, map_zero' := nnreal.sqrt_zero, map_one' := nnreal.sqrt_one, map_mul' := nnreal.sqrt_mul}

theorem nnreal.sqrt_inv (x : ℝ≥0) :

⇑nnreal.sqrt x⁻¹ = (⇑nnreal.sqrt x)⁻¹

theorem nnreal.sqrt_div (x y : ℝ≥0) :

⇑nnreal.sqrt (x / y) = ⇑nnreal.sqrt x / ⇑nnreal.sqrt y

theorem nnreal.continuous_sqrt :

continuous ⇑nnreal.sqrt

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

real.sqrt_aux f (n + 1) = let s : ℚ := real.sqrt_aux f n in max 0 ((s + ⇑f (n + 1) / s) / 2)
real.sqrt_aux f 0 = rat.mk_nat ↑(nat.sqrt (⇑f 0).num.to_nat) (nat.sqrt (⇑f 0).denom)

theorem real.sqrt_aux_nonneg (f : cau_seq ℚ abs) (i : ℕ) :

0 ≤ real.sqrt_aux f i

noncomputable def real.sqrt (x : ℝ) :

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

Equations

real.sqrt x = ↑(⇑nnreal.sqrt x.to_nnreal)

@[simp, norm_cast]

theorem real.coe_sqrt {x : ℝ≥0} :

↑(⇑nnreal.sqrt x) = real.sqrt ↑x

@[continuity]

theorem real.continuous_sqrt :

continuous real.sqrt

theorem real.sqrt_eq_zero_of_nonpos {x : ℝ} (h : x ≤ 0) :

real.sqrt x = 0

theorem real.sqrt_nonneg (x : ℝ) :

0 ≤ real.sqrt x

@[simp]

theorem real.mul_self_sqrt {x : ℝ} (h : 0 ≤ x) :

(real.sqrt x) * real.sqrt x = x

@[simp]

theorem real.sqrt_mul_self {x : ℝ} (h : 0 ≤ x) :

real.sqrt (x * x) = x

theorem real.sqrt_eq_cases {x y : ℝ} :

real.sqrt 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) :

real.sqrt x = y ↔ y * y = x

theorem real.sqrt_eq_iff_mul_self_eq_of_pos {x y : ℝ} (h : 0 < y) :

real.sqrt x = y ↔ y * y = x

@[simp]

theorem real.sqrt_eq_one {x : ℝ} :

real.sqrt x = 1 ↔ x = 1

@[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 :

real.sqrt 0 = 0

@[simp]

theorem real.sqrt_one :

real.sqrt 1 = 1

@[simp]

theorem real.sqrt_le_sqrt_iff {x y : ℝ} (hy : 0 ≤ y) :

real.sqrt x ≤ real.sqrt y ↔ x ≤ y

@[simp]

theorem real.sqrt_lt_sqrt_iff {x y : ℝ} (hx : 0 ≤ x) :

real.sqrt x < real.sqrt y ↔ x < y

theorem real.sqrt_lt_sqrt_iff_of_pos {x y : ℝ} (hy : 0 < y) :

real.sqrt x < real.sqrt y ↔ x < y

theorem real.sqrt_le_sqrt {x y : ℝ} (h : x ≤ y) :

real.sqrt x ≤ real.sqrt y

theorem real.sqrt_lt_sqrt {x y : ℝ} (hx : 0 ≤ x) (h : x < y) :

real.sqrt x < real.sqrt 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.sqrt_lt {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) :

real.sqrt x < y ↔ x < y ^ 2

theorem real.sqrt_lt' {x y : ℝ} (hy : 0 < y) :

real.sqrt x < 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) :

|x| ≤ real.sqrt y

theorem real.sq_le {x y : ℝ} (h : 0 ≤ y) :

x ^ 2 ≤ y ↔ -real.sqrt y ≤ x ∧ x ≤ real.sqrt y

theorem real.neg_sqrt_le_of_sq_le {x y : ℝ} (h : x ^ 2 ≤ y) :

-real.sqrt y ≤ x

theorem real.le_sqrt_of_sq_le {x y : ℝ} (h : x ^ 2 ≤ y) :

x ≤ real.sqrt y

@[simp]

theorem real.sqrt_inj {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) :

real.sqrt x = real.sqrt y ↔ x = 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) :

real.sqrt x ≠ 0 ↔ x ≠ 0

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 : ℝ) :

real.sqrt (x * y) = (real.sqrt x) * real.sqrt y

@[simp]

theorem real.sqrt_mul' (x : ℝ) {y : ℝ} (hy : 0 ≤ y) :

real.sqrt (x * y) = (real.sqrt x) * real.sqrt y

@[simp]

theorem real.sqrt_inv (x : ℝ) :

real.sqrt x⁻¹ = (real.sqrt x)⁻¹

@[simp]

theorem real.sqrt_div {x : ℝ} (hx : 0 ≤ x) (y : ℝ) :

real.sqrt (x / y) = real.sqrt x / real.sqrt y

@[simp]

theorem real.div_sqrt {x : ℝ} :

x / real.sqrt x = real.sqrt x

theorem real.sqrt_div_self' {x : ℝ} :

real.sqrt x / x = 1 / real.sqrt x

theorem real.sqrt_div_self {x : ℝ} :

real.sqrt x / x = (real.sqrt x)⁻¹

theorem real.lt_sqrt {x y : ℝ} (hx : 0 ≤ x) :

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) :

-real.sqrt y < x

theorem real.lt_sqrt_of_sq_lt {x y : ℝ} (h : x ^ 2 < y) :

x < real.sqrt y

theorem real.nat_sqrt_le_real_sqrt {a : ℕ} :

↑(nat.sqrt a) ≤ real.sqrt ↑a

The natural square root is at most the real square root

theorem real.real_sqrt_le_nat_sqrt_succ {a : ℕ} :

real.sqrt ↑a ≤ ↑(nat.sqrt a) + 1

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

@[protected, instance]

def real.star_ordered_ring :

star_ordered_ring ℝ

Equations

real.star_ordered_ring = {to_star_ring := real.star_ring, add_le_add_left := _, nonneg_iff := real.star_ordered_ring._proof_1}

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

@[continuity]

theorem continuous.sqrt {α : Type u_1} [topological_space α] {f : α → ℝ} (h : continuous f) :

continuous (λ (x : α), real.sqrt (f x))