# 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)`.

## Tags #

square root

source
noncomputable def NNReal.sqrt :
NNReal ≃o NNReal

Square root of a nonnegative real number.

Equations

- NNReal.sqrt = (NNReal.powOrderIso 2 NNReal.sqrt._proof_1).symm

Instances For

source
@[simp]
theorem NNReal.sq_sqrt (x : NNReal) :
sqrt x ^ 2 = x
source
@[simp]
theorem NNReal.sqrt_sq (x : NNReal) :
sqrt (x ^ 2) = x
source
@[simp]
theorem NNReal.mul_self_sqrt (x : NNReal) :
sqrt x * sqrt x = x
source
@[simp]
theorem NNReal.sqrt_mul_self (x : NNReal) :
sqrt (x * x) = x
source
theorem NNReal.sqrt_le_sqrt {x y : NNReal} :
sqrt x ≤ sqrt y ↔ x ≤ y
source
theorem NNReal.sqrt_lt_sqrt {x y : NNReal} :
sqrt x < sqrt y ↔ x < y
source
theorem NNReal.sqrt_eq_iff_eq_sq {x y : NNReal} :
sqrt x = y ↔ x = y ^ 2
source
theorem NNReal.sqrt_le_iff_le_sq {x y : NNReal} :
sqrt x ≤ y ↔ x ≤ y ^ 2
source
theorem NNReal.le_sqrt_iff_sq_le {x y : NNReal} :
x ≤ sqrt y ↔ x ^ 2 ≤ y
source
@[simp]
theorem NNReal.sqrt_eq_zero {x : NNReal} :
sqrt x = 0 ↔ x = 0
source
@[simp]
theorem NNReal.sqrt_eq_one {x : NNReal} :
sqrt x = 1 ↔ x = 1
source
@[simp]
theorem NNReal.sqrt_zero :
sqrt 0 = 0
source
@[simp]
theorem NNReal.sqrt_one :
sqrt 1 = 1
source
@[simp]
theorem NNReal.sqrt_le_one {x : NNReal} :
sqrt x ≤ 1 ↔ x ≤ 1
source
@[simp]
theorem NNReal.one_le_sqrt {x : NNReal} :
1 ≤ sqrt x ↔ 1 ≤ x
source
theorem NNReal.sqrt_mul (x y : NNReal) :
sqrt (x * y) = sqrt x * sqrt y
source
noncomputable def NNReal.sqrtHom :
NNReal →*₀ NNReal

`NNReal.sqrt` as a `MonoidWithZeroHom`.

Equations

- NNReal.sqrtHom = { toFun := ⇑NNReal.sqrt, map_zero' := NNReal.sqrt_zero, map_one' := NNReal.sqrt_one, map_mul' := NNReal.sqrt_mul }

Instances For

source
theorem NNReal.sqrt_inv (x : NNReal) :
sqrt x⁻¹ = (sqrt x)⁻¹
source
theorem NNReal.sqrt_div (x y : NNReal) :
sqrt (x / y) = sqrt x / sqrt y
source
theorem NNReal.continuous_sqrt :
Continuous ⇑sqrt
source
@[simp]
theorem NNReal.sqrt_pos {x : NNReal} :
0 < sqrt x ↔ 0 < x
source
theorem NNReal.sqrt_pos_of_pos {x : NNReal} :
0 < x → 0 < sqrt x

Alias of the reverse direction of `NNReal.sqrt_pos`.

source
@[simp]
theorem NNReal.isSquare (x : NNReal) :
IsSquare x
source
noncomputable def Real.sqrt (x : ℝ) :
ℝ

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

This has notation `√x`. Note that `√x⁻¹` is parsed as `√(x⁻¹)`.

Equations

- √x = ↑(NNReal.sqrt x.toNNReal)

Instances For

source
def Real.«term√_» :
Lean.ParserDescr

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

This has notation `√x`. Note that `√x⁻¹` is parsed as `√(x⁻¹)`.

Equations

- Real.«term√_» = Lean.ParserDescr.node `Real.«term√_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "√") (Lean.ParserDescr.cat `term 1024))

