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

      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.

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

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

              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.

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