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). We also define a Cauchy sequence Real.sqrtAux (f : CauSeq ℚ abs) which converges to Real.sqrt (mk f) but do not prove (yet) that this sequence actually converges to Real.sqrt (mk f).

Tags

square root

noncomputable def NNReal.sqrt : NNReal ≃o NNReal

Square root of a nonnegative real number.

Equations

• NNReal.sqrt = OrderIso.symm (NNReal.powOrderIso 2 NNReal.sqrt.proof_1)

@[simp]

theorem NNReal.sq_sqrt (x : NNReal) : NNReal.sqrt x ^ 2 = x

@[simp]

theorem NNReal.sqrt_sq (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_mul_self (x : NNReal) : NNReal.sqrt (x * x) = x

theorem NNReal.sqrt_le_sqrt {x : NNReal} {y : NNReal} : NNReal.sqrt x ≤ NNReal.sqrt y ↔ x ≤ y

theorem NNReal.sqrt_lt_sqrt {x : NNReal} {y : NNReal} : NNReal.sqrt x < NNReal.sqrt y ↔ x < y

theorem NNReal.sqrt_eq_iff_eq_sq {x : NNReal} {y : NNReal} : NNReal.sqrt x = y ↔ x = y ^ 2

theorem NNReal.sqrt_le_iff_le_sq {x : NNReal} {y : NNReal} : NNReal.sqrt x ≤ y ↔ x ≤ y ^ 2

theorem NNReal.le_sqrt_iff_sq_le {x : NNReal} {y : NNReal} : x ≤ NNReal.sqrt y ↔ x ^ 2 ≤ y

@[deprecated NNReal.sqrt_le_sqrt]

theorem NNReal.sqrt_le_sqrt_iff {x : NNReal} {y : NNReal} : NNReal.sqrt x ≤ NNReal.sqrt y ↔ x ≤ y

Alias of NNReal.sqrt_le_sqrt.

@[deprecated NNReal.sqrt_lt_sqrt]

theorem NNReal.sqrt_lt_sqrt_iff {x : NNReal} {y : NNReal} : NNReal.sqrt x < NNReal.sqrt y ↔ x < y

Alias of NNReal.sqrt_lt_sqrt.

@[deprecated NNReal.sqrt_le_iff_le_sq]

theorem NNReal.sqrt_le_iff {x : NNReal} {y : NNReal} : NNReal.sqrt x ≤ y ↔ x ≤ y ^ 2

Alias of NNReal.sqrt_le_iff_le_sq.

@[deprecated NNReal.le_sqrt_iff_sq_le]

theorem NNReal.le_sqrt_iff {x : NNReal} {y : NNReal} : x ≤ NNReal.sqrt y ↔ x ^ 2 ≤ y

Alias of NNReal.le_sqrt_iff_sq_le.

@[deprecated NNReal.sqrt_eq_iff_eq_sq]

theorem NNReal.sqrt_eq_iff_sq_eq {x : NNReal} {y : NNReal} : NNReal.sqrt x = y ↔ x = y ^ 2

Alias of NNReal.sqrt_eq_iff_eq_sq.

@[simp]

theorem NNReal.sqrt_eq_zero {x : NNReal} : NNReal.sqrt x = 0 ↔ x = 0

@[simp]

theorem NNReal.sqrt_eq_one {x : NNReal} : NNReal.sqrt x = 1 ↔ x = 1

@[simp]

theorem NNReal.sqrt_zero : NNReal.sqrt 0 = 0

@[simp]

theorem NNReal.sqrt_one : NNReal.sqrt 1 = 1

@[simp]

theorem NNReal.sqrt_le_one {x : NNReal} : NNReal.sqrt x ≤ 1 ↔ x ≤ 1

@[simp]

theorem NNReal.one_le_sqrt {x : NNReal} : 1 ≤ NNReal.sqrt x ↔ 1 ≤ x

theorem NNReal.sqrt_mul (x : NNReal) (y : NNReal) : NNReal.sqrt (x * y) = NNReal.sqrt x * NNReal.sqrt y

noncomputable def NNReal.sqrtHom : NNReal →*₀ NNReal

NNReal.sqrt as a MonoidWithZeroHom.

Equations

• NNReal.sqrtHom = { toZeroHom := { toFun := ⇑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 : NNReal) (y : NNReal) : NNReal.sqrt (x / y) = NNReal.sqrt x / NNReal.sqrt y

theorem NNReal.continuous_sqrt : Continuous ⇑NNReal.sqrt

@[simp]

theorem NNReal.sqrt_pos {x : NNReal} : 0 < NNReal.sqrt x ↔ 0 < x

theorem NNReal.sqrt_pos_of_pos {x : NNReal} : 0 < x → 0 < NNReal.sqrt x

Alias of the reverse direction of NNReal.sqrt_pos.

def Real.sqrtAux (f : CauSeq ℚ abs) : ℕ → ℚ

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

Equations

• Real.sqrtAux f 0 = mkRat (↑(Nat.sqrt (Int.toNat (↑f 0).num))) (Nat.sqrt (↑f 0).den)
• Real.sqrtAux f (Nat.succ n) = let s := Real.sqrtAux f n; max 0 ((s + ↑f (n + 1) / s) / 2)

theorem Real.sqrtAux_nonneg (f : CauSeq ℚ abs) (i : ℕ) : 0 ≤ Real.sqrtAux 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 (Real.toNNReal x))

@[simp]

theorem Real.coe_sqrt {x : NNReal} : ↑(NNReal.sqrt x) = Real.sqrt ↑x

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

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

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

theorem Real.sqrt_pos_of_pos {x : ℝ} : 0 < x → 0 < Real.sqrt x

Alias of the reverse direction of Real.sqrt_pos.

theorem Real.sqrt_le_sqrt_iff' {x : ℝ} {y : ℝ} (hx : 0 < x) : Real.sqrt x ≤ Real.sqrt y ↔ x ≤ y

@[simp]

theorem Real.one_le_sqrt {x : ℝ} : 1 ≤ Real.sqrt x ↔ 1 ≤ x

@[simp]

theorem Real.sqrt_le_one {x : ℝ} : Real.sqrt x ≤ 1 ↔ x ≤ 1

def Mathlib.Meta.Positivity.evalNNRealSqrt : Mathlib.Meta.Positivity.PositivityExt

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

def Mathlib.Meta.Positivity.evalSqrt : Mathlib.Meta.Positivity.PositivityExt

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 : ℝ) : 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.sqrt_div' (x : ℝ) {y : ℝ} (hy : 0 ≤ 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.lt_sq_of_sqrt_lt {x : ℝ} {y : ℝ} (h : Real.sqrt x < y) : x < y ^ 2

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

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

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

