## Stream: Is there code for X?

### Topic: Simple nat.sqrt lemmas

#### Adrián Doña Mateo (Nov 30 2020 at 18:43):

I couldn't find any of these in the library so I wrote them myself.

lemma sqrt_pred_lt (n : ℕ) (h : n ≠ 0) :
sqrt (n - 1) * sqrt (n - 1) < n := lt_of_le_of_lt (sqrt_le _) (pred_lt h)

lemma le_succ_sqrt_pred (n : ℕ) (h : n ≠ 0) :
n ≤ (sqrt (n - 1) + 1) * (sqrt (n - 1) + 1) := le_of_pred_lt (lt_succ_sqrt _)

/-- There are no perfect squares strictly between a² and (a+1)² -/
lemma no_middle_square {n a : ℕ} (hl : a * a < n) (hr : n < (a + 1) * (a + 1)):
¬ ∃ t, t * t = n :=
begin
rintro ⟨t, rfl⟩,
have : a < t, from nat.mul_self_lt_mul_self_iff.mpr hl,
have : t < a + 1, from nat.mul_self_lt_mul_self_iff.mpr hr,
linarith,
end


I was wondering if it would be good to add any them to data.nat.sqrt.
The last one is very useful for proving that a natural number is not a square.

Make a PR!

#### Yakov Pechersky (Nov 30 2020 at 18:55):

Some golfing to remove unnecessary n \ne 0 hypotheses. Do you really need to state it on the pred versions?

import data.nat.sqrt
import tactic.linarith

open nat

lemma sqrt_lt (n : ℕ) : sqrt n * sqrt n < n + 1 :=
lt_succ_iff.mpr (sqrt_le _)

lemma le_succ_sqrt (n : ℕ) : n + 1 ≤ (sqrt n + 1) * (sqrt n + 1) :=
le_of_pred_lt (lt_succ_sqrt _)

/-- There are no perfect squares strictly between a² and (a+1)² -/
lemma no_middle_square {n a : ℕ} (hl : a * a < n) (hr : n < (a + 1) * (a + 1)):
¬ ∃ t, t * t = n :=
begin
rintro ⟨t, rfl⟩,
have : a < t, from nat.mul_self_lt_mul_self_iff.mpr hl,
have : t < a + 1, from nat.mul_self_lt_mul_self_iff.mpr hr,
linarith,
end


#### Yakov Pechersky (Nov 30 2020 at 19:21):

Further golfing, no linarith dep, and no necessary hyps for the no_middle_square:

import data.nat.sqrt

open nat

lemma sqrt_lt (n : ℕ) : sqrt n * sqrt n < n + 1 :=
lt_succ_iff.mpr (sqrt_le _)

lemma le_succ_sqrt (n : ℕ) : n + 1 ≤ (sqrt n + 1) * (sqrt n + 1) :=
le_of_pred_lt (lt_succ_sqrt _)

lemma not_exists_between_succ (n : ℕ) : ¬ ∃ k, n < k ∧ k < n + 1 :=
not_exists.mpr (λ k, not_and.mpr (λ h H, absurd H (not_lt_of_le (lt_of_succ_le h))))

/-- There are no perfect squares strictly between n² and (n+1)² -/
lemma no_middle_square (n : ℕ) :
¬ ∃ t, n * n < t * t ∧ t * t < (n + 1) * (n + 1) :=
begin
rintro ⟨t, ht, ht'⟩,
rw ←nat.mul_self_lt_mul_self_iff at ht ht',
rcases eq_or_lt_of_le (le_of_lt_succ ht') with rfl|H,
{ exact absurd ht (lt_irrefl t) },
{ exact not_exists_between_succ t ⟨n, H, lt_succ_of_lt ht⟩ },
end


#### Eric Wieser (Nov 30 2020 at 19:50):

Constructively, it seems like it would be more useful to have that last lemma as a for all / or

#### Eric Wieser (Nov 30 2020 at 19:50):

The previous lemma, with hypotheses, looks easier to work with

#### Yakov Pechersky (Nov 30 2020 at 20:23):

lemma no_middle_square' {n t : ℕ} (h : n * n < t * t) :
(n + 1) * (n + 1) ≤ t * t :=
nat.mul_self_le_mul_self (succ_le_of_lt (nat.mul_self_lt_mul_self_iff.mpr h))


Last updated: May 17 2021 at 16:26 UTC