Documentation

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

noncomputable def NNReal.sqrt :

Square root of a nonnegative real number.

Equations
Instances For
    @[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.sqrt as a MonoidWithZeroHom.

    Equations
    Instances For
      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
      @[simp]
      theorem NNReal.sqrt_pos {x : NNReal} :
      0 < NNReal.sqrt x 0 < x
      theorem NNReal.sqrt_pos_of_pos {x : NNReal} :
      0 < x0 < NNReal.sqrt x

      Alias of the reverse direction of NNReal.sqrt_pos.

      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

        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
        Instances For
          @[simp]
          theorem Real.coe_sqrt {x : NNReal} :
          (NNReal.sqrt x) = x
          theorem Real.sqrt_eq_zero_of_nonpos {x : } (h : x 0) :
          x = 0
          @[simp]
          theorem Real.sqrt_nonneg (x : ) :
          0 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 x = y * y
          @[deprecated Real.sqrt_eq_iff_mul_self_eq]
          theorem Real.sqrt_eq_iff_eq_mul_self {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_eq_sq {x : } {y : } (hx : 0 x) (hy : 0 y) :
          x = y x = y ^ 2
          @[deprecated Real.sqrt_eq_iff_eq_sq]
          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) :
          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

          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'

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

          Alias of the reverse direction of Real.sqrt_pos.

          theorem Real.sqrt_le_sqrt_iff' {x : } {y : } (hx : 0 < x) :
          x y x y
          @[simp]
          theorem Real.one_le_sqrt {x : } :
          1 x 1 x
          @[simp]
          theorem Real.sqrt_le_one {x : } :
          x 1 x 1

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

          Instances For

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

            Instances For
              @[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 : ) :
              @[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.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 : } :
              a.sqrt a

              The natural square root is at most the real square root

              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

              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

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

              @[simp]

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

              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.

              theorem Filter.Tendsto.sqrt {α : Type u_1} {f : α} {l : Filter α} {x : } (h : Filter.Tendsto f l (nhds x)) :
              Filter.Tendsto (fun (x : α) => (f x)) l (nhds x)
              theorem ContinuousWithinAt.sqrt {α : Type u_1} [TopologicalSpace α] {f : α} {s : Set α} {x : α} (h : ContinuousWithinAt f s x) :
              ContinuousWithinAt (fun (x : α) => (f x)) s x
              theorem ContinuousAt.sqrt {α : Type u_1} [TopologicalSpace α] {f : α} {x : α} (h : ContinuousAt f x) :
              ContinuousAt (fun (x : α) => (f x)) x
              theorem ContinuousOn.sqrt {α : Type u_1} [TopologicalSpace α] {f : α} {s : Set α} (h : ContinuousOn f s) :
              ContinuousOn (fun (x : α) => (f x)) s
              theorem Continuous.sqrt {α : Type u_1} [TopologicalSpace α] {f : α} (h : Continuous f) :
              Continuous fun (x : α) => (f x)
              theorem NNReal.sum_mul_le_sqrt_mul_sqrt {ι : Type u_2} (s : Finset ι) (f : ιNNReal) (g : ιNNReal) :
              is, f i * g i NNReal.sqrt (∑ is, f i ^ 2) * NNReal.sqrt (∑ is, 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) :
              is, NNReal.sqrt (f i) * NNReal.sqrt (g i) NNReal.sqrt (∑ is, f i) * NNReal.sqrt (∑ is, 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 : ι) :
              is, f i * g i (∑ is, f i ^ 2) * (∑ is, 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) :
              is, (f i) * (g i) (∑ is, f i) * (∑ is, g i)

              Cauchy-Schwarz inequality for finsets using square roots in .