Square root of natural numbers

This file defines an efficient implementation of the square root function that returns the unique r such that r * r ≤ n < (r + 1) * (r + 1).

Reference

See [Wikipedia, Methods of computing square roots] (https://en.wikipedia.org/wiki/Methods_of_computing_square_roots#Binary_numeral_system_(base_2)).

theorem Nat.sqrt_le (n : ℕ) : Nat.sqrt n * Nat.sqrt n ≤ n

theorem Nat.sqrt_le' (n : ℕ) : Nat.sqrt n ^ 2 ≤ n

theorem Nat.lt_succ_sqrt (n : ℕ) : n < Nat.succ (Nat.sqrt n) * Nat.succ (Nat.sqrt n)

theorem Nat.lt_succ_sqrt' (n : ℕ) : n < Nat.succ (Nat.sqrt n) ^ 2

theorem Nat.sqrt_le_add (n : ℕ) : n ≤ Nat.sqrt n * Nat.sqrt n + Nat.sqrt n + Nat.sqrt n

theorem Nat.le_sqrt {m : ℕ} {n : ℕ} : m ≤ Nat.sqrt n ↔ m * m ≤ n

theorem Nat.le_sqrt' {m : ℕ} {n : ℕ} : m ≤ Nat.sqrt n ↔ m ^ 2 ≤ n

theorem Nat.sqrt_lt {m : ℕ} {n : ℕ} : Nat.sqrt m < n ↔ m < n * n

theorem Nat.sqrt_lt' {m : ℕ} {n : ℕ} : Nat.sqrt m < n ↔ m < n ^ 2

theorem Nat.sqrt_le_self (n : ℕ) : Nat.sqrt n ≤ n

theorem Nat.sqrt_le_sqrt {m : ℕ} {n : ℕ} (h : m ≤ n) : Nat.sqrt m ≤ Nat.sqrt n

@[simp]

theorem Nat.sqrt_zero : Nat.sqrt 0 = 0

theorem Nat.sqrt_eq_zero {n : ℕ} : Nat.sqrt n = 0 ↔ n = 0

theorem Nat.eq_sqrt {n : ℕ} {q : ℕ} : q = Nat.sqrt n ↔ q * q ≤ n ∧ n < (q + 1) * (q + 1)

theorem Nat.eq_sqrt' {n : ℕ} {q : ℕ} : q = Nat.sqrt n ↔ q ^ 2 ≤ n ∧ n < (q + 1) ^ 2

theorem Nat.le_three_of_sqrt_eq_one {n : ℕ} (h : Nat.sqrt n = 1) : n ≤ 3

theorem Nat.sqrt_lt_self {n : ℕ} (h : 1 < n) : Nat.sqrt n < n

theorem Nat.sqrt_pos {n : ℕ} : 0 < Nat.sqrt n ↔ 0 < n

theorem Nat.sqrt_add_eq (n : ℕ) {a : ℕ} (h : a ≤ n + n) : Nat.sqrt (n * n + a) = n

theorem Nat.sqrt_add_eq' (n : ℕ) {a : ℕ} (h : a ≤ n + n) : Nat.sqrt (n ^ 2 + a) = n

theorem Nat.sqrt_eq (n : ℕ) : Nat.sqrt (n * n) = n

theorem Nat.sqrt_eq' (n : ℕ) : Nat.sqrt (n ^ 2) = n

@[simp]

theorem Nat.sqrt_one : Nat.sqrt 1 = 1

theorem Nat.sqrt_succ_le_succ_sqrt (n : ℕ) : Nat.sqrt (Nat.succ n) ≤ Nat.succ (Nat.sqrt n)

theorem Nat.exists_mul_self (x : ℕ) : (∃ (n : ℕ), n * n = x) ↔ Nat.sqrt x * Nat.sqrt x = x

theorem Nat.exists_mul_self' (x : ℕ) : (∃ (n : ℕ), n ^ 2 = x) ↔ Nat.sqrt x ^ 2 = x

instance Nat.instDecidablePredNatIsSquareInstMulNat : DecidablePred IsSquare

IsSquare can be decided on ℕ by checking against the square root.

Equations

• Nat.instDecidablePredNatIsSquareInstMulNat m = decidable_of_iff' (Nat.sqrt m * Nat.sqrt m = m) ⋯

theorem Nat.sqrt_mul_sqrt_lt_succ (n : ℕ) : Nat.sqrt n * Nat.sqrt n < n + 1

theorem Nat.sqrt_mul_sqrt_lt_succ' (n : ℕ) : Nat.sqrt n ^ 2 < n + 1

theorem Nat.succ_le_succ_sqrt (n : ℕ) : n + 1 ≤ (Nat.sqrt n + 1) * (Nat.sqrt n + 1)

theorem Nat.succ_le_succ_sqrt' (n : ℕ) : n + 1 ≤ (Nat.sqrt n + 1) ^ 2

theorem Nat.not_exists_sq {n : ℕ} {m : ℕ} (hl : m * m < n) (hr : n < (m + 1) * (m + 1)) : ¬∃ (t : ℕ), t * t = n

There are no perfect squares strictly between m² and (m+1)²

theorem Nat.not_exists_sq' {n : ℕ} {m : ℕ} (hl : m ^ 2 < n) (hr : n < (m + 1) ^ 2) : ¬∃ (t : ℕ), t ^ 2 = n