Instances For

source
@[simp]
theorem Real.coe_sqrt {x : NNReal} :
↑(NNReal.sqrt x) = √↑x
source
theorem Real.continuous_sqrt :
Continuous fun (x : ℝ) => √x
source
theorem Real.sqrt_eq_zero_of_nonpos {x : ℝ} (h : x ≤ 0) :
√x = 0
source
@[simp]
theorem Real.sqrt_nonneg (x : ℝ) :
0 ≤ √x
source
@[simp]
theorem Real.mul_self_sqrt {x : ℝ} (h : 0 ≤ x) :
√x * √x = x
source
@[simp]
theorem Real.sqrt_mul_self {x : ℝ} (h : 0 ≤ x) :
√(x * x) = x
source
theorem Real.sqrt_eq_cases {x y : ℝ} :
√x = y ↔ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0
source
theorem Real.sqrt_eq_iff_mul_self_eq {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) :
√x = y ↔ x = y * y
source
theorem Real.sqrt_eq_iff_mul_self_eq_of_pos {x y : ℝ} (h : 0 < y) :
√x = y ↔ y * y = x
source
@[simp]
theorem Real.sqrt_eq_one {x : ℝ} :
√x = 1 ↔ x = 1
source
@[simp]
theorem Real.sq_sqrt {x : ℝ} (h : 0 ≤ x) :
√x ^ 2 = x
source
@[simp]
theorem Real.sqrt_sq {x : ℝ} (h : 0 ≤ x) :
√(x ^ 2) = x
source
theorem Real.sqrt_eq_iff_eq_sq {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) :
√x = y ↔ x = y ^ 2
source
theorem Real.sqrt_mul_self_eq_abs (x : ℝ) :
√(x * x) = |x|
source
theorem Real.sqrt_sq_eq_abs (x : ℝ) :
√(x ^ 2) = |x|
source
@[simp]
theorem Real.sqrt_zero :
√0 = 0
source
@[simp]
theorem Real.sqrt_one :
√1 = 1
source
@[simp]
theorem Real.sqrt_le_sqrt_iff {x y : ℝ} (hy : 0 ≤ y) :
√x ≤ √y ↔ x ≤ y
source
@[simp]
theorem Real.sqrt_lt_sqrt_iff {x y : ℝ} (hx : 0 ≤ x) :
√x < √y ↔ x < y
source
theorem Real.sqrt_lt_sqrt_iff_of_pos {x y : ℝ} (hy : 0 < y) :
√x < √y ↔ x < y
source
theorem Real.sqrt_le_sqrt {x y : ℝ} (h : x ≤ y) :
√x ≤ √y
source
theorem Real.sqrt_monotone :
Monotone sqrt
source
theorem Real.sqrt_lt_sqrt {x y : ℝ} (hx : 0 ≤ x) (h : x < y) :
√x < √y
source
theorem Real.sqrt_le_left {x y : ℝ} (hy : 0 ≤ y) :
√x ≤ y ↔ x ≤ y ^ 2
source
theorem Real.sqrt_le_iff {x y : ℝ} :
√x ≤ y ↔ 0 ≤ y ∧ x ≤ y ^ 2
source
theorem Real.sqrt_lt {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) :
√x < y ↔ x < y ^ 2
source
theorem Real.sqrt_lt' {x y : ℝ} (hy : 0 < y) :
√x < y ↔ x < y ^ 2
source
theorem Real.le_sqrt {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) :
x ≤ √y ↔ x ^ 2 ≤ y

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

