doc-next-gen

Mathlib.Data.Nat.Sqrt

Module docstring

{"# Properties of the natural number square root function. ","### sqrt

See [Wikipedia, Methods of computing square roots] (https://en.wikipedia.org/wiki/Methodsofcomputingsquareroots#Binarynumeralsystem(base2)). "}

Nat.sqrt.iter_sq_le theorem
(n guess : ℕ) : sqrt.iter n guess * sqrt.iter n guess ≤ n
Full source 
lemma sqrt.iter_sq_le (n guess : ℕ) : sqrt.iter n guess * sqrt.iter n guess ≤ n := by
  unfold sqrt.iter
  let next := (guess + n / guess) / 2
  if h : next < guess then
    simpa only [next, dif_pos h] using sqrt.iter_sq_le n next
  else
    simp only [next, dif_neg h]
    apply Nat.mul_le_of_le_div
    apply Nat.le_of_add_le_add_left (a := guess)
    rw [← Nat.mul_two, ← le_div_iff_mul_le]
    · exact Nat.le_of_not_lt h
    · exact Nat.zero_lt_two
Iterative Square Root Bound: $(\mathit{sqrt.iter}\ n\ \mathit{guess})^2 \leq n$
Informal description
For any natural numbers $n$ and $\mathit{guess}$, the square of the iterative square root function $\mathit{sqrt.iter}\ n\ \mathit{guess}$ is less than or equal to $n$, i.e., $(\mathit{sqrt.iter}\ n\ \mathit{guess})^2 \leq n$.
Nat.sqrt.lt_iter_succ_sq theorem
(n guess : ℕ) (hn : n < (guess + 1) * (guess + 1)) : n < (sqrt.iter n guess + 1) * (sqrt.iter n guess + 1)
Full source 
lemma sqrt.lt_iter_succ_sq (n guess : ℕ) (hn : n < (guess + 1) * (guess + 1)) :
    n < (sqrt.iter n guess + 1) * (sqrt.iter n guess + 1) := by
  unfold sqrt.iter
  -- m was `next`
  let m := (guess + n / guess) / 2
  dsimp
  split_ifs with h
  · suffices n < (m + 1) * (m + 1) by
      simpa only [dif_pos h] using sqrt.lt_iter_succ_sq n m this
    refine Nat.lt_of_mul_lt_mul_left ?_ (a := 4 * (guess * guess))
    apply Nat.lt_of_le_of_lt AM_GM
    rw [show (4 : ℕ) = 2 * 2 from rfl]
    rw [Nat.mul_mul_mul_comm 2, Nat.mul_mul_mul_comm (2 * guess)]
    refine Nat.mul_self_lt_mul_self (?_ : _ < _ * ((_ / 2) + 1))
    rw [← add_div_right _ (by decide), Nat.mul_comm 2, Nat.mul_assoc,
      show guess + n / guess + 2 = (guess + n / guess + 1) + 1 from rfl]
    have aux_lemma {a : ℕ} : a ≤ 2 * ((a + 1) / 2) := by omega
    refine lt_of_lt_of_le ?_ (Nat.mul_le_mul_left _ aux_lemma)
    rw [Nat.add_assoc, Nat.mul_add]
    exact Nat.add_lt_add_left (lt_mul_div_succ _ (lt_of_le_of_lt (Nat.zero_le m) h)) _
  · simpa only [dif_neg h] using hn
Iterative Square Root Preserves Upper Bound: $n < (\mathit{guess} + 1)^2 \implies n < (\mathit{sqrt.iter}\ n\ \mathit{guess} + 1)^2$
Informal description
For any natural numbers $n$ and $\mathit{guess}$, if $n < (\mathit{guess} + 1)^2$, then $n < (\mathit{sqrt.iter}\ n\ \mathit{guess} + 1)^2$, where $\mathit{sqrt.iter}$ is the iterative square root function for natural numbers.
Nat.sqrt_le theorem
(n : ℕ) : sqrt n * sqrt n ≤ n
Full source 
lemma sqrt_le (n : ℕ) : sqrt n * sqrt n ≤ n := (sqrt_isSqrt n).left
Square of Natural Square Root is Bounded by Original Number
Informal description
For any natural number $n$, the square of its natural number square root is less than or equal to $n$, i.e., $\sqrt{n} \times \sqrt{n} \leq n$.
Nat.sqrt_le' theorem
(n : ℕ) : sqrt n ^ 2 ≤ n
Full source 
lemma sqrt_le' (n : ℕ) : sqrt n ^ 2 ≤ n := by simpa [Nat.pow_two] using sqrt_le n
Square of Natural Square Root is Bounded by Original Number (Power Form)
Informal description
For any natural number $n$, the square of its natural number square root is less than or equal to $n$, i.e., $(\sqrt{n})^2 \leq n$.
Nat.lt_succ_sqrt theorem
(n : ℕ) : n < succ (sqrt n) * succ (sqrt n)
Full source 
lemma lt_succ_sqrt (n : ℕ) : n < succ (sqrt n) * succ (sqrt n) := (sqrt_isSqrt n).right
$n < (s(\sqrt{n}))^2$ for natural numbers
Informal description
For any natural number $n$, we have $n < (s(\sqrt{n}))^2$, where $s$ denotes the successor function and $\sqrt{n}$ is the natural number square root of $n$.
Nat.lt_succ_sqrt' theorem
(n : ℕ) : n < succ (sqrt n) ^ 2
Full source 
lemma lt_succ_sqrt' (n : ℕ) : n < succ (sqrt n) ^ 2 := by simpa [Nat.pow_two] using lt_succ_sqrt n
$n < (s(\sqrt{n}))^2$ for natural numbers (power form)
Informal description
For any natural number $n$, we have $n < (s(\sqrt{n}))^2$, where $s$ denotes the successor function and $\sqrt{n}$ is the natural number square root of $n$.
Nat.sqrt_le_add theorem
(n : ℕ) : n ≤ sqrt n * sqrt n + sqrt n + sqrt n
Full source 
lemma sqrt_le_add (n : ℕ) : n ≤ sqrt n * sqrt n + sqrt n + sqrt n := by
  rw [← succ_mul]; exact le_of_lt_succ (lt_succ_sqrt n)
Upper Bound for Natural Numbers via Square Root: $n \leq (\sqrt{n})^2 + 2\sqrt{n}$
Informal description
For any natural number $n$, we have $n \leq (\sqrt{n})^2 + \sqrt{n} + \sqrt{n}$, where $\sqrt{n}$ denotes the natural number square root of $n$.
Nat.le_sqrt' theorem
: m ≤ sqrt n ↔ m ^ 2 ≤ n
Full source 
lemma le_sqrt' : m ≤ sqrt n ↔ m ^ 2 ≤ n := by simpa only [Nat.pow_two] using le_sqrt
Square Root Comparison: $m \leq \sqrt{n} \leftrightarrow m^2 \leq n$
Informal description
For any natural numbers $m$ and $n$, the inequality $m \leq \sqrt{n}$ holds if and only if $m^2 \leq n$.
Nat.sqrt_lt theorem
: sqrt m < n ↔ m < n * n
Full source 
lemma sqrt_lt : sqrtsqrt m < n ↔ m < n * n := by simp only [← not_le, le_sqrt]
Square Root Comparison: $\sqrt{m} < n \leftrightarrow m < n^2$
Informal description
For any natural numbers $m$ and $n$, the square root of $m$ is less than $n$ if and only if $m$ is less than $n \times n$.
Nat.sqrt_lt' theorem
: sqrt m < n ↔ m < n ^ 2
Full source 
lemma sqrt_lt' : sqrtsqrt m < n ↔ m < n ^ 2 := by simp only [← not_le, le_sqrt']
Square Root Comparison: $\sqrt{m} < n \leftrightarrow m < n^2$
Informal description
For any natural numbers $m$ and $n$, the square root of $m$ is less than $n$ if and only if $m$ is less than $n^2$. In other words, $\sqrt{m} < n \leftrightarrow m < n^2$.
Nat.sqrt_le_self theorem
(n : ℕ) : sqrt n ≤ n
Full source 
lemma sqrt_le_self (n : ℕ) : sqrt n ≤ n := le_trans (le_mul_self _) (sqrt_le n)
Square Root Bounded by Original Number: $\sqrt{n} \leq n$
Informal description
For any natural number $n$, the square root of $n$ is less than or equal to $n$, i.e., $\sqrt{n} \leq n$.
Nat.sqrt_le_sqrt theorem
(h : m ≤ n) : sqrt m ≤ sqrt n
Full source 
lemma sqrt_le_sqrt (h : m ≤ n) : sqrt m ≤ sqrt n := le_sqrt.2 (le_trans (sqrt_le _) h)
Monotonicity of Natural Square Root: $m \leq n \Rightarrow \sqrt{m} \leq \sqrt{n}$
Informal description
For any natural numbers $m$ and $n$, if $m \leq n$, then $\sqrt{m} \leq \sqrt{n}$.
Nat.sqrt_zero theorem
: sqrt 0 = 0
Full source 
@[simp] lemma sqrt_zero : sqrt 0 = 0 := rfl
Square Root of Zero: $\sqrt{0} = 0$
Informal description
The square root of the natural number $0$ is equal to $0$, i.e., $\sqrt{0} = 0$.
Nat.sqrt_one theorem
: sqrt 1 = 1
Full source 
@[simp] lemma sqrt_one : sqrt 1 = 1 := rfl
Square Root of One is One
Informal description
The square root of the natural number $1$ is equal to $1$, i.e., $\sqrt{1} = 1$.
Nat.le_three_of_sqrt_eq_one theorem
(h : sqrt n = 1) : n ≤ 3
Full source 
lemma le_three_of_sqrt_eq_one (h : sqrt n = 1) : n ≤ 3 :=
  le_of_lt_succ <| (@sqrt_lt n 2).1 <| by rw [h]; decide
Upper Bound for Numbers with Square Root One: $\sqrt{n} = 1 \Rightarrow n \leq 3$
Informal description
For any natural number $n$, if the square root of $n$ equals $1$, then $n$ is less than or equal to $3$.
Nat.sqrt_lt_self theorem
(h : 1 < n) : sqrt n < n
Full source 
lemma sqrt_lt_self (h : 1 < n) : sqrt n < n :=
  sqrt_lt.2 <| by have := Nat.mul_lt_mul_of_pos_left h (lt_of_succ_lt h); rwa [Nat.mul_one] at this
Square Root is Less Than Original Number for $n > 1$
Informal description
For any natural number $n$ such that $1 < n$, the square root of $n$ is strictly less than $n$, i.e., $\sqrt{n} < n$.
Nat.sqrt_pos theorem
: 0 < sqrt n ↔ 0 < n
Full source 
lemma sqrt_pos : 0 < sqrt n ↔ 0 < n :=
  le_sqrt
Positivity of Square Root: $0 < \sqrt{n} \leftrightarrow 0 < n$
Informal description
For any natural number $n$, the square root of $n$ is positive if and only if $n$ is positive, i.e., $0 < \sqrt{n} \leftrightarrow 0 < n$.
Nat.sqrt_add_eq theorem
(n : ℕ) (h : a ≤ n + n) : sqrt (n * n + a) = n
Full source 
lemma sqrt_add_eq (n : ℕ) (h : a ≤ n + n) : sqrt (n * n + a) = n :=
  le_antisymm
    (le_of_lt_succ <|
      sqrt_lt.2 <| by
        rw [succ_mul, mul_succ, add_succ, Nat.add_assoc]
        exact lt_succ_of_le (Nat.add_le_add_left h _))
    (le_sqrt.2 <| Nat.le_add_right _ _)
Square Root of $n^2 + a$ Equals $n$ When $a \leq 2n$
Informal description
For any natural numbers $n$ and $a$ such that $a \leq 2n$, the square root of $n^2 + a$ equals $n$, i.e., $\sqrt{n^2 + a} = n$.
Nat.sqrt_add_eq' theorem
(n : ℕ) (h : a ≤ n + n) : sqrt (n ^ 2 + a) = n
Full source 
lemma sqrt_add_eq' (n : ℕ) (h : a ≤ n + n) : sqrt (n ^ 2 + a) = n := by
  simpa [Nat.pow_two] using sqrt_add_eq n h
Square Root of $n^2 + a$ Equals $n$ When $a \leq 2n$
Informal description
For any natural numbers $n$ and $a$ such that $a \leq 2n$, the square root of $n^2 + a$ equals $n$, i.e., $\sqrt{n^2 + a} = n$.
Nat.sqrt_eq theorem
(n : ℕ) : sqrt (n * n) = n
Full source 
lemma sqrt_eq (n : ℕ) : sqrt (n * n) = n := sqrt_add_eq n (zero_le _)
Square Root of Perfect Square: $\sqrt{n^2} = n$
Informal description
For any natural number $n$, the square root of $n^2$ equals $n$, i.e., $\sqrt{n^2} = n$.
Nat.sqrt_eq' theorem
(n : ℕ) : sqrt (n ^ 2) = n
Full source 
lemma sqrt_eq' (n : ℕ) : sqrt (n ^ 2) = n := sqrt_add_eq' n (zero_le _)
Square Root of Perfect Square: $\sqrt{n^2} = n$
Informal description
For any natural number $n$, the square root of $n^2$ equals $n$, i.e., $\sqrt{n^2} = n$.
Nat.sqrt_succ_le_succ_sqrt theorem
(n : ℕ) : sqrt n.succ ≤ n.sqrt.succ
Full source 
lemma sqrt_succ_le_succ_sqrt (n : ℕ) : sqrt n.succ ≤ n.sqrt.succ :=
  le_of_lt_succ <| sqrt_lt.2 <| lt_succ_of_le <|
  succ_le_succ <| le_trans (sqrt_le_add n) <| Nat.add_le_add_right
    (by refine add_le_add (Nat.mul_le_mul_right _ ?_) ?_ <;> exact Nat.le_add_right _ 2) _
Monotonicity of Square Root: $\sqrt{n+1} \leq \sqrt{n} + 1$
Informal description
For any natural number $n$, the square root of $n+1$ is less than or equal to the successor of the square root of $n$, i.e., $\sqrt{n+1} \leq \sqrt{n} + 1$.
Nat.exists_mul_self theorem
(x : ℕ) : (∃ n, n * n = x) ↔ sqrt x * sqrt x = x
Full source 
lemma exists_mul_self (x : ℕ) : (∃ n, n * n = x) ↔ sqrt x * sqrt x = x :=
  ⟨fun ⟨n, hn⟩ ↦ by rw [← hn, sqrt_eq], fun h ↦ ⟨sqrt x, h⟩⟩
Characterization of Perfect Squares via Square Root: $\exists n, n^2 = x \leftrightarrow \sqrt{x}^2 = x$
Informal description
For any natural number $x$, there exists a natural number $n$ such that $n \times n = x$ if and only if the square of the square root of $x$ equals $x$, i.e., $\sqrt{x} \times \sqrt{x} = x$.
Nat.exists_mul_self' theorem
(x : ℕ) : (∃ n, n ^ 2 = x) ↔ sqrt x ^ 2 = x
Full source 
lemma exists_mul_self' (x : ℕ) : (∃ n, n ^ 2 = x) ↔ sqrt x ^ 2 = x := by
  simpa only [Nat.pow_two] using exists_mul_self x
Characterization of Perfect Squares via Square Root: $\exists n, n^2 = x \leftrightarrow (\sqrt{x})^2 = x$
Informal description
For any natural number $x$, there exists a natural number $n$ such that $n^2 = x$ if and only if $(\sqrt{x})^2 = x$.
Nat.sqrt_mul_sqrt_lt_succ theorem
(n : ℕ) : sqrt n * sqrt n < n + 1
Full source 
lemma sqrt_mul_sqrt_lt_succ (n : ℕ) : sqrt n * sqrt n < n + 1 :=
  Nat.lt_succ_iff.mpr (sqrt_le _)
Square of Natural Square Root is Strictly Less Than Successor
Informal description
For any natural number $n$, the square of its natural number square root is strictly less than $n + 1$, i.e., $\sqrt{n} \times \sqrt{n} < n + 1$.
Nat.sqrt_mul_sqrt_lt_succ' theorem
(n : ℕ) : sqrt n ^ 2 < n + 1
Full source 
lemma sqrt_mul_sqrt_lt_succ' (n : ℕ) : sqrt n ^ 2 < n + 1 :=
  Nat.lt_succ_iff.mpr (sqrt_le' _)
Square of Natural Square Root is Strictly Less Than Successor (Power Form)
Informal description
For any natural number $n$, the square of its natural number square root is strictly less than $n + 1$, i.e., $(\sqrt{n})^2 < n + 1$.
Nat.succ_le_succ_sqrt theorem
(n : ℕ) : n + 1 ≤ (sqrt n + 1) * (sqrt n + 1)
Full source 
lemma succ_le_succ_sqrt (n : ℕ) : n + 1 ≤ (sqrt n + 1) * (sqrt n + 1) :=
  le_of_pred_lt (lt_succ_sqrt _)
Successor Inequality for Natural Number Square Roots: $n + 1 \leq (\sqrt{n} + 1)^2$
Informal description
For any natural number $n$, we have $n + 1 \leq (\sqrt{n} + 1)^2$, where $\sqrt{n}$ denotes the natural number square root of $n$.
Nat.succ_le_succ_sqrt' theorem
(n : ℕ) : n + 1 ≤ (sqrt n + 1) ^ 2
Full source 
lemma succ_le_succ_sqrt' (n : ℕ) : n + 1 ≤ (sqrt n + 1) ^ 2 :=
  le_of_pred_lt (lt_succ_sqrt' _)
Successor Inequality for Natural Number Square Roots: $n + 1 \leq (\sqrt{n} + 1)^2$
Informal description
For any natural number $n$, we have $n + 1 \leq (\sqrt{n} + 1)^2$, where $\sqrt{n}$ denotes the natural number square root of $n$.
Nat.not_exists_sq theorem
(hl : m * m < n) (hr : n < (m + 1) * (m + 1)) : ¬∃ t, t * t = n
Full source 
/-- There are no perfect squares strictly between m² and (m+1)² -/
lemma not_exists_sq (hl : m * m < n) (hr : n < (m + 1) * (m + 1)) : ¬∃ t, t * t = n := by
  rintro ⟨t, rfl⟩
  have h1 : m < t := Nat.mul_self_lt_mul_self_iff.1 hl
  have h2 : t < m + 1 := Nat.mul_self_lt_mul_self_iff.1 hr
  exact (not_lt_of_ge <| le_of_lt_succ h2) h1
No Perfect Squares Between Consecutive Squares in Natural Numbers
Informal description
For any natural numbers $m$ and $n$, if $m^2 < n < (m+1)^2$, then there does not exist a natural number $t$ such that $t^2 = n$.
Nat.not_exists_sq' theorem
: m ^ 2 < n → n < (m + 1) ^ 2 → ¬∃ t, t ^ 2 = n
Full source 
lemma not_exists_sq' : m ^ 2 < n → n < (m + 1) ^ 2 → ¬∃ t, t ^ 2 = n := by
  simpa only [Nat.pow_two] using not_exists_sq
No Perfect Squares Between Consecutive Squares in Natural Numbers
Informal description
For any natural numbers $m$ and $n$, if $m^2 < n < (m+1)^2$, then there does not exist a natural number $t$ such that $t^2 = n$.