feat(analysis/convex/strict_convex_space): Ray characterization of `∥…

…x - y∥` (#13293)

`∥x - y∥ = |∥x∥ - ∥y∥|` if and only if `x` and `y` are on the same ray.

src/analysis/complex/arg.lean

@@ -24,25 +24,32 @@ the usual way this is considered.
 
 variables {x y : ℂ}
 
-lemma complex.same_ray_iff : same_ray ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg :=
+namespace complex
+
+lemma same_ray_iff : same_ray ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg :=
 begin
   rcases eq_or_ne x 0 with rfl | hx,
   { simp },
   rcases eq_or_ne y 0 with rfl | hy,
   { simp },
-  simp only [hx, hy, false_or, same_ray_iff_norm_smul_eq, complex.arg_eq_arg_iff hx hy],
+  simp only [hx, hy, false_or, same_ray_iff_norm_smul_eq, arg_eq_arg_iff hx hy],
   field_simp [hx, hy],
   rw [mul_comm, eq_comm]
 end
 
-lemma complex.abs_add_eq_iff : (x + y).abs = x.abs + y.abs ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg :=
-same_ray_iff_norm_add.symm.trans complex.same_ray_iff
+lemma abs_add_eq_iff : (x + y).abs = x.abs + y.abs ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg :=
+same_ray_iff_norm_add.symm.trans same_ray_iff
+
+lemma abs_sub_eq_iff : (x - y).abs = |x.abs - y.abs| ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg :=
+same_ray_iff_norm_sub.symm.trans same_ray_iff
+
+lemma same_ray_of_arg_eq (h : x.arg = y.arg) : same_ray ℝ x y :=
+same_ray_iff.mpr $ or.inr $ or.inr h
 
-lemma complex.same_ray_of_arg_eq (h : x.arg = y.arg) : same_ray ℝ x y :=
-complex.same_ray_iff.mpr $ or.inr $ or.inr h
+lemma abs_add_eq (h : x.arg = y.arg) : (x + y).abs = x.abs + y.abs :=
+(same_ray_of_arg_eq h).norm_add
 
-lemma complex.abs_add_eq (h : x.arg = y.arg) : (x + y).abs = x.abs + y.abs :=
-(complex.same_ray_of_arg_eq h).norm_add
+lemma abs_sub_eq (h : x.arg = y.arg) : (x - y).abs = ∥x.abs - y.abs∥ :=
+(same_ray_of_arg_eq h).norm_sub
 
-lemma complex.abs_sub_eq (h : x.arg = y.arg) : (x - y).abs = ∥x.abs - y.abs∥ :=
-(complex.same_ray_of_arg_eq h).norm_sub
+end complex

src/analysis/convex/strict_convex_space.lean

@@ -151,6 +151,19 @@ begin
     real.norm_of_nonneg (inv_pos.2 hxy).le, ← div_eq_inv_mul, div_lt_one hxy] at this
 end
 
+lemma lt_norm_sub_of_not_same_ray (h : ¬same_ray ℝ x y) : ∥x∥ - ∥y∥ < ∥x - y∥ :=
+begin
+  nth_rewrite 0 ←sub_add_cancel x y at ⊢ h,
+  exact sub_lt_iff_lt_add.2 (norm_add_lt_of_not_same_ray $ λ H', h $ H'.add_left same_ray.rfl),
+end
+
+lemma abs_lt_norm_sub_of_not_same_ray (h : ¬same_ray ℝ x y) : |∥x∥ - ∥y∥| < ∥x - y∥ :=
+begin
+  refine abs_sub_lt_iff.2 ⟨lt_norm_sub_of_not_same_ray h, _⟩,
+  rw norm_sub_rev,
+  exact lt_norm_sub_of_not_same_ray (mt same_ray.symm h),
+end
+
 /-- In a strictly convex space, two vectors `x`, `y` are in the same ray if and only if the triangle
 inequality for `x` and `y` becomes an equality. -/
 lemma same_ray_iff_norm_add : same_ray ℝ x y ↔ ∥x + y∥ = ∥x∥ + ∥y∥ :=
@@ -161,6 +174,12 @@ triangle inequality for `x` and `y` is strict. -/
 lemma not_same_ray_iff_norm_add_lt : ¬ same_ray ℝ x y ↔ ∥x + y∥ < ∥x∥ + ∥y∥ :=
 same_ray_iff_norm_add.not.trans (norm_add_le _ _).lt_iff_ne.symm
 
+lemma same_ray_iff_norm_sub : same_ray ℝ x y ↔ ∥x - y∥ = |∥x∥ - ∥y∥| :=
+⟨same_ray.norm_sub, λ h, not_not.1 $ λ h', (abs_lt_norm_sub_of_not_same_ray h').ne' h⟩
+
+lemma not_same_ray_iff_abs_lt_norm_sub : ¬ same_ray ℝ x y ↔ |∥x∥ - ∥y∥| < ∥x - y∥ :=
+same_ray_iff_norm_sub.not.trans $ ne_comm.trans (abs_norm_sub_norm_le _ _).lt_iff_ne.symm
+
 /-- In a strictly convex space, the triangle inequality turns into an equality if and only if the
 middle point belongs to the segment joining two other points. -/
 lemma dist_add_dist_eq_iff : dist x y + dist y z = dist x z ↔ y ∈ [x -[ℝ] z] :=