instance Real.instStarOrderedRingRealToNonUnitalSemiringToNonUnitalCommSemiringToNonUnitalCommRingCommRingPartialOrder : StarOrderedRing ℝ

Although the instance RCLike.toStarOrderedRing exists, it is locked behind the ComplexOrder scope because currently the order on ℂ is not enabled globally. But we want StarOrderedRing ℝ to be available globally, so we include this instance separately. In addition, providing this instance here makes it available earlier in the import hierarchy; otherwise in order to access it we would need to import Analysis.RCLike.Basic

Equations

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

instance NNReal.instStarOrderedRing : StarOrderedRing NNReal

Equations

• NNReal.instStarOrderedRing = StarOrderedRing.ofLEIff NNReal.instStarOrderedRing.proof_1

theorem Filter.Tendsto.sqrt {α : Type u_1} {f : α → ℝ} {l : Filter α} {x : ℝ} (h : Filter.Tendsto f l (nhds x)) : Filter.Tendsto (fun (x : α) => Real.sqrt (f x)) l (nhds (Real.sqrt x))

theorem ContinuousWithinAt.sqrt {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} {s : Set α} {x : α} (h : ContinuousWithinAt f s x) : ContinuousWithinAt (fun (x : α) => Real.sqrt (f x)) s x

theorem ContinuousAt.sqrt {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} {x : α} (h : ContinuousAt f x) : ContinuousAt (fun (x : α) => Real.sqrt (f x)) x

theorem ContinuousOn.sqrt {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} {s : Set α} (h : ContinuousOn f s) : ContinuousOn (fun (x : α) => Real.sqrt (f x)) s

theorem Continuous.sqrt {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} (h : Continuous f) : Continuous fun (x : α) => Real.sqrt (f x)

theorem NNReal.sum_mul_le_sqrt_mul_sqrt {ι : Type u_2} (s : Finset ι) (f : ι → NNReal) (g : ι → NNReal) : (Finset.sum s fun (i : ι) => f i * g i) ≤ NNReal.sqrt (Finset.sum s fun (i : ι) => f i ^ 2) * NNReal.sqrt (Finset.sum s fun (i : ι) => g i ^ 2)

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

theorem NNReal.sum_sqrt_mul_sqrt_le {ι : Type u_2} (s : Finset ι) (f : ι → NNReal) (g : ι → NNReal) : (Finset.sum s fun (i : ι) => NNReal.sqrt (f i) * NNReal.sqrt (g i)) ≤ NNReal.sqrt (Finset.sum s fun (i : ι) => f i) * NNReal.sqrt (Finset.sum s fun (i : ι) => g i)

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

theorem Real.sum_mul_le_sqrt_mul_sqrt {ι : Type u_2} (s : Finset ι) (f : ι → ℝ) (g : ι → ℝ) : (Finset.sum s fun (i : ι) => f i * g i) ≤ Real.sqrt (Finset.sum s fun (i : ι) => f i ^ 2) * Real.sqrt (Finset.sum s fun (i : ι) => g i ^ 2)

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

theorem Real.sum_sqrt_mul_sqrt_le {ι : Type u_2} {f : ι → ℝ} {g : ι → ℝ} (s : Finset ι) (hf : ∀ (i : ι), 0 ≤ f i) (hg : ∀ (i : ι), 0 ≤ g i) : (Finset.sum s fun (i : ι) => Real.sqrt (f i) * Real.sqrt (g i)) ≤ Real.sqrt (Finset.sum s fun (i : ι) => f i) * Real.sqrt (Finset.sum s fun (i : ι) => g i)

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