Mathlib.Data.Real.Sqrt

NNReal.sqrt definition

: ℝ≥0 ≃o ℝ≥0

Full source

/-- Square root of a nonnegative real number. -/
-- Porting note (kmill): `pp_nodot` has no effect here
-- unless RFC https://github.com/leanprover/lean4/issues/6178 leads to dot notation pp for CoeFun
@[pp_nodot]
noncomputable def sqrt : ℝ≥0ℝ≥0 ≃o ℝ≥0 :=
  OrderIso.symm <| powOrderIso 2 two_ne_zero

Square root on nonnegative reals

Informal description

The square root function on nonnegative real numbers, defined as the inverse of the order isomorphism $ x \mapsto x^2 $. This function is a strictly increasing bijection from $\mathbb{R}_{\geq 0}$ to itself, preserving the order structure.

NNReal.sq_sqrt theorem

(x : ℝ≥0) : sqrt x ^ 2 = x

Full source

@[simp] lemma sq_sqrt (x : ℝ≥0) : sqrt x ^ 2 = x := sqrt.symm_apply_apply _

Square of Square Root Recovers Original Nonnegative Real: $(\sqrt{x})^2 = x$

Informal description

For any nonnegative real number $x \in \mathbb{R}_{\geq 0}$, the square of its square root equals $x$, i.e., $(\sqrt{x})^2 = x$.

NNReal.sqrt_sq theorem

(x : ℝ≥0) : sqrt (x ^ 2) = x

Full source

@[simp] lemma sqrt_sq (x : ℝ≥0) : sqrt (x ^ 2) = x := sqrt.apply_symm_apply _

Square Root of Square Identity: $\sqrt{x^2} = x$ for $x \geq 0$

Informal description

For any nonnegative real number $x \in \mathbb{R}_{\geq 0}$, the square root of $x^2$ equals $x$, i.e., $\sqrt{x^2} = x$.

NNReal.mul_self_sqrt theorem

(x : ℝ≥0) : sqrt x * sqrt x = x

Full source

@[simp] lemma mul_self_sqrt (x : ℝ≥0) : sqrt x * sqrt x = x := by rw [← sq, sq_sqrt]

Square Root Identity: $\sqrt{x} \cdot \sqrt{x} = x$ for $x \geq 0$

Informal description

For any nonnegative real number $x \in \mathbb{R}_{\geq 0}$, the product of its square root with itself equals $x$, i.e., $\sqrt{x} \cdot \sqrt{x} = x$.

NNReal.sqrt_mul_self theorem

(x : ℝ≥0) : sqrt (x * x) = x

Full source

@[simp] lemma sqrt_mul_self (x : ℝ≥0) : sqrt (x * x) = x := by rw [← sq, sqrt_sq]

Square Root of Squared Nonnegative Real Number: $\sqrt{x \cdot x} = x$

Informal description

For any nonnegative real number $x \in \mathbb{R}_{\geq 0}$, the square root of $x \cdot x$ equals $x$, i.e., $\sqrt{x \cdot x} = x$.

NNReal.sqrt_le_sqrt theorem

: sqrt x ≤ sqrt y ↔ x ≤ y

Full source

lemma sqrt_le_sqrt : sqrtsqrt x ≤ sqrt y ↔ x ≤ y := sqrt.le_iff_le

Square Root Preserves Order on Nonnegative Reals ($\sqrt{x} \leq \sqrt{y} \leftrightarrow x \leq y$)

Informal description

For any nonnegative real numbers $x$ and $y$, the inequality $\sqrt{x} \leq \sqrt{y}$ holds if and only if $x \leq y$.

NNReal.sqrt_lt_sqrt theorem

: sqrt x < sqrt y ↔ x < y

Full source

lemma sqrt_lt_sqrt : sqrtsqrt x < sqrt y ↔ x < y := sqrt.lt_iff_lt

Square Root Preserves Strict Order on Nonnegative Reals ($\sqrt{x} < \sqrt{y} \leftrightarrow x < y$)

Informal description

For any nonnegative real numbers $x$ and $y$, the square root of $x$ is less than the square root of $y$ if and only if $x$ is less than $y$.

NNReal.sqrt_eq_iff_eq_sq theorem

: sqrt x = y ↔ x = y ^ 2

Full source

lemma sqrt_eq_iff_eq_sq : sqrtsqrt x = y ↔ x = y ^ 2 := sqrt.toEquiv.apply_eq_iff_eq_symm_apply

Square Root Equality: $\sqrt{x} = y \leftrightarrow x = y^2$

Informal description

For any nonnegative real numbers $x$ and $y$, the square root of $x$ equals $y$ if and only if $x$ equals $y^2$. In other words, $\sqrt{x} = y \leftrightarrow x = y^2$.

NNReal.sqrt_le_iff_le_sq theorem

: sqrt x ≤ y ↔ x ≤ y ^ 2

Full source

lemma sqrt_le_iff_le_sq : sqrtsqrt x ≤ y ↔ x ≤ y ^ 2 := sqrt.to_galoisConnection _ _

Square Root Inequality: $\sqrt{x} \leq y \leftrightarrow x \leq y^2$

Informal description

For any nonnegative real numbers $x$ and $y$, the square root of $x$ is less than or equal to $y$ if and only if $x$ is less than or equal to $y^2$. In other words, $\sqrt{x} \leq y \leftrightarrow x \leq y^2$.

NNReal.le_sqrt_iff_sq_le theorem

: x ≤ sqrt y ↔ x ^ 2 ≤ y

Full source

lemma le_sqrt_iff_sq_le : x ≤ sqrt y ↔ x ^ 2 ≤ y := (sqrt.symm.to_galoisConnection _ _).symm

Square Root Inequality: $x \leq \sqrt{y} \leftrightarrow x^2 \leq y$

Informal description

For any nonnegative real numbers $x$ and $y$, the inequality $x \leq \sqrt{y}$ holds if and only if $x^2 \leq y$.

NNReal.sqrt_eq_zero theorem

: sqrt x = 0 ↔ x = 0

Full source

@[simp] lemma sqrt_eq_zero : sqrtsqrt x = 0 ↔ x = 0 := by simp [sqrt_eq_iff_eq_sq]

Square Root Vanishes if and only if Argument is Zero

Informal description

For any nonnegative real number $x$, the square root of $x$ is equal to zero if and only if $x$ itself is equal to zero, i.e., $\sqrt{x} = 0 \leftrightarrow x = 0$.

NNReal.sqrt_eq_one theorem

: sqrt x = 1 ↔ x = 1

Full source

@[simp] lemma sqrt_eq_one : sqrtsqrt x = 1 ↔ x = 1 := by simp [sqrt_eq_iff_eq_sq]

Square Root Equals One iff Argument Equals One

Informal description

For any nonnegative real number $x$, the square root of $x$ equals $1$ if and only if $x$ equals $1$, i.e., $\sqrt{x} = 1 \leftrightarrow x = 1$.

NNReal.sqrt_zero theorem

: sqrt 0 = 0

Full source

@[simp] lemma sqrt_zero : sqrt 0 = 0 := by simp

Square Root of Zero is Zero

Informal description

The square root of zero is zero, i.e., $\sqrt{0} = 0$.

NNReal.sqrt_one theorem

: sqrt 1 = 1

Full source

@[simp] lemma sqrt_one : sqrt 1 = 1 := by simp

Square Root of One Equals One

Informal description

The square root of the nonnegative real number $1$ is equal to $1$, i.e., $\sqrt{1} = 1$.

NNReal.sqrt_le_one theorem

: sqrt x ≤ 1 ↔ x ≤ 1

Full source

@[simp] lemma sqrt_le_one : sqrtsqrt x ≤ 1 ↔ x ≤ 1 := by rw [← sqrt_one, sqrt_le_sqrt, sqrt_one]

Square Root Inequality: $\sqrt{x} \leq 1 \leftrightarrow x \leq 1$

Informal description

