mathlib documentation

data.nat.sqrt

Square root of natural numbers

An efficient binary implementation of a (sqrt n) function that returns s such that

s*s ≤ n ≤ s*s + s + s

theorem nat.sqrt_aux_dec {b : ℕ} (h : b ≠ 0) :

b.shiftr 2 < b

def nat.sqrt_aux (a a_1 a_2 : ℕ) :

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+ a] = _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.lt_succ_sqrt (n : ℕ) :

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

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.sqrt_lt {m n : ℕ} :

nat.sqrt m < n ↔ m < n * n

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

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.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_eq (n : ℕ) :

nat.sqrt (n * n) = n

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