source
theorem Real.le_sqrt' {x y : ℝ} (hx : 0 < x) :
x ≤ √y ↔ x ^ 2 ≤ y
source
theorem Real.abs_le_sqrt {x y : ℝ} (h : x ^ 2 ≤ y) :
|x| ≤ √y
source
theorem Real.sq_le {x y : ℝ} (h : 0 ≤ y) :
x ^ 2 ≤ y ↔ -√y ≤ x ∧ x ≤ √y
source
theorem Real.neg_sqrt_le_of_sq_le {x y : ℝ} (h : x ^ 2 ≤ y) :
-√y ≤ x
source
theorem Real.le_sqrt_of_sq_le {x y : ℝ} (h : x ^ 2 ≤ y) :
x ≤ √y
source
@[simp]
theorem Real.sqrt_inj {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) :
√x = √y ↔ x = y
source
@[simp]
theorem Real.sqrt_eq_zero {x : ℝ} (h : 0 ≤ x) :
√x = 0 ↔ x = 0
source
theorem Real.sqrt_eq_zero' {x : ℝ} :
√x = 0 ↔ x ≤ 0
source
theorem Real.sqrt_ne_zero {x : ℝ} (h : 0 ≤ x) :
√x ≠ 0 ↔ x ≠ 0
source
theorem Real.sqrt_ne_zero' {x : ℝ} :
√x ≠ 0 ↔ 0 < x
source
theorem Real.sq_sqrt' {x : ℝ} :
√x ^ 2 = max x 0

Variant of `sq_sqrt` without a non-negativity assumption on `x`.

source
@[simp]
theorem Real.sqrt_pos {x : ℝ} :
0 < √x ↔ 0 < x
source
theorem Real.sqrt_pos_of_pos {x : ℝ} :
0 < x → 0 < √x

Alias of the reverse direction of `Real.sqrt_pos`.

source
theorem Real.sqrt_le_sqrt_iff' {x y : ℝ} (hx : 0 < x) :
√x ≤ √y ↔ x ≤ y
source
@[simp]
theorem Real.one_le_sqrt {x : ℝ} :
1 ≤ √x ↔ 1 ≤ x
source
@[simp]
theorem Real.sqrt_le_one {x : ℝ} :
√x ≤ 1 ↔ x ≤ 1
source
@[simp]
theorem Real.isSquare_iff {x : ℝ} :
IsSquare x ↔ 0 ≤ x
source
def Mathlib.Meta.Positivity.evalNNRealSqrt :
PositivityExt

Extension for the `positivity` tactic: a square root of a strictly positive nonnegative real is positive.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Meta.Positivity.evalSqrt :
PositivityExt

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem Real.one_lt_sqrt_two :
1 < √2
source
theorem Real.sqrt_two_lt_three_halves :
√2 < 3 / 2
source
theorem Real.inv_sqrt_two_sub_one :
(√2 - 1)⁻¹ = √2 + 1
source
@[simp]
theorem Real.sqrt_mul {x : ℝ} (hx : 0 ≤ x) (y : ℝ) :
√(x * y) = √x * √y
source
@[simp]
theorem Real.sqrt_mul' (x : ℝ) {y : ℝ} (hy : 0 ≤ y) :
√(x * y) = √x * √y
source
@[simp]
theorem Real.sqrt_inv (x : ℝ) :
√x⁻¹ = (√x)⁻¹
source
@[simp]
theorem Real.sqrt_div {x : ℝ} (hx : 0 ≤ x) (y : ℝ) :
√(x / y) = √x / √y
source
@[simp]
theorem Real.sqrt_div' (x : ℝ) {y : ℝ} (hy : 0 ≤ y) :
√(x / y) = √x / √y
source
@[simp]
theorem Real.div_sqrt {x : ℝ} :
x / √x = √x
source
theorem Real.sqrt_div_self' {x : ℝ} :
√x / x = 1 / √x
source
theorem Real.sqrt_div_self {x : ℝ} :
√x / x = (√x)⁻¹
source
theorem Real.lt_sqrt {x y : ℝ} (hx : 0 ≤ x) :
x < √y ↔ x ^ 2 < y
source
theorem Real.sq_lt {x y : ℝ} :
x ^ 2 < y ↔ -√y < x ∧ x < √y
source
theorem Real.neg_sqrt_lt_of_sq_lt {x y : ℝ} (h : x ^ 2 < y) :
-√y < x
source
theorem Real.lt_sqrt_of_sq_lt {x y : ℝ} (h : x ^ 2 < y) :
x < √y
source
theorem Real.lt_sq_of_sqrt_lt {x y : ℝ} (h : √x < y) :
x < y ^ 2
source
theorem Real.nat_sqrt_le_real_sqrt {a : ℕ} :
↑a.sqrt ≤ √↑a

