feat(analysis.normed_space.lattice_ordered_group): Add `two_inf_sub_t…

…wo_inf_le`, `two_sup_sub_two_sup_le` and supporting lemmas (#10514)

feat(analysis.normed_space.lattice_ordered_group): Add `two_inf_sub_two_inf_le`, `two_sup_sub_two_sup_le` and supporting lemmas



Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>

src/algebra/lattice_ordered_group.lean

@@ -326,15 +326,15 @@ begin
 end
 
 -- 2•(a ⊔ b) = a + b + |b - a|
-@[to_additive]
+@[to_additive two_sup_eq_add_add_abs_sub]
 lemma sup_sq_eq_mul_mul_abs_div [covariant_class α α (*) (≤)] (a b : α) :
   (a ⊔ b)^2 = a * b * |b / a| :=
 by rw [← inf_mul_sup a b, ← sup_div_inf_eq_abs_div, div_eq_mul_inv, ← mul_assoc, mul_comm,
     mul_assoc, ← pow_two, inv_mul_cancel_left]
 
 -- 2•(a ⊓ b) = a + b - |b - a|
-@[to_additive]
-lemma two_inf_eq_mul_div_abs_div [covariant_class α α (*) (≤)] (a b : α) :
+@[to_additive two_inf_eq_add_sub_abs_sub]
+lemma inf_sq_eq_mul_div_abs_div [covariant_class α α (*) (≤)] (a b : α) :
   (a ⊓ b)^2 = a * b / |b / a| :=
 by rw [← inf_mul_sup a b, ← sup_div_inf_eq_abs_div, div_eq_mul_inv, div_eq_mul_inv,
     mul_inv_rev, inv_inv, mul_assoc, mul_inv_cancel_comm_assoc, ← pow_two]
@@ -476,4 +476,31 @@ begin
     exact mul_le_mul' (inv_le_abs _) (inv_le_abs _), }
 end
 
+-- |a - b| = |b - a|
+@[to_additive]
+lemma abs_inv_comm (a b : α) : |a/b| = |b/a| :=
+begin
+  unfold has_abs.abs,
+  rw [inv_div' a b, ← inv_inv (a / b), inv_div', sup_comm],
+end
+
+-- | |a| - |b| | ≤ |a - b|
+@[to_additive]
+lemma abs_abs_div_abs_le [covariant_class α α (*) (≤)] (a b : α) : | |a| / |b| | ≤ |a / b| :=
+begin
+  unfold has_abs.abs,
+  rw sup_le_iff,
+  split,
+  { apply div_le_iff_le_mul.2,
+    convert mabs_mul_le (a/b) b,
+    { rw div_mul_cancel', },
+    { rw div_mul_cancel', },
+    { exact covariant_swap_mul_le_of_covariant_mul_le α, } },
+  { rw [div_eq_mul_inv, mul_inv_rev, inv_inv, mul_inv_le_iff_le_mul, ← abs_eq_sup_inv (a / b),
+      abs_inv_comm],
+    convert  mabs_mul_le (b/a) a,
+    { rw div_mul_cancel', },
+    {rw div_mul_cancel', } },
+end
+
 end lattice_ordered_comm_group

src/analysis/normed_space/lattice_ordered_group.lean

@@ -135,3 +135,45 @@ Let `α` be a normed lattice ordered group. Then `α` is a topological lattice i
 @[priority 100] -- see Note [lower instance priority]
 instance normed_lattice_add_comm_group_topological_lattice : topological_lattice α :=
 topological_lattice.mk
+
+lemma norm_abs_sub_abs (a b : α) :
+  ∥ |a| - |b| ∥ ≤ ∥a-b∥ :=
+solid (lattice_ordered_comm_group.abs_abs_sub_abs_le _ _)
+
+lemma norm_two_inf_sub_two_inf_le (a b c d : α) :
+  ∥2•(a⊓b)-2•(c⊓d)∥ ≤ 2*∥a - c∥ + 2*∥b - d∥ :=
+calc ∥2•(a⊓b) - 2•(c⊓d)∥ = ∥(a + b - |b - a|) - (c + d - |d - c|)∥ :
+    by rw [lattice_ordered_comm_group.two_inf_eq_add_sub_abs_sub,
+      lattice_ordered_comm_group.two_inf_eq_add_sub_abs_sub]
+  ... = ∥(a + b - |b - a|) - c - d + |d - c|∥      : by abel
+  ... = ∥(a - c + (b - d))  + (|d - c| - |b - a|)∥ : by abel
+  ... ≤ ∥a - c + (b - d)∥ + ∥|d - c| - |b - a|∥    :
+    by apply norm_add_le (a - c + (b - d)) (|d - c| - |b - a|)
+  ... ≤ (∥a - c∥ + ∥b - d∥) + ∥|d - c| - |b - a|∥   : by exact add_le_add_right (norm_add_le _ _) _
+  ... ≤ (∥a - c∥ + ∥b - d∥) + ∥ d - c - (b - a) ∥   :
+    by exact add_le_add_left (norm_abs_sub_abs _ _) _
+  ... = (∥a - c∥ + ∥b - d∥) + ∥ a - c - (b - d) ∥ :
+    by { rw [sub_sub_assoc_swap, sub_sub_assoc_swap, add_comm (a-c), ← add_sub_assoc], simp, abel, }
+  ... ≤ (∥a - c∥ + ∥b - d∥) + (∥ a - c ∥ + ∥ b - d ∥) :
+    by apply add_le_add_left (norm_sub_le (a-c) (b-d) )
+  ... = 2*∥a - c∥ + 2*∥b - d∥ :
+    by { ring, }
+
+lemma norm_two_sup_sub_two_sup_le (a b c d : α) :
+  ∥2•(a⊔b)-2•(c⊔d)∥ ≤ 2*∥a - c∥ + 2*∥b - d∥ :=
+calc ∥2•(a⊔b) - 2•(c⊔d)∥ = ∥(a + b + |b - a|) - (c + d + |d - c|)∥ :
+    by rw [lattice_ordered_comm_group.two_sup_eq_add_add_abs_sub,
+      lattice_ordered_comm_group.two_sup_eq_add_add_abs_sub]
+  ... = ∥(a + b + |b - a|) - c - d - |d - c|∥      : by abel
+  ... = ∥(a - c + (b - d))  + (|b - a| - |d - c|)∥ : by abel
+  ... ≤ ∥a - c + (b - d)∥ + ∥|b - a| - |d - c|∥    :
+    by apply norm_add_le (a - c + (b - d)) (|b - a| - |d - c|)
+  ... ≤ (∥a - c∥ + ∥b - d∥) + ∥|b - a| - |d - c|∥   : by exact add_le_add_right (norm_add_le _ _) _
+  ... ≤ (∥a - c∥ + ∥b - d∥) + ∥ b - a - (d - c) ∥   :
+    by exact add_le_add_left (norm_abs_sub_abs _ _) _
+  ... = (∥a - c∥ + ∥b - d∥) + ∥ b - d - (a - c) ∥ :
+    by { rw [sub_sub_assoc_swap, sub_sub_assoc_swap, add_comm (b-d), ← add_sub_assoc], simp, abel, }
+  ... ≤ (∥a - c∥ + ∥b - d∥) + (∥ b - d ∥ + ∥ a - c ∥) :
+    by apply add_le_add_left (norm_sub_le (b-d) (a-c)  )
+  ... = 2*∥a - c∥ + 2*∥b - d∥ :
+    by { ring, }