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

Square root of a nonnegative real number.

Equations
Instances For
    theorem NNReal.sqrt_le_iff {x : NNReal} {y : NNReal} :
    NNReal.sqrt x y x y ^ 2
    theorem NNReal.le_sqrt_iff {x : NNReal} {y : NNReal} :
    x NNReal.sqrt y x ^ 2 y
    @[simp]
    theorem NNReal.sqrt_eq_zero {x : NNReal} :
    NNReal.sqrt x = 0 x = 0
    @[simp]
    @[simp]
    @[simp]
    theorem NNReal.sq_sqrt (x : NNReal) :
    @[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
    noncomputable def NNReal.sqrtHom :

    NNReal.sqrt as a MonoidWithZeroHom.

    Equations
    Instances For
      @[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.

      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
      Instances For
        theorem Real.sqrtAux_nonneg (f : CauSeq abs) (i : ) :
        noncomputable def Real.sqrt (x : ) :

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

        Equations
        Instances For
          @[simp]
          theorem Real.coe_sqrt {x : NNReal} :
          (NNReal.sqrt x) = Real.sqrt x
          theorem Real.sqrt_eq_zero_of_nonpos {x : } (h : x 0) :
          @[simp]
          theorem Real.mul_self_sqrt {x : } (h : 0 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_sq_eq_abs (x : ) :
          Real.sqrt (x ^ 2) = |x|
          @[simp]
          @[simp]
          @[simp]
          theorem Real.sqrt_le_sqrt_iff {x : } {y : } (hy : 0 y) :
          @[simp]
          theorem Real.sqrt_lt_sqrt_iff {x : } {y : } (hx : 0 x) :
          theorem Real.sqrt_lt_sqrt_iff_of_pos {x : } {y : } (hy : 0 < 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) :
          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) :
          theorem Real.sq_le {x : } {y : } (h : 0 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) :
          @[simp]
          theorem Real.sqrt_eq_zero {x : } (h : 0 x) :
          Real.sqrt x = 0 x = 0
          theorem Real.sqrt_ne_zero {x : } (h : 0 x) :
          @[simp]
          theorem Real.sqrt_pos {x : } :
          0 < Real.sqrt x 0 < x
          theorem Real.sqrt_pos_of_pos {x : } :
          0 < x0 < Real.sqrt x

          Alias of the reverse direction of Real.sqrt_pos.

          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

            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
              @[simp]
              theorem Real.sqrt_mul {x : } (hx : 0 x) (y : ) :
              @[simp]
              theorem Real.sqrt_mul' (x : ) {y : } (hy : 0 y) :
              @[simp]
              theorem Real.sqrt_div {x : } (hx : 0 x) (y : ) :
              @[simp]
              theorem Real.sqrt_div' (x : ) {y : } (hy : 0 y) :
              @[simp]
              theorem Real.div_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) :
              theorem Real.lt_sqrt_of_sq_lt {x : } {y : } (h : x ^ 2 < y) :
              theorem Real.lt_sq_of_sqrt_lt {x : } {y : } (h : Real.sqrt x < y) :
              x < y ^ 2

              The natural square root is at most the real square root

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

              Although the instance IsROrC.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 Data.IsROrC.Basic

              Equations
              • One or more equations did not get rendered due to their size.
              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)