The natural square root is at most the real square root

source
theorem Real.real_sqrt_lt_nat_sqrt_succ {a : ℕ} :
√↑a < ↑a.sqrt + 1

The real square root is less than the natural square root plus one

source
theorem Real.real_sqrt_le_nat_sqrt_succ {a : ℕ} :
√↑a ≤ ↑a.sqrt + 1

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

source
@[simp]
theorem Real.floor_real_sqrt_eq_nat_sqrt {a : ℕ} :
⌊√↑a⌋ = ↑a.sqrt

The floor of the real square root is the same as the natural square root.

source
@[simp]
theorem Real.nat_floor_real_sqrt_eq_nat_sqrt {a : ℕ} :
⌊√↑a⌋₊ = a.sqrt

The natural floor of the real square root is the same as the natural square root.

source
theorem Real.sqrt_one_add_le {x : ℝ} (h : -1 ≤ x) :
√(1 + x) ≤ 1 + x / 2

Bernoulli's inequality for exponent `1 / 2`, stated using `sqrt`.

source
theorem Filter.Tendsto.sqrt {α : Type u_1} {f : α → ℝ} {l : Filter α} {x : ℝ} (h : Tendsto f l (nhds x)) :
Tendsto (fun (x : α) => √(f x)) l (nhds √x)
source
theorem ContinuousWithinAt.sqrt {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} {s : Set α} {x : α} (h : ContinuousWithinAt f s x) :
ContinuousWithinAt (fun (x : α) => √(f x)) s x
source
theorem ContinuousAt.sqrt {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} {x : α} (h : ContinuousAt f x) :
ContinuousAt (fun (x : α) => √(f x)) x
source
theorem ContinuousOn.sqrt {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} {s : Set α} (h : ContinuousOn f s) :
ContinuousOn (fun (x : α) => √(f x)) s
source
theorem Continuous.sqrt {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} (h : Continuous f) :
Continuous fun (x : α) => √(f x)
source
theorem NNReal.sum_mul_le_sqrt_mul_sqrt {ι : Type u_2} (s : Finset ι) (f g : ι → NNReal) :
∑ i ∈ s, f i * g i ≤ sqrt (∑ i ∈ s, f i ^ 2) * sqrt (∑ i ∈ s, g i ^ 2)

Cauchy-Schwarz inequality for finsets using square roots in `ℝ≥0`.

source
theorem NNReal.sum_sqrt_mul_sqrt_le {ι : Type u_2} (s : Finset ι) (f g : ι → NNReal) :
∑ i ∈ s, sqrt (f i) * sqrt (g i) ≤ sqrt (∑ i ∈ s, f i) * sqrt (∑ i ∈ s, g i)

Cauchy-Schwarz inequality for finsets using square roots in `ℝ≥0`.

source
theorem Real.sum_mul_le_sqrt_mul_sqrt {ι : Type u_2} (s : Finset ι) (f g : ι → ℝ) :
∑ i ∈ s, f i * g i ≤ √(∑ i ∈ s, f i ^ 2) * √(∑ i ∈ s, g i ^ 2)

Cauchy-Schwarz inequality for finsets using square roots in `ℝ`.

source
theorem Real.sum_sqrt_mul_sqrt_le {ι : Type u_2} {f g : ι → ℝ} (s : Finset ι) (hf : ∀ (i : ι), 0 ≤ f i) (hg : ∀ (i : ι), 0 ≤ g i) :
∑ i ∈ s, √(f i) * √(g i) ≤ √(∑ i ∈ s, f i) * √(∑ i ∈ s, g i)

Cauchy-Schwarz inequality for finsets using square roots in `ℝ`.