mathlib documentation

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

b.sqrt_aux r n = ite (b = 0) r (let b' : ℕ := b.shiftr 2 in nat.sqrt_aux._match_1 (λ (n' : ℕ), (b.shiftr 2).sqrt_aux (r.div2 + b) n') ((b.shiftr 2).sqrt_aux r.div2 n) (↑n - ↑(r + b)))
nat.sqrt_aux._match_1 _f_1 _f_2 -[1+ ᾰ] = _f_2
nat.sqrt_aux._match_1 _f_1 _f_2 ↑n' = _f_1 n'

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

nat.sqrt n = nat.sqrt._match_1 n n.size
nat.sqrt._match_1 n s.succ = (1.shiftl (bit0 s.div2)).sqrt_aux 0 n
nat.sqrt._match_1 n 0 = 0

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) * nat.sqrt n ≤ n

theorem nat.sqrt_le' (n : ℕ) :

nat.sqrt n ^ 2 ≤ n

theorem nat.lt_succ_sqrt (n : ℕ) :

n < ((nat.sqrt n).succ) * (nat.sqrt n).succ

theorem nat.lt_succ_sqrt' (n : ℕ) :

n < (nat.sqrt n).succ ^ 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 :

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) :

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 :

theorem nat.sqrt_succ_le_succ_sqrt (n : ℕ) :

nat.sqrt n.succ ≤ (nat.sqrt n).succ

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

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