For any nonnegative real number $x$, the inequality $\sqrt{x} \leq 1$ holds if and only if $x \leq 1$.

NNReal.one_le_sqrt theorem

: 1 ≤ sqrt x ↔ 1 ≤ x

Full source

@[simp] lemma one_le_sqrt : 1 ≤ sqrt x ↔ 1 ≤ x := by rw [← sqrt_one, sqrt_le_sqrt, sqrt_one]

Square Root Order Comparison: $1 \leq \sqrt{x} \leftrightarrow 1 \leq x$

Informal description

For any nonnegative real number $x$, the inequality $1 \leq \sqrt{x}$ holds if and only if $1 \leq x$.

NNReal.sqrt_mul theorem

(x y : ℝ≥0) : sqrt (x * y) = sqrt x * sqrt y

Full source

theorem sqrt_mul (x y : ℝ≥0) : sqrt (x * y) = sqrt x * sqrt y := by
  rw [sqrt_eq_iff_eq_sq, mul_pow, sq_sqrt, sq_sqrt]

Square Root of Product Equals Product of Square Roots: $\sqrt{xy} = \sqrt{x}\sqrt{y}$

Informal description

For any nonnegative real numbers $x$ and $y$, the square root of their product equals the product of their square roots, i.e., $\sqrt{x \cdot y} = \sqrt{x} \cdot \sqrt{y}$.

NNReal.sqrtHom definition

: ℝ≥0 →*₀ ℝ≥0

Full source

/-- `NNReal.sqrt` as a `MonoidWithZeroHom`. -/
noncomputable def sqrtHom : ℝ≥0ℝ≥0 →*₀ ℝ≥0 :=
  ⟨⟨sqrt, sqrt_zero⟩, sqrt_one, sqrt_mul⟩

Square root as a monoid homomorphism with zero

Informal description

The square root function on nonnegative real numbers, viewed as a monoid homomorphism with zero, i.e., a map that preserves multiplication, the multiplicative identity, and maps zero to zero. Specifically, it satisfies: 1. $\sqrt{0} = 0$, 2. $\sqrt{1} = 1$, 3. $\sqrt{x \cdot y} = \sqrt{x} \cdot \sqrt{y}$ for all $x, y \in \mathbb{R}_{\geq 0}$.

NNReal.sqrt_inv theorem

(x : ℝ≥0) : sqrt x⁻¹ = (sqrt x)⁻¹

Full source

theorem sqrt_inv (x : ℝ≥0) : sqrt x⁻¹ = (sqrt x)⁻¹ :=
  map_inv₀ sqrtHom x

Square Root of Inverse Equals Inverse of Square Root: $\sqrt{x^{-1}} = (\sqrt{x})^{-1}$

Informal description

For any nonnegative real number $x$, the square root of its multiplicative inverse equals the multiplicative inverse of its square root, i.e., $\sqrt{x^{-1}} = (\sqrt{x})^{-1}$.

NNReal.sqrt_div theorem

(x y : ℝ≥0) : sqrt (x / y) = sqrt x / sqrt y

Full source

theorem sqrt_div (x y : ℝ≥0) : sqrt (x / y) = sqrt x / sqrt y :=
  map_div₀ sqrtHom x y

Square Root of Quotient Equals Quotient of Square Roots on Nonnegative Reals

Informal description

For any nonnegative real numbers $x$ and $y$, the square root of the quotient $x / y$ is equal to the quotient of the square roots $\sqrt{x} / \sqrt{y}$.

NNReal.continuous_sqrt theorem

: Continuous sqrt

Full source

@[continuity, fun_prop]
theorem continuous_sqrt : Continuous sqrt := sqrt.continuous

Continuity of the Square Root Function on Nonnegative Reals

Informal description

The square root function $\sqrt{\cdot} : \mathbb{R}_{\geq 0} \to \mathbb{R}_{\geq 0}$ is continuous.

NNReal.sqrt_pos theorem

: 0 < sqrt x ↔ 0 < x

Full source

@[simp] theorem sqrt_pos : 0 < sqrt x ↔ 0 < x := by simp [pos_iff_ne_zero]

Positivity of Square Root on Nonnegative Reals: $\sqrt{x} > 0 \leftrightarrow x > 0$

Informal description

For any nonnegative real number $x$, the square root of $x$ is positive if and only if $x$ itself is positive, i.e., $\sqrt{x} > 0 \leftrightarrow x > 0$.

Real.sqrt definition

(x : ℝ) : ℝ

Full source

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

This has notation `√x`. Note that `√x⁻¹` is parsed as `√(x⁻¹)`. -/
noncomputable def sqrt (x : ℝ) : ℝ :=
  NNReal.sqrt (Real.toNNReal x)

Square root of a real number

Informal description

The square root function on real numbers, defined as $\sqrt{x} = \text{NNReal.sqrt}(\text{Real.toNNReal}(x))$, where $\text{Real.toNNReal}(x)$ maps $x$ to its nonnegative part (i.e., $x$ if $x \geq 0$ and $0$ otherwise). For negative inputs, the function returns $0$. This function is denoted by the notation $\sqrt{x}$.

Real.term√_ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc]
prefix:max "√" => Real.sqrt

Square root notation for real numbers

Informal description

The notation `√x` is defined as a prefix operator for the real square root function `Real.sqrt x`, which computes the square root of a real number $x$ (defined to be zero when $x$ is negative).

Real.coe_sqrt theorem

{x : ℝ≥0} : (NNReal.sqrt x : ℝ) = √(x : ℝ)

Full source

@[simp, norm_cast]
theorem coe_sqrt {x : ℝ≥0} : (NNReal.sqrt x : ℝ) = √(x : ℝ) := by
  rw [Real.sqrt, Real.toNNReal_coe]

Coercion of Nonnegative Square Root to Real Square Root

Informal description

For any nonnegative real number $x \in \mathbb{R}_{\geq 0}$, the real-valued square root of $x$ obtained by coercing the nonnegative square root function equals the real square root function applied to $x$, i.e., $\text{NNReal.sqrt}(x) = \sqrt{x}$.

Real.continuous_sqrt theorem

: Continuous (√· : ℝ → ℝ)

Full source

@[continuity]
theorem continuous_sqrt : Continuous (√· : ℝ → ℝ) :=
  NNReal.continuous_coe.comp <| NNReal.continuous_sqrt.comp continuous_real_toNNReal

Continuity of the Real Square Root Function

Informal description

The square root function $\sqrt{\cdot} : \mathbb{R} \to \mathbb{R}$ is continuous.

Real.sqrt_eq_zero_of_nonpos theorem

(h : x ≤ 0) : sqrt x = 0

Full source

theorem sqrt_eq_zero_of_nonpos (h : x ≤ 0) : sqrt x = 0 := by simp [sqrt, Real.toNNReal_eq_zero.2 h]

Square Root Vanishes on Nonpositive Reals

Informal description

For any real number $x \leq 0$, the square root of $x$ is equal to $0$, i.e., $\sqrt{x} = 0$.

Real.sqrt_nonneg theorem

(x : ℝ) : 0 ≤ √x

Full source

@[simp] theorem sqrt_nonneg (x : ℝ) : 0 ≤ √x := NNReal.coe_nonneg _

Nonnegativity of the Real Square Root

Informal description

For any real number $x$, the square root $\sqrt{x}$ is nonnegative, i.e., $0 \leq \sqrt{x}$.

Real.mul_self_sqrt theorem

(h : 0 ≤ x) : √x * √x = x

Full source

@[simp]
theorem mul_self_sqrt (h : 0 ≤ x) : √x * √x = x := by
  rw [Real.sqrt, ← NNReal.coe_mul, NNReal.mul_self_sqrt, Real.coe_toNNReal _ h]

Square Root Identity: $\sqrt{x} \cdot \sqrt{x} = x$ for $x \geq 0$

Informal description

For any real number $x \geq 0$, the product of its square root with itself equals $x$, i.e., $\sqrt{x} \cdot \sqrt{x} = x$.

