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

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 :

nnreal ≃o nnreal

Square root of a nonnegative real number.

Equations

nnreal.sqrt = (nnreal.pow_order_iso 2 nnreal.sqrt._proof_1).symm

theorem nnreal.sqrt_le_sqrt_iff {x y : nnreal} :

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

theorem nnreal.sqrt_lt_sqrt_iff {x y : nnreal} :

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

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

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

theorem nnreal.le_sqrt_iff {x y : nnreal} :

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

@[simp]

theorem nnreal.sqrt_eq_zero {x : nnreal} :

⇑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.sq_sqrt (x : nnreal) :

⇑nnreal.sqrt x ^ 2 = x

@[simp]

theorem nnreal.mul_self_sqrt (x : nnreal) :

⇑nnreal.sqrt x * ⇑nnreal.sqrt x = 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 y : nnreal) :

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

noncomputable def nnreal.sqrt_hom :

nnreal →*₀ nnreal

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

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

theorem nnreal.sqrt_div (x y : nnreal) :

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

theorem nnreal.continuous_sqrt :

continuous ⇑nnreal.sqrt

def real.sqrt_aux (f : cau_seq ℚ 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

real.sqrt_aux f (n + 1) = let s : ℚ := real.sqrt_aux f n in linear_order.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 ℚ has_abs.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

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

@[simp, norm_cast]

theorem real.coe_sqrt {x : nnreal} :

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

@[continuity]

theorem real.continuous_sqrt :

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

√ x = 0

theorem real.sqrt_nonneg (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) :

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

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

√ 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.

meta def tactic.positivity_sqrt :

expr → tactic tactic.positivity.strictness

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

√ x⁻¹ = (√ 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

theorem real.nat_sqrt_le_real_sqrt {a : ℕ} :

↑(nat.sqrt a) ≤ √ ↑a

The natural square root is at most the real square root

theorem real.real_sqrt_le_nat_sqrt_succ {a : ℕ} :

√ ↑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 = star_ordered_ring.of_nonneg_iff' real.star_ordered_ring._proof_1 real.star_ordered_ring._proof_2

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