data.nat.sqrt

# Square root of natural numbers #

This file defines an efficient binary implementation of the square root function that returns the unique r such that r * r ≤ n < (r + 1) * (r + 1). It takes advantage of the binary representation by replacing the multiplication by 2 appearing in (a + b)^2 = a^2 + 2 * a * b + b^2 by a bitmask manipulation.

## 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_aux_dec {b : } (h : b 0) :
b.shiftr 2 < b
def nat.sqrt_aux  :

Auxiliary function for nat.sqrt. See e.g. https://en.wikipedia.org/wiki/Methods_of_computing_square_roots#Binary_numeral_system_(base_2)

Equations
def nat.sqrt (n : ) :

sqrt n is the square root of a natural number n. If n is not a perfect square, it returns the largest k:ℕ such that k*k ≤ n.

Equations
theorem nat.sqrt_aux_0 (r n : ) :
0.sqrt_aux r n = r
theorem nat.sqrt_aux_1 {r n b : } (h : b 0) {n' : } (h₂ : r + b + n' = n) :
b.sqrt_aux r n = (b.shiftr 2).sqrt_aux (r.div2 + b) n'
theorem nat.sqrt_aux_2 {r n b : } (h : b 0) (h₂ : n < r + b) :
b.sqrt_aux r n = (b.shiftr 2).sqrt_aux r.div2 n
theorem nat.sqrt_le (n : ) :
(nat.sqrt n) * n
theorem nat.sqrt_le' (n : ) :
^ 2 n
theorem nat.lt_succ_sqrt (n : ) :
theorem nat.lt_succ_sqrt' (n : ) :
n < (nat.sqrt n).succ ^ 2
theorem nat.sqrt_le_add (n : ) :
n (nat.sqrt n) * + +
theorem nat.le_sqrt {m n : } :
m m * m n
theorem nat.le_sqrt' {m n : } :
m m ^ 2 n
theorem nat.sqrt_lt {m n : } :
< n m < n * n
theorem nat.sqrt_lt' {m n : } :
< n m < n ^ 2
theorem nat.sqrt_le_self (n : ) :
n
theorem nat.sqrt_le_sqrt {m n : } (h : m n) :
@[simp]
theorem nat.sqrt_zero  :
= 0
theorem nat.sqrt_eq_zero {n : } :
= 0 n = 0
theorem nat.eq_sqrt {n q : } :
q = q * q n n < (q + 1) * (q + 1)
theorem nat.eq_sqrt' {n q : } :
q = q ^ 2 n n < (q + 1) ^ 2
theorem nat.le_three_of_sqrt_eq_one {n : } (h : = 1) :
n 3
theorem nat.sqrt_lt_self {n : } (h : 1 < n) :
< n
theorem nat.sqrt_pos {n : } :
0 < 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
theorem nat.exists_mul_self (x : ) :
(∃ (n : ), n * n = x) (nat.sqrt x) * = x
theorem nat.exists_mul_self' (x : ) :
(∃ (n : ), n ^ 2 = x) ^ 2 = x
theorem nat.sqrt_mul_sqrt_lt_succ (n : ) :
(nat.sqrt n) * < n + 1
theorem nat.sqrt_mul_sqrt_lt_succ' (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