Real.sqrt_mul_self theorem

(h : 0 ≤ x) : √(x * x) = x

Full source

@[simp]
theorem sqrt_mul_self (h : 0 ≤ x) : √(x * x) = x :=
  (mul_self_inj_of_nonneg (sqrt_nonneg _) h).1 (mul_self_sqrt (mul_self_nonneg _))

Square Root of Squared Nonnegative Real Number: $\sqrt{x^2} = x$ for $x \geq 0$

Informal description

For any real number $x \geq 0$, the square root of $x^2$ equals $x$, i.e., $\sqrt{x^2} = x$.

Real.sqrt_eq_cases theorem

: √x = y ↔ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0

Full source

theorem sqrt_eq_cases : √x√x = y ↔ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0 := by
  constructor
  · rintro rfl
    rcases le_or_lt 0 x with hle | hlt
    · exact Or.inl ⟨mul_self_sqrt hle, sqrt_nonneg x⟩
    · exact Or.inr ⟨hlt, sqrt_eq_zero_of_nonpos hlt.le⟩
  · rintro (⟨rfl, hy⟩ | ⟨hx, rfl⟩)
    exacts [sqrt_mul_self hy, sqrt_eq_zero_of_nonpos hx.le]

Characterization of Real Square Root: $\sqrt{x} = y \leftrightarrow (y^2 = x \land y \geq 0) \lor (x < 0 \land y = 0)$

Informal description

For any real numbers $x$ and $y$, the equality $\sqrt{x} = y$ holds if and only if either: 1. $y^2 = x$ and $y \geq 0$, or 2. $x < 0$ and $y = 0$.

Real.sqrt_eq_iff_mul_self_eq theorem

(hx : 0 ≤ x) (hy : 0 ≤ y) : √x = y ↔ x = y * y

Full source

theorem sqrt_eq_iff_mul_self_eq (hx : 0 ≤ x) (hy : 0 ≤ y) : √x√x = y ↔ x = y * y :=
  ⟨fun h => by rw [← h, mul_self_sqrt hx], fun h => by rw [h, sqrt_mul_self hy]⟩

Square Root Equality for Nonnegative Reals: $\sqrt{x} = y \leftrightarrow x = y^2$

Informal description

For any nonnegative real numbers $x$ and $y$, the square root of $x$ equals $y$ if and only if $x$ equals $y^2$, i.e., $\sqrt{x} = y \leftrightarrow x = y^2$.

Real.sqrt_eq_iff_mul_self_eq_of_pos theorem

(h : 0 < y) : √x = y ↔ y * y = x

Full source

