difference of floors

Stream: maths

[Jakob von Raumer]

Any easier ways to get this? Or should I put this somewhere?

lemma floor_sub_floor_lt (r s : ℝ) : ↑⌊r⌋ - ↑⌊s⌋ < |r - s| + 1 :=
by calc ↑⌊r⌋ - ↑⌊s⌋ ≤ r - ↑⌊s⌋    : sub_le_sub_right (int.floor_le r) _
                ... < r - (s - 1) : by apply sub_lt_sub_left; simp
                ... = (r - s) + 1 : by rw [sub_add]
                ... ≤ |r - s| + 1 : add_le_add_right (le_abs_self (r - s)) _

lemma abs_floor_sub_floor_lt (r s : ℝ) : ↑|⌊r⌋ - ⌊s⌋| < | r - s | + 1 :=
begin
  rw [int.cast_abs, int.cast_sub, abs_sub_lt_iff], split,
  { apply floor_sub_floor_lt },
  { rw abs_sub_comm, apply floor_sub_floor_lt },
end

[Heather Macbeth]

This might be an #xy problem -- often when on paper I'd use the floor the Lean answer is to invoke the archimedean principle, or something ...

[Yaël Dillies]

I think you're just making it harder for yourself with this first calc block. Don't we have the sub version of docs#add_lt_add_of_le_of_lt?

[Yaël Dillies]

Also I suggest using docs#sub_lt_iff_lt_add to interleave rewriting and inequality steps one less time.

[Heather Macbeth]

lemma floor_sub_floor_lt (r s : ℝ) : ↑⌊r⌋ - ↑⌊s⌋ < |r - s| + 1 :=
by linarith [int.floor_le r, int.sub_one_lt_floor s, le_abs_self (r - s)]

[Jakob von Raumer]

Thanks for the suggestions :)

[Jakob von Raumer]

Heather Macbeth said:

This might be an #xy problem -- often when on paper I'd use the floor the Lean answer is to invoke the archimedean principle, or something ...

This is more for a program verification context, where we really need floor