feat(algebra/order/floor): sub/super-additivity of floor/ceil/fract (#…

…17728)

src/algebra/order/floor.lean

@@ -321,6 +321,12 @@ by { convert ceil_add_nat ha 1, exact cast_one.symm }
 lemma ceil_lt_add_one (ha : 0 ≤ a) : (⌈a⌉₊ : α) < a + 1 :=
 lt_ceil.1 $ (nat.lt_succ_self _).trans_le (ceil_add_one ha).ge
 
+lemma ceil_add_le (a b : α) : ⌈a + b⌉₊ ≤ ⌈a⌉₊ + ⌈b⌉₊ :=
+begin
+  rw [ceil_le, nat.cast_add],
+  exact add_le_add (le_ceil _) (le_ceil _),
+end
+
 end linear_ordered_semiring
 
 section linear_ordered_ring
@@ -484,6 +490,20 @@ eq_of_forall_le_iff $ λ a, by rw [le_floor,
 lemma floor_add_one (a : α) : ⌊a + 1⌋ = ⌊a⌋ + 1 :=
 by { convert floor_add_int a 1, exact cast_one.symm }
 
+lemma le_floor_add (a b : α) : ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋ :=
+begin
+  rw [le_floor, int.cast_add],
+  exact add_le_add (floor_le _) (floor_le _),
+end
+
+lemma le_floor_add_floor (a b : α) : ⌊a + b⌋ - 1 ≤ ⌊a⌋ + ⌊b⌋ :=
+begin
+  rw [←sub_le_iff_le_add, le_floor, int.cast_sub, sub_le_comm, int.cast_sub, int.cast_one],
+  refine le_trans _ (sub_one_lt_floor _).le,
+  rw [sub_le_iff_le_add', ←add_sub_assoc, sub_le_sub_iff_right],
+  exact floor_le _,
+end
+
 @[simp] lemma floor_int_add (z : ℤ) (a : α) : ⌊↑z + a⌋ = z + ⌊a⌋ :=
 by simpa only [add_comm] using floor_add_int a z
 
@@ -551,6 +571,18 @@ by { rw fract, simp }
 @[simp] lemma fract_int_nat (n : ℕ) (a : α) : fract (↑n + a) = fract a :=
 by rw [add_comm, fract_add_nat]
 
+lemma fract_add_le (a b : α) : fract (a + b) ≤ fract a + fract b :=
+begin
+  rw [fract, fract, fract, sub_add_sub_comm, sub_le_sub_iff_left, ←int.cast_add, int.cast_le],
+  exact le_floor_add _ _,
+end
+
+lemma fract_add_fract_le (a b : α) : fract a + fract b ≤ fract (a + b) + 1 :=
+begin
+  rw [fract, fract, fract, sub_add_sub_comm, sub_add, sub_le_sub_iff_left],
+  exact_mod_cast le_floor_add_floor a b,
+end
+
 @[simp] lemma self_sub_fract (a : α) : a - fract a = ⌊a⌋ := sub_sub_cancel _ _
 
 @[simp] lemma fract_sub_self (a : α) : fract a - a = -⌊a⌋ := sub_sub_cancel_left _ _
@@ -772,6 +804,20 @@ by rw [eq_sub_iff_add_eq, ← ceil_add_one, sub_add_cancel]
 lemma ceil_lt_add_one (a : α) : (⌈a⌉ : α) < a + 1 :=
 by { rw [← lt_ceil, ← int.cast_one, ceil_add_int], apply lt_add_one }
 
+lemma ceil_add_le (a b : α) : ⌈a + b⌉ ≤ ⌈a⌉ + ⌈b⌉ :=
+begin
+  rw [ceil_le, int.cast_add],
+  exact add_le_add (le_ceil _) (le_ceil _),
+end
+
+lemma ceil_add_ceil_le (a b : α) : ⌈a⌉ + ⌈b⌉ ≤ ⌈a + b⌉ + 1 :=
+begin
+  rw [←le_sub_iff_add_le, ceil_le, int.cast_sub, int.cast_add, int.cast_one, le_sub_comm],
+  refine (ceil_lt_add_one _).le.trans _,
+  rw [le_sub_iff_add_le', ←add_assoc, add_le_add_iff_right],
+  exact le_ceil _,
+end
+
 @[simp] lemma ceil_pos : 0 < ⌈a⌉ ↔ 0 < a := by rw [lt_ceil, cast_zero]
 
 @[simp] lemma ceil_zero : ⌈(0 : α)⌉ = 0 := by rw [← cast_zero, ceil_int_cast]