theorem sqrt_eq_iff_mul_self_eq_of_pos (h : 0 < y) : √x√x = y ↔ y * y = x := by
  simp [sqrt_eq_cases, h.ne', h.le]

Square Root Equality for Positive $y$: $\sqrt{x} = y \leftrightarrow y^2 = x$

Informal description

For any real numbers $x$ and $y$ with $y > 0$, the equality $\sqrt{x} = y$ holds if and only if $y^2 = x$.

Real.sqrt_eq_one theorem

: √x = 1 ↔ x = 1

Full source

@[simp]
theorem sqrt_eq_one : √x√x = 1 ↔ x = 1 :=
  calc
    √x = 1 ↔ 1 * 1 = x := sqrt_eq_iff_mul_self_eq_of_pos zero_lt_one
    _ ↔ x = 1 := by rw [eq_comm, mul_one]

Square Root of One Equivalence: $\sqrt{x} = 1 \leftrightarrow x = 1$

Informal description

For any real number $x$, the square root of $x$ equals $1$ if and only if $x$ equals $1$, i.e., $\sqrt{x} = 1 \leftrightarrow x = 1$.

Real.sq_sqrt theorem

(h : 0 ≤ x) : √x ^ 2 = x

Full source

@[simp]
theorem sq_sqrt (h : 0 ≤ x) : √x ^ 2 = x := by rw [sq, mul_self_sqrt h]

Square of Square Root Identity: $(\sqrt{x})^2 = x$ for $x \geq 0$

Informal description

For any real number $x \geq 0$, the square of its square root equals $x$, i.e., $(\sqrt{x})^2 = x$.

Real.sqrt_sq theorem

(h : 0 ≤ x) : √(x ^ 2) = x

Full source

@[simp]
theorem sqrt_sq (h : 0 ≤ x) : √(x ^ 2) = x := by rw [sq, sqrt_mul_self h]

Square Root of Squared Nonnegative Real Number: $\sqrt{x^2} = x$ for $x \geq 0$

Informal description

For any real number $x \geq 0$, the square root of $x^2$ equals $x$, i.e., $\sqrt{x^2} = x$.

Real.sqrt_eq_iff_eq_sq theorem

(hx : 0 ≤ x) (hy : 0 ≤ y) : √x = y ↔ x = y ^ 2

Full source

theorem sqrt_eq_iff_eq_sq (hx : 0 ≤ x) (hy : 0 ≤ y) : √x√x = y ↔ x = y ^ 2 := by
  rw [sq, sqrt_eq_iff_mul_self_eq hx hy]

Square Root Characterization: $\sqrt{x} = y \leftrightarrow x = y^2$ for $x, y \geq 0$

Informal description

For any nonnegative real numbers $x$ and $y$, the square root of $x$ equals $y$ if and only if $x$ equals $y^2$, i.e., $\sqrt{x} = y \leftrightarrow x = y^2$.

Real.sqrt_mul_self_eq_abs theorem

(x : ℝ) : √(x * x) = |x|

Full source

theorem sqrt_mul_self_eq_abs (x : ℝ) : √(x * x) = |x| := by
  rw [← abs_mul_abs_self x, sqrt_mul_self (abs_nonneg _)]

Square Root of Squared Real Number Equals Absolute Value: $\sqrt{x^2} = |x|$

Informal description

For any real number $x$, the square root of $x^2$ equals the absolute value of $x$, i.e., $\sqrt{x^2} = |x|$.

Real.sqrt_sq_eq_abs theorem

(x : ℝ) : √(x ^ 2) = |x|

Full source

theorem sqrt_sq_eq_abs (x : ℝ) : √(x ^ 2) = |x| := by rw [sq, sqrt_mul_self_eq_abs]

Square Root of Squared Real Number Equals Absolute Value: $\sqrt{x^2} = |x|$

Informal description

For any real number $x$, the square root of $x^2$ equals the absolute value of $x$, i.e., $\sqrt{x^2} = |x|$.

Real.sqrt_zero theorem

: √0 = 0

Full source

@[simp]
theorem sqrt_zero : √0 = 0 := by simp [Real.sqrt]

Square Root of Zero Identity: $\sqrt{0} = 0$

Informal description

The square root of zero is zero, i.e., $\sqrt{0} = 0$.

Real.sqrt_one theorem

: √1 = 1

Full source

@[simp]
theorem sqrt_one : √1 = 1 := by simp [Real.sqrt]

Square Root Identity: $\sqrt{1} = 1$

Informal description

The square root of the real number $1$ is equal to $1$, i.e., $\sqrt{1} = 1$.

Real.sqrt_le_sqrt_iff theorem

(hy : 0 ≤ y) : √x ≤ √y ↔ x ≤ y

Full source

@[simp]
theorem sqrt_le_sqrt_iff (hy : 0 ≤ y) : √x√x ≤ √y ↔ x ≤ y := by
  rw [Real.sqrt, Real.sqrt, NNReal.coe_le_coe, NNReal.sqrt_le_sqrt, toNNReal_le_toNNReal_iff hy]

Square Root Preserves Order for Nonnegative Real Numbers ($\sqrt{x} \leq \sqrt{y} \leftrightarrow x \leq y$ when $y \geq 0$)

Informal description

For any real numbers $x$ and $y$ with $y \geq 0$, the inequality $\sqrt{x} \leq \sqrt{y}$ holds if and only if $x \leq y$.

Real.sqrt_lt_sqrt_iff theorem

(hx : 0 ≤ x) : √x < √y ↔ x < y

Full source

@[simp]
theorem sqrt_lt_sqrt_iff (hx : 0 ≤ x) : √x√x < √y ↔ x < y :=
  lt_iff_lt_of_le_iff_le (sqrt_le_sqrt_iff hx)

Square Root Preserves Strict Order for Nonnegative Real Numbers ($\sqrt{x} < \sqrt{y} \leftrightarrow x < y$ when $x \geq 0$)

Informal description

For any real numbers $x$ and $y$ with $x \geq 0$, the inequality $\sqrt{x} < \sqrt{y}$ holds if and only if $x < y$.

Real.sqrt_lt_sqrt_iff_of_pos theorem

(hy : 0 < y) : √x < √y ↔ x < y

Full source

theorem sqrt_lt_sqrt_iff_of_pos (hy : 0 < y) : √x√x < √y ↔ x < y := by
  rw [Real.sqrt, Real.sqrt, NNReal.coe_lt_coe, NNReal.sqrt_lt_sqrt, toNNReal_lt_toNNReal_iff hy]

Square Root Preserves Strict Order for Positive Real Numbers ($\sqrt{x} < \sqrt{y} \leftrightarrow x < y$ when $y > 0$)

Informal description

For any real numbers $x$ and $y$ with $y > 0$, the inequality $\sqrt{x} < \sqrt{y}$ holds if and only if $x < y$.

Real.sqrt_le_sqrt theorem

(h : x ≤ y) : √x ≤ √y

Full source

@[gcongr, bound]
theorem sqrt_le_sqrt (h : x ≤ y) : √x ≤ √y := by
  rw [Real.sqrt, Real.sqrt, NNReal.coe_le_coe, NNReal.sqrt_le_sqrt]
  exact toNNReal_le_toNNReal h

Square Root Preserves Order ($x \leq y \Rightarrow \sqrt{x} \leq \sqrt{y}$)

Informal description

For any real numbers $x$ and $y$, if $x \leq y$, then $\sqrt{x} \leq \sqrt{y}$.

Real.sqrt_lt_sqrt theorem

(hx : 0 ≤ x) (h : x < y) : √x < √y

Full source

@[gcongr, bound]
theorem sqrt_lt_sqrt (hx : 0 ≤ x) (h : x < y) : √x < √y :=
  (sqrt_lt_sqrt_iff hx).2 h

Square Root Preserves Strict Inequality for Nonnegative Reals

Informal description

For any real numbers $x$ and $y$ with $x \geq 0$, if $x < y$, then $\sqrt{x} < \sqrt{y}$.

Real.sqrt_le_left theorem

(hy : 0 ≤ y) : √x ≤ y ↔ x ≤ y ^ 2

Full source

theorem sqrt_le_left (hy : 0 ≤ y) : √x√x ≤ y ↔ x ≤ y ^ 2 := by
  rw [sqrt, ← Real.le_toNNReal_iff_coe_le hy, NNReal.sqrt_le_iff_le_sq, sq, ← Real.toNNReal_mul hy,
    Real.toNNReal_le_toNNReal_iff (mul_self_nonneg y), sq]

Square Root Inequality: $\sqrt{x} \leq y \leftrightarrow x \leq y^2$ for $y \geq 0$

Informal description

For any real numbers $x$ and $y$ with $y \geq 0$, the inequality $\sqrt{x} \leq y$ holds if and only if $x \leq y^2$.

Real.sqrt_le_iff theorem

: √x ≤ y ↔ 0 ≤ y ∧ x ≤ y ^ 2

Full source

theorem sqrt_le_iff : √x√x ≤ y ↔ 0 ≤ y ∧ x ≤ y ^ 2 := by
  rw [← and_iff_right_of_imp fun h => (sqrt_nonneg x).trans h, and_congr_right_iff]
  exact sqrt_le_left

Square Root Inequality: $\sqrt{x} \leq y \leftrightarrow y \geq 0 \land x \leq y^2$

Informal description

For any real numbers $x$ and $y$, the inequality $\sqrt{x} \leq y$ holds if and only if $y$ is nonnegative and $x \leq y^2$.

Real.sqrt_lt theorem

(hx : 0 ≤ x) (hy : 0 ≤ y) : √x < y ↔ x < y ^ 2

Full source

theorem sqrt_lt (hx : 0 ≤ x) (hy : 0 ≤ y) : √x√x < y ↔ x < y ^ 2 := by
  rw [← sqrt_lt_sqrt_iff hx, sqrt_sq hy]

Square Root Strict Inequality: $\sqrt{x} < y \leftrightarrow x < y^2$ for $x, y \geq 0$

Informal description

For any nonnegative real numbers $x$ and $y$ (i.e., $x \geq 0$ and $y \geq 0$), the inequality $\sqrt{x} < y$ holds if and only if $x < y^2$.

Real.sqrt_lt' theorem

(hy : 0 < y) : √x < y ↔ x < y ^ 2

Full source

theorem sqrt_lt' (hy : 0 < y) : √x√x < y ↔ x < y ^ 2 := by
  rw [← sqrt_lt_sqrt_iff_of_pos (pow_pos hy _), sqrt_sq hy.le]

Square Root Inequality for Positive $y$: $\sqrt{x} < y \leftrightarrow x < y^2$ when $y > 0$

Informal description

For any real numbers $x$ and $y$ with $y > 0$, the inequality $\sqrt{x} < y$ holds if and only if $x < y^2$.

Real.le_sqrt theorem

(hx : 0 ≤ x) (hy : 0 ≤ y) : x ≤ √y ↔ x ^ 2 ≤ y

Full source

/-- 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 le_sqrt (hx : 0 ≤ x) (hy : 0 ≤ y) : x ≤ √y ↔ x ^ 2 ≤ y :=
  le_iff_le_iff_lt_iff_lt.2 <| sqrt_lt hy hx

Square Root Inequality: $x \leq \sqrt{y} \leftrightarrow x^2 \leq y$ for $x, y \geq 0$

Informal description

For any nonnegative real numbers $x$ and $y$ (i.e., $x \geq 0$ and $y \geq 0$), the inequality $x \leq \sqrt{y}$ holds if and only if $x^2 \leq y$.

Real.le_sqrt' theorem

(hx : 0 < x) : x ≤ √y ↔ x ^ 2 ≤ y

Full source

theorem le_sqrt' (hx : 0 < x) : x ≤ √y ↔ x ^ 2 ≤ y :=
  le_iff_le_iff_lt_iff_lt.2 <| sqrt_lt' hx

Square Root Inequality for Positive $x$: $x \leq \sqrt{y} \leftrightarrow x^2 \leq y$ when $x > 0$

Informal description

For any positive real number $x$ and any real number $y$, the inequality $x \leq \sqrt{y}$ holds if and only if $x^2 \leq y$.

Real.abs_le_sqrt theorem

(h : x ^ 2 ≤ y) : |x| ≤ √y

Full source

theorem abs_le_sqrt (h : x ^ 2 ≤ y) : |x| ≤ √y := by
  rw [← sqrt_sq_eq_abs]; exact sqrt_le_sqrt h

Absolute Value Bound by Square Root: $x^2 \leq y \Rightarrow |x| \leq \sqrt{y}$

Informal description

For any real numbers $x$ and $y$, if $x^2 \leq y$, then $|x| \leq \sqrt{y}$.

Real.sq_le theorem

(h : 0 ≤ y) : x ^ 2 ≤ y ↔ -√y ≤ x ∧ x ≤ √y

Full source

theorem sq_le (h : 0 ≤ y) : x ^ 2 ≤ y ↔ -√y ≤ x ∧ x ≤ √y := by
  constructor
  · simpa only [abs_le] using abs_le_sqrt
  · rw [← abs_le, ← sq_abs]
    exact (le_sqrt (abs_nonneg x) h).mp

Square Bound Equivalence: $x^2 \leq y \leftrightarrow x \in [-\sqrt{y}, \sqrt{y}]$ for $y \geq 0$

Informal description

For any real numbers $x$ and $y$ with $y \geq 0$, the inequality $x^2 \leq y$ holds if and only if $x$ lies in the closed interval $[-\sqrt{y}, \sqrt{y}]$.

Real.neg_sqrt_le_of_sq_le theorem

(h : x ^ 2 ≤ y) : -√y ≤ x

Full source

theorem neg_sqrt_le_of_sq_le (h : x ^ 2 ≤ y) : -√y ≤ x :=
  ((sq_le ((sq_nonneg x).trans h)).mp h).1

Lower Bound of Square Root: $x^2 \leq y \Rightarrow -\sqrt{y} \leq x$

Informal description

For any real numbers $x$ and $y$, if $x^2 \leq y$, then $x$ is bounded below by $-\sqrt{y}$, i.e., $-\sqrt{y} \leq x$.

Real.le_sqrt_of_sq_le theorem

(h : x ^ 2 ≤ y) : x ≤ √y

Full source

theorem le_sqrt_of_sq_le (h : x ^ 2 ≤ y) : x ≤ √y :=
  ((sq_le ((sq_nonneg x).trans h)).mp h).2

Inequality from Square Bound: $x^2 \leq y \Rightarrow x \leq \sqrt{y}$

Informal description

For any real numbers $x$ and $y$, if $x^2 \leq y$, then $x \leq \sqrt{y}$.

Real.sqrt_inj theorem

(hx : 0 ≤ x) (hy : 0 ≤ y) : √x = √y ↔ x = y

Full source

@[simp]
theorem sqrt_inj (hx : 0 ≤ x) (hy : 0 ≤ y) : √x√x = √y ↔ x = y := by
  simp [le_antisymm_iff, hx, hy]

Injectivity of Square Root on Nonnegative Reals

Informal description

For any nonnegative real numbers $x$ and $y$, the square roots $\sqrt{x}$ and $\sqrt{y}$ are equal if and only if $x = y$.

Real.sqrt_eq_zero theorem

(h : 0 ≤ x) : √x = 0 ↔ x = 0

Full source

@[simp]
theorem sqrt_eq_zero (h : 0 ≤ x) : √x√x = 0 ↔ x = 0 := by simpa using sqrt_inj h le_rfl

Square Root Vanishes if and only if Argument is Zero on Nonnegative Reals

Informal description

For any nonnegative real number $x$, the square root of $x$ is zero if and only if $x$ is zero, i.e., $\sqrt{x} = 0 \leftrightarrow x = 0$.

Real.sqrt_eq_zero' theorem

: √x = 0 ↔ x ≤ 0

Full source

theorem sqrt_eq_zero' : √x√x = 0 ↔ x ≤ 0 := by
  rw [sqrt, NNReal.coe_eq_zero, NNReal.sqrt_eq_zero, Real.toNNReal_eq_zero]

Square Root Vanishes if and only if Argument is Nonpositive

Informal description

For any real number $x$, the square root of $x$ equals zero if and only if $x$ is less than or equal to zero, i.e., $\sqrt{x} = 0 \leftrightarrow x \leq 0$.

Real.sqrt_ne_zero theorem

(h : 0 ≤ x) : √x ≠ 0 ↔ x ≠ 0

Full source

theorem sqrt_ne_zero (h : 0 ≤ x) : √x√x ≠ 0√x ≠ 0 ↔ x ≠ 0 := by rw [not_iff_not, sqrt_eq_zero h]

Nonzero Square Root of Nonnegative Real Numbers

Informal description

For any nonnegative real number $x$, the square root of $x$ is nonzero if and only if $x$ is nonzero, i.e., $\sqrt{x} \neq 0 \leftrightarrow x \neq 0$.

Real.sqrt_ne_zero' theorem

: √x ≠ 0 ↔ 0 < x

Full source

theorem sqrt_ne_zero' : √x√x ≠ 0√x ≠ 0 ↔ 0 < x := by rw [← not_le, not_iff_not, sqrt_eq_zero']

