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
      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
          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 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_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 : } :
              (Nat.sqrt a) a

              The natural square root is at most the real square root

              theorem Real.real_sqrt_le_nat_sqrt_succ {a : } :
              a (Nat.sqrt a) + 1

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

              theorem Real.real_sqrt_lt_nat_sqrt_succ {a : } :
              a < (Nat.sqrt a) + 1

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

              @[simp]

              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.

              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.
              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) :
              (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) (Finset.sum s fun (i : ι) => f i ^ 2) * (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 : ι) => (f i) * (g i)) (Finset.sum s fun (i : ι) => f i) * (Finset.sum s fun (i : ι) => g i)

              Cauchy-Schwarz inequality for finsets using square roots in .