Nonzero Square Root if and only if Positive Argument

Informal description

For any real number $x$, the square root of $x$ is nonzero if and only if $x$ is strictly positive, i.e., $\sqrt{x} \neq 0 \leftrightarrow x > 0$.

Real.sqrt_pos theorem

: 0 < √x ↔ 0 < x

Full source

@[simp]
theorem sqrt_pos : 0 < √x ↔ 0 < x :=
  lt_iff_lt_of_le_iff_le (Iff.trans (by simp [le_antisymm_iff, sqrt_nonneg]) sqrt_eq_zero')

Square Root Positivity Condition: $\sqrt{x} > 0 \leftrightarrow x > 0$

Informal description

For any real number $x$, the square root of $x$ is positive if and only if $x$ is positive, i.e., $\sqrt{x} > 0 \leftrightarrow x > 0$.

Real.sqrt_le_sqrt_iff' theorem

(hx : 0 < x) : √x ≤ √y ↔ x ≤ y

Full source

lemma sqrt_le_sqrt_iff' (hx : 0 < x) : √x√x ≤ √y ↔ x ≤ y := by
  obtain hy | hy := le_total y 0
  · exact iff_of_false ((sqrt_eq_zero_of_nonpos hy).trans_lt <| sqrt_pos.2 hx).not_le
      (hy.trans_lt hx).not_le
  · exact sqrt_le_sqrt_iff hy

Square Root Order Preservation for Positive Reals: $\sqrt{x} \leq \sqrt{y} \leftrightarrow x \leq y$ when $x > 0$

Informal description

For any real numbers $x$ and $y$ with $x > 0$, the inequality $\sqrt{x} \leq \sqrt{y}$ holds if and only if $x \leq y$.

Real.one_le_sqrt theorem

: 1 ≤ √x ↔ 1 ≤ x

Full source

@[simp] lemma one_le_sqrt : 1 ≤ √x ↔ 1 ≤ x := by
  rw [← sqrt_one, sqrt_le_sqrt_iff' zero_lt_one, sqrt_one]

Square Root Inequality: $1 \leq \sqrt{x} \leftrightarrow 1 \leq x$

Informal description

For any real number $x$, the inequality $1 \leq \sqrt{x}$ holds if and only if $1 \leq x$.

Real.sqrt_le_one theorem

: √x ≤ 1 ↔ x ≤ 1

Full source

@[simp] lemma sqrt_le_one : √x√x ≤ 1 ↔ x ≤ 1 := by
  rw [← sqrt_one, sqrt_le_sqrt_iff zero_le_one, sqrt_one]

Square Root Inequality: $\sqrt{x} \leq 1 \leftrightarrow x \leq 1$

Informal description

For any real number $x$, the inequality $\sqrt{x} \leq 1$ holds if and only if $x \leq 1$.

Mathlib.Meta.Positivity.evalNNRealSqrt definition

: PositivityExt

Full source

/-- Extension for the `positivity` tactic: a square root of a strictly positive nonnegative real is
positive. -/
@[positivity NNReal.sqrt _]
def evalNNRealSqrt : PositivityExt where eval {u α} _zα _pα e := do
  match u, α, e with
  | 0, ~q(NNReal), ~q(NNReal.sqrt $a) =>
    let ra ← core  q(inferInstance) q(inferInstance) a
    assertInstancesCommute
    match ra with
    | .positive pa => pure (.positive q(NNReal.sqrt_pos_of_pos $pa))
    | _ => failure -- this case is dealt with by generic nonnegativity of nnreals
  | _, _, _ => throwError "not NNReal.sqrt"

Positivity of square root on nonnegative reals

Informal description

The positivity extension tactic for the square root function on nonnegative real numbers, which proves that if the input is strictly positive, then its square root is also strictly positive.

Mathlib.Meta.Positivity.evalSqrt definition

: PositivityExt

Full source

/-- Extension for the `positivity` tactic: a square root is nonnegative, and is strictly positive if
its input is. -/
@[positivity √_]
def evalSqrt : PositivityExt where eval {u α} _zα _pα e := do
  match u, α, e with
  | 0, ~q(ℝ), ~q(√$a) =>
    let ra ← catchNone <| core q(inferInstance) q(inferInstance) a
    assertInstancesCommute
    match ra with
    | .positive pa => pure (.positive q(Real.sqrt_pos_of_pos $pa))
    | _ => pure (.nonnegative q(Real.sqrt_nonneg $a))
  | _, _, _ => throwError "not Real.sqrt"

Square root of a real number

Informal description

The square root function on real numbers, denoted $\sqrt{x}$, is defined to be the nonnegative square root of a nonnegative real number $x$ and zero for negative $x$. It is the extension of the square root function from nonnegative real numbers to all real numbers.

Real.sqrt_mul theorem

{x : ℝ} (hx : 0 ≤ x) (y : ℝ) : √(x * y) = √x * √y

Full source

@[simp]
theorem sqrt_mul {x : ℝ} (hx : 0 ≤ x) (y : ℝ) : √(x * y) = √x * √y := by
  simp_rw [Real.sqrt, ← NNReal.coe_mul, NNReal.coe_inj, Real.toNNReal_mul hx, NNReal.sqrt_mul]

Square Root of Product: $\sqrt{xy} = \sqrt{x}\sqrt{y}$ for $x \geq 0$

Informal description

For any real number $x \geq 0$ and any real number $y$, the square root of the product $x \cdot y$ equals the product of the square roots, i.e., $\sqrt{x \cdot y} = \sqrt{x} \cdot \sqrt{y}$.

Real.sqrt_mul' theorem

(x) {y : ℝ} (hy : 0 ≤ y) : √(x * y) = √x * √y

Full source

@[simp]
theorem sqrt_mul' (x) {y : ℝ} (hy : 0 ≤ y) : √(x * y) = √x * √y := by
  rw [mul_comm, sqrt_mul hy, mul_comm]

Square Root of Product: $\sqrt{xy} = \sqrt{x}\sqrt{y}$ for $y \geq 0$

Informal description

For any real number $x$ and any nonnegative real number $y$, the square root of the product $x \cdot y$ equals the product of the square roots, i.e., $\sqrt{x \cdot y} = \sqrt{x} \cdot \sqrt{y}$.

Real.sqrt_inv theorem

(x : ℝ) : √x⁻¹ = (√x)⁻¹

Full source

@[simp]
theorem sqrt_inv (x : ℝ) : √x⁻¹ = (√x)⁻¹ := by
  rw [Real.sqrt, Real.toNNReal_inv, NNReal.sqrt_inv, NNReal.coe_inv, Real.sqrt]

Square Root of Inverse Equals Inverse of Square Root: $\sqrt{x^{-1}} = (\sqrt{x})^{-1}$

Informal description

For any real number $x$, the square root of its multiplicative inverse equals the multiplicative inverse of its square root, i.e., $\sqrt{x^{-1}} = (\sqrt{x})^{-1}$.

Real.sqrt_div theorem

{x : ℝ} (hx : 0 ≤ x) (y : ℝ) : √(x / y) = √x / √y

Full source

@[simp]
theorem sqrt_div {x : ℝ} (hx : 0 ≤ x) (y : ℝ) : √(x / y) = √x / √y := by
  rw [division_def, sqrt_mul hx, sqrt_inv, division_def]

Square Root of Quotient: $\sqrt{x / y} = \sqrt{x} / \sqrt{y}$ for $x \geq 0$

Informal description

For any real number $x \geq 0$ and any real number $y$, the square root of the quotient $x / y$ equals the quotient of the square roots, i.e., $\sqrt{x / y} = \sqrt{x} / \sqrt{y}$.

Real.sqrt_div' theorem

(x) {y : ℝ} (hy : 0 ≤ y) : √(x / y) = √x / √y

Full source

@[simp]
theorem sqrt_div' (x) {y : ℝ} (hy : 0 ≤ y) : √(x / y) = √x / √y := by
  rw [division_def, sqrt_mul' x (inv_nonneg.2 hy), sqrt_inv, division_def]

Square Root of Quotient: $\sqrt{x / y} = \sqrt{x} / \sqrt{y}$ for $y \geq 0$

Informal description

For any real number $x$ and any nonnegative real number $y \geq 0$, the square root of the quotient $x / y$ equals the quotient of the square roots, i.e., $\sqrt{x / y} = \sqrt{x} / \sqrt{y}$.

Real.div_sqrt theorem

: x / √x = √x

Full source

@[simp]
theorem div_sqrt : x / √x = √x := by
  rcases le_or_lt x 0 with h | h
  · rw [sqrt_eq_zero'.mpr h, div_zero]
  · rw [div_eq_iff (sqrt_ne_zero'.mpr h), mul_self_sqrt h.le]

Quotient-Square Root Identity: $x / \sqrt{x} = \sqrt{x}$ for $x > 0$

Informal description

For any real number $x > 0$, the quotient of $x$ divided by its square root equals the square root of $x$, i.e., $x / \sqrt{x} = \sqrt{x}$.

Real.sqrt_div_self' theorem

: √x / x = 1 / √x

Full source

theorem sqrt_div_self' : √x / x = 1 / √x := by rw [← div_sqrt, one_div_div, div_sqrt]

Square Root Quotient Identity: $\frac{\sqrt{x}}{x} = \frac{1}{\sqrt{x}}$ for $x > 0$

Informal description

For any real number $x > 0$, the quotient of the square root of $x$ divided by $x$ equals the reciprocal of the square root of $x$, i.e., $\frac{\sqrt{x}}{x} = \frac{1}{\sqrt{x}}$.

Real.sqrt_div_self theorem

: √x / x = (√x)⁻¹

Full source

theorem sqrt_div_self : √x / x = (√x)⁻¹ := by rw [sqrt_div_self', one_div]

Square Root Quotient-Inverse Identity: $\frac{\sqrt{x}}{x} = (\sqrt{x})^{-1}$ for $x > 0$

Informal description

For any real number $x > 0$, the quotient of the square root of $x$ divided by $x$ equals the multiplicative inverse of the square root of $x$, i.e., $\frac{\sqrt{x}}{x} = (\sqrt{x})^{-1}$.

Real.lt_sqrt theorem

(hx : 0 ≤ x) : x < √y ↔ x ^ 2 < y

Full source

theorem lt_sqrt (hx : 0 ≤ x) : x < √y ↔ x ^ 2 < y := by
  rw [← sqrt_lt_sqrt_iff (sq_nonneg _), sqrt_sq hx]

Square Root Order Relation: $x < \sqrt{y} \leftrightarrow x^2 < y$ for $x \geq 0$

Informal description

For any real numbers $x$ and $y$ with $x \geq 0$, the inequality $x < \sqrt{y}$ holds if and only if $x^2 < y$.

Real.sq_lt theorem

: x ^ 2 < y ↔ -√y < x ∧ x < √y

Full source

theorem sq_lt : x ^ 2 < y ↔ -√y < x ∧ x < √y := by
  rw [← abs_lt, ← sq_abs, lt_sqrt (abs_nonneg _)]

Square Inequality Characterization: $x^2 < y \leftrightarrow -\sqrt{y} < x < \sqrt{y}$

Informal description

For any real numbers $x$ and $y$, the inequality $x^2 < y$ holds if and only if $x$ lies strictly between $-\sqrt{y}$ and $\sqrt{y}$, i.e., $-\sqrt{y} < x < \sqrt{y}$.

Real.neg_sqrt_lt_of_sq_lt theorem

(h : x ^ 2 < y) : -√y < x

Full source

theorem neg_sqrt_lt_of_sq_lt (h : x ^ 2 < y) : -√y < x :=
  (sq_lt.mp h).1

Lower Bound from Square Inequality: $x^2 < y \Rightarrow -\sqrt{y} < x$

Informal description

For any real numbers $x$ and $y$, if $x^2 < y$, then $-\sqrt{y} < x$.

Real.lt_sqrt_of_sq_lt theorem

(h : x ^ 2 < y) : x < √y

Full source

theorem lt_sqrt_of_sq_lt (h : x ^ 2 < y) : x < √y :=
  (sq_lt.mp h).2

Square Inequality Implication: $x^2 < y \Rightarrow x < \sqrt{y}$

Informal description

For any real numbers $x$ and $y$, if $x^2 < y$, then $x < \sqrt{y}$.

Real.lt_sq_of_sqrt_lt theorem

(h : √x < y) : x < y ^ 2

Full source

theorem lt_sq_of_sqrt_lt (h : √x < y) : x < y ^ 2 := by
  have hy := x.sqrt_nonneg.trans_lt h
  rwa [← sqrt_lt_sqrt_iff_of_pos (sq_pos_of_pos hy), sqrt_sq hy.le]

Square Root Inequality: $\sqrt{x} < y \Rightarrow x < y^2$

Informal description

For any real numbers $x$ and $y$, if $\sqrt{x} < y$, then $x < y^2$.

Real.nat_sqrt_le_real_sqrt theorem

{a : ℕ} : ↑(Nat.sqrt a) ≤ √(a : ℝ)

Full source

/-- The natural square root is at most the real square root -/
theorem nat_sqrt_le_real_sqrt {a : ℕ} : ↑(Nat.sqrt a) ≤ √(a : ℝ) := by
  rw [Real.le_sqrt (Nat.cast_nonneg _) (Nat.cast_nonneg _)]
  norm_cast
  exact Nat.sqrt_le' a

Natural Square Root is Bounded by Real Square Root: $\text{Nat.sqrt}(a) \leq \sqrt{a}$

Informal description

For any natural number $a$, the natural number square root of $a$ (when cast to a real number) is less than or equal to the real square root of $a$, i.e., $\text{Nat.sqrt}(a) \leq \sqrt{a}$.

Real.real_sqrt_lt_nat_sqrt_succ theorem

{a : ℕ} : √(a : ℝ) < Nat.sqrt a + 1

Full source

/-- The real square root is less than the natural square root plus one -/
theorem real_sqrt_lt_nat_sqrt_succ {a : ℕ} : √(a : ℝ) < Nat.sqrt a + 1 := by
  rw [sqrt_lt (by simp)] <;> norm_cast
  · exact Nat.lt_succ_sqrt' a
  · exact Nat.le_add_left 0 (Nat.sqrt a + 1)

Real Square Root is Less Than Natural Square Root Plus One: $\sqrt{a} < \text{Nat.sqrt}(a) + 1$

Informal description

For any natural number $a$, the real square root of $a$ is less than the natural number square root of $a$ plus one, i.e., $\sqrt{a} < \text{Nat.sqrt}(a) + 1$.

Real.real_sqrt_le_nat_sqrt_succ theorem

{a : ℕ} : √(a : ℝ) ≤ Nat.sqrt a + 1

Full source

/-- The real square root is at most the natural square root plus one -/
theorem real_sqrt_le_nat_sqrt_succ {a : ℕ} : √(a : ℝ) ≤ Nat.sqrt a + 1 :=
  real_sqrt_lt_nat_sqrt_succ.le

Upper Bound for Real Square Root: $\sqrt{a} \leq \text{Nat.sqrt}(a) + 1$

Informal description

For any natural number $a$, the real square root of $a$ is less than or equal to the natural number square root of $a$ plus one, i.e., $\sqrt{a} \leq \text{Nat.sqrt}(a) + 1$.

Real.floor_real_sqrt_eq_nat_sqrt theorem

{a : ℕ} : ⌊√(a : ℝ)⌋ = Nat.sqrt a

Full source

/-- The floor of the real square root is the same as the natural square root. -/
@[simp]
theorem floor_real_sqrt_eq_nat_sqrt {a : ℕ} : ⌊√(a : ℝ)⌋ = Nat.sqrt a := by
  rw [Int.floor_eq_iff]
  exact ⟨nat_sqrt_le_real_sqrt, real_sqrt_lt_nat_sqrt_succ⟩

Floor of Real Square Root Equals Natural Square Root: $\lfloor \sqrt{a} \rfloor = \text{Nat.sqrt}(a)$

Informal description

For any natural number $a$, the floor of the real square root of $a$ equals the natural number square root of $a$, i.e., $\lfloor \sqrt{a} \rfloor = \text{Nat.sqrt}(a)$.

Real.nat_floor_real_sqrt_eq_nat_sqrt theorem

{a : ℕ} : ⌊√(a : ℝ)⌋₊ = Nat.sqrt a

Full source

/-- The natural floor of the real square root is the same as the natural square root. -/
@[simp]
theorem nat_floor_real_sqrt_eq_nat_sqrt {a : ℕ} : ⌊√(a : ℝ)⌋₊ = Nat.sqrt a := by
  rw [Nat.floor_eq_iff (sqrt_nonneg a)]
  exact ⟨nat_sqrt_le_real_sqrt, real_sqrt_lt_nat_sqrt_succ⟩

Natural Floor of Real Square Root Equals Natural Square Root: $\lfloor \sqrt{a} \rfloor_\mathbb{N} = \text{Nat.sqrt}(a)$

Informal description

For any natural number $a$, the natural floor of the real square root of $a$ equals the natural number square root of $a$, i.e., $\lfloor \sqrt{a} \rfloor_\mathbb{N} = \text{Nat.sqrt}(a)$.

Real.sqrt_one_add_le theorem

(h : -1 ≤ x) : √(1 + x) ≤ 1 + x / 2

Full source

/-- Bernoulli's inequality for exponent `1 / 2`, stated using `sqrt`. -/
theorem sqrt_one_add_le (h : -1 ≤ x) : √(1 + x) ≤ 1 + x / 2 := by
  refine sqrt_le_iff.mpr ⟨by linarith, ?_⟩
  calc 1 + x
    _ ≤ 1 + x + (x / 2) ^ 2 := le_add_of_nonneg_right <| sq_nonneg _
    _ = _ := by ring

Square Root Inequality: $\sqrt{1 + x} \leq 1 + \frac{x}{2}$ for $x \geq -1$

Informal description

For any real number $x$ such that $x \geq -1$, the square root of $1 + x$ satisfies the inequality $\sqrt{1 + x} \leq 1 + \frac{x}{2}$.

Filter.Tendsto.sqrt theorem

{f : α → ℝ} {l : Filter α} {x : ℝ} (h : Tendsto f l (𝓝 x)) : Tendsto (fun x => √(f x)) l (𝓝 (√x))

Full source

theorem Filter.Tendsto.sqrt {f : α → ℝ} {l : Filter α} {x : ℝ} (h : Tendsto f l (𝓝 x)) :
    Tendsto (fun x => √(f x)) l (𝓝 (√x)) :=
  (continuous_sqrt.tendsto _).comp h

Limit Preservation of Square Root under Filter Convergence

Informal description

Let $f : \alpha \to \mathbb{R}$ be a function and $l$ be a filter on $\alpha$. For any real number $x$, if $f$ tends to $x$ along the filter $l$, then the composition $\sqrt{f}$ tends to $\sqrt{x}$ along $l$.

ContinuousWithinAt.sqrt theorem

(h : ContinuousWithinAt f s x) : ContinuousWithinAt (fun x => √(f x)) s x

Full source

nonrec theorem ContinuousWithinAt.sqrt (h : ContinuousWithinAt f s x) :
    ContinuousWithinAt (fun x => √(f x)) s x :=
  h.sqrt

Continuity Within a Set of the Square Root Function

Informal description

Let $f : \alpha \to \mathbb{R}$ be a function, $s$ a subset of $\alpha$, and $x \in \alpha$. If $f$ is continuous within $s$ at $x$, then the function $\sqrt{f}$ is also continuous within $s$ at $x$.

ContinuousAt.sqrt theorem

(h : ContinuousAt f x) : ContinuousAt (fun x => √(f x)) x

Full source

@[fun_prop]
nonrec theorem ContinuousAt.sqrt (h : ContinuousAt f x) : ContinuousAt (fun x => √(f x)) x :=
  h.sqrt

Continuity of Square Root Composition at a Point: $\sqrt{f(x)}$ is Continuous at $x$ When $f$ is Continuous at $x$

Informal description

Let $f : X \to \mathbb{R}$ be a function defined on a topological space $X$, and let $x \in X$. If $f$ is continuous at $x$, then the function $x \mapsto \sqrt{f(x)}$ is also continuous at $x$.

ContinuousOn.sqrt theorem

(h : ContinuousOn f s) : ContinuousOn (fun x => √(f x)) s

Full source

@[fun_prop]
theorem ContinuousOn.sqrt (h : ContinuousOn f s) : ContinuousOn (fun x => √(f x)) s :=
  fun x hx => (h x hx).sqrt

Continuity of Square Root Composition on a Set: $\sqrt{f(x)}$ is Continuous on $s$ When $f$ is Continuous on $s$

Informal description

Let $f : X \to \mathbb{R}$ be a function defined on a topological space $X$, and let $s \subseteq X$. If $f$ is continuous on $s$, then the function $x \mapsto \sqrt{f(x)}$ is also continuous on $s$.

Continuous.sqrt theorem

(h : Continuous f) : Continuous fun x => √(f x)

Full source

@[continuity, fun_prop]
theorem Continuous.sqrt (h : Continuous f) : Continuous fun x => √(f x) :=
  continuous_sqrt.comp h

Continuity of Composition with Square Root Function: $\sqrt{f(x)}$ is Continuous When $f$ is Continuous

Informal description

Let $f : X \to \mathbb{R}$ be a continuous function from a topological space $X$ to the real numbers. Then the function $x \mapsto \sqrt{f(x)}$ is also continuous.

NNReal.sum_mul_le_sqrt_mul_sqrt theorem

 (s : Finset ι) (f g : ι → ℝ≥0) : ∑ i ∈ s, f i * g i ≤ sqrt (∑ i ∈ s, f i ^ 2) * sqrt (∑ i ∈ s, g i ^ 2)

Full source

/-- **Cauchy-Schwarz inequality** for finsets using square roots in `ℝ≥0`. -/
lemma sum_mul_le_sqrt_mul_sqrt (s : Finset ι) (f g : ι → ℝ≥0) :
    ∑ i ∈ s, f i * g i ≤ sqrt (∑ i ∈ s, f i ^ 2) * sqrt (∑ i ∈ s, g i ^ 2) :=
  (le_sqrt_iff_sq_le.2 <| sum_mul_sq_le_sq_mul_sq _ _ _).trans_eq <| sqrt_mul _ _

Cauchy-Schwarz Inequality for Nonnegative Real-Valued Functions on Finite Sets: $\sum f_i g_i \leq \sqrt{\sum f_i^2} \sqrt{\sum g_i^2}$

Informal description

For any finite set $s$ and functions $f, g : s \to \mathbb{R}_{\geq 0}$, the following inequality holds: \[ \sum_{i \in s} f(i) g(i) \leq \sqrt{\sum_{i \in s} f(i)^2} \cdot \sqrt{\sum_{i \in s} g(i)^2}. \]

NNReal.sum_sqrt_mul_sqrt_le theorem

 (s : Finset ι) (f g : ι → ℝ≥0) : ∑ i ∈ s, sqrt (f i) * sqrt (g i) ≤ sqrt (∑ i ∈ s, f i) * sqrt (∑ i ∈ s, g i)

Full source

/-- **Cauchy-Schwarz inequality** for finsets using square roots in `ℝ≥0`. -/
lemma sum_sqrt_mul_sqrt_le (s : Finset ι) (f g : ι → ℝ≥0) :
    ∑ i ∈ s, sqrt (f i) * sqrt (g i) ≤ sqrt (∑ i ∈ s, f i) * sqrt (∑ i ∈ s, g i) := by
  simpa [*] using sum_mul_le_sqrt_mul_sqrt _ (fun x ↦ sqrt (f x)) (fun x ↦ sqrt (g x))

Cauchy-Schwarz Inequality for Square Roots of Nonnegative Real-Valued Functions on Finite Sets: $\sum \sqrt{f_i} \sqrt{g_i} \leq \sqrt{\sum f_i} \sqrt{\sum g_i}$

Informal description

For any finite set $s$ and nonnegative real-valued functions $f, g : s \to \mathbb{R}_{\geq 0}$, the following inequality holds: \[ \sum_{i \in s} \sqrt{f(i)} \cdot \sqrt{g(i)} \leq \sqrt{\sum_{i \in s} f(i)} \cdot \sqrt{\sum_{i \in s} g(i)}. \]

Real.sum_mul_le_sqrt_mul_sqrt theorem

(s : Finset ι) (f g : ι → ℝ) : ∑ i ∈ s, f i * g i ≤ √(∑ i ∈ s, f i ^ 2) * √(∑ i ∈ s, g i ^ 2)

Full source

/-- **Cauchy-Schwarz inequality** for finsets using square roots in `ℝ`. -/
lemma sum_mul_le_sqrt_mul_sqrt (s : Finset ι) (f g : ι → ℝ) :
    ∑ i ∈ s, f i * g i ≤ √(∑ i ∈ s, f i ^ 2) * √(∑ i ∈ s, g i ^ 2) :=
  (le_sqrt_of_sq_le <| sum_mul_sq_le_sq_mul_sq _ _ _).trans_eq <| sqrt_mul
    (sum_nonneg fun _ _ ↦ by positivity) _

Cauchy-Schwarz Inequality for Real-Valued Functions on Finite Sets: $\sum f_i g_i \leq \sqrt{\sum f_i^2} \sqrt{\sum g_i^2}$

Informal description

For any finite set $s$ and real-valued functions $f, g : s \to \mathbb{R}$, the following inequality holds: \[ \sum_{i \in s} f(i) g(i) \leq \sqrt{\sum_{i \in s} f(i)^2} \cdot \sqrt{\sum_{i \in s} g(i)^2}. \]

Real.sum_sqrt_mul_sqrt_le theorem

 (s : Finset ι) (hf : ∀ i, 0 ≤ f i) (hg : ∀ i, 0 ≤ g i) : ∑ i ∈ s, √(f i) * √(g i) ≤ √(∑ i ∈ s, f i) * √(∑ i ∈ s, g i)

Full source

/-- **Cauchy-Schwarz inequality** for finsets using square roots in `ℝ`. -/
lemma sum_sqrt_mul_sqrt_le (s : Finset ι) (hf : ∀ i, 0 ≤ f i) (hg : ∀ i, 0 ≤ g i) :
    ∑ i ∈ s, √(f i) * √(g i) ≤ √(∑ i ∈ s, f i) * √(∑ i ∈ s, g i) := by
  simpa [*] using sum_mul_le_sqrt_mul_sqrt _ (fun x ↦ √(f x)) (fun x ↦ √(g x))

Cauchy-Schwarz Inequality for Square Roots of Nonnegative Real-Valued Functions: $\sum \sqrt{f_i} \sqrt{g_i} \leq \sqrt{\sum f_i} \sqrt{\sum g_i}$

Informal description

For any finite set $s$ and real-valued functions $f, g : s \to \mathbb{R}$ such that $f(i) \geq 0$ and $g(i) \geq 0$ for all $i \in s$, the following inequality holds: \[ \sum_{i \in s} \sqrt{f(i)} \cdot \sqrt{g(i)} \leq \sqrt{\sum_{i \in s} f(i)} \cdot \sqrt{\sum_{i \in s} g(i)}. \]

Mathlib.Data.Real.Sqrt

Implementation notes

Tags