refactor(linear_algebra/ray): redefine same_ray to allow zero vectors (#12618)

In a strictly convex space, the new definition is equivalent to the fact that the triangle inequality becomes an equality. The old definition was only used for nonzero vectors in `mathlib`. Also make the definition of `ray_vector` semireducible so that `ray_vector.setoid` can be an instance.

Author: urkud

src/analysis/convex/basic.lean

@@ -7,6 +7,7 @@ import algebra.order.invertible
 import algebra.order.module
 import linear_algebra.affine_space.midpoint
 import linear_algebra.affine_space.affine_subspace
+import linear_algebra.ray
 
 /-!
 # Convex sets and functions in vector spaces
@@ -58,6 +59,15 @@ def open_segment (x y : E) : set E :=
 
 localized "notation `[` x ` -[` 𝕜 `] ` y `]` := segment 𝕜 x y" in convex
 
+lemma segment_eq_image₂ (x y : E) :
+  [x -[𝕜] y] = (λ p : 𝕜 × 𝕜, p.1 • x + p.2 • y) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} :=
+by simp only [segment, image, prod.exists, mem_set_of_eq, exists_prop, and_assoc]
+
+lemma open_segment_eq_image₂ (x y : E) :
+  open_segment 𝕜 x y =
+    (λ p : 𝕜 × 𝕜, p.1 • x + p.2 • y) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} :=
+by simp only [open_segment, image, prod.exists, mem_set_of_eq, exists_prop, and_assoc]
+
 lemma segment_symm (x y : E) : [x -[𝕜] y] = [y -[𝕜] x] :=
 set.ext $ λ z,
 ⟨λ ⟨a, b, ha, hb, hab, H⟩, ⟨b, a, hb, ha, (add_comm _ _).trans hab, (add_comm _ _).trans H⟩,
@@ -101,7 +111,7 @@ end mul_action_with_zero
 section module
 variables (𝕜) [module 𝕜 E]
 
-lemma segment_same (x : E) : [x -[𝕜] x] = {x} :=
+@[simp] lemma segment_same (x : E) : [x -[𝕜] x] = {x} :=
 set.ext $ λ z, ⟨λ ⟨a, b, ha, hb, hab, hz⟩,
   by simpa only [(add_smul _ _ _).symm, mem_singleton_iff, hab, one_smul, eq_comm] using hz,
   λ h, mem_singleton_iff.1 h ▸ left_mem_segment 𝕜 z z⟩
@@ -177,15 +187,6 @@ set.ext $ λ z,
     ⟨b, ⟨hb, hab ▸ lt_add_of_pos_left _ ha⟩, hab ▸ hz ▸ by simp only [add_sub_cancel]⟩,
     λ ⟨θ, ⟨hθ₀, hθ₁⟩, hz⟩, ⟨1 - θ, θ, sub_pos.2 hθ₁, hθ₀, sub_add_cancel _ _, hz⟩⟩
 
-lemma segment_eq_image₂ (x y : E) :
-  [x -[𝕜] y] = (λ p : 𝕜 × 𝕜, p.1 • x + p.2 • y) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} :=
-by simp only [segment, image, prod.exists, mem_set_of_eq, exists_prop, and_assoc]
-
-lemma open_segment_eq_image₂ (x y : E) :
-  open_segment 𝕜 x y =
-    (λ p : 𝕜 × 𝕜, p.1 • x + p.2 • y) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} :=
-by simp only [open_segment, image, prod.exists, mem_set_of_eq, exists_prop, and_assoc]
-
 lemma segment_eq_image' (x y : E) :
   [x -[𝕜] y] = (λ (θ : 𝕜), x + θ • (y - x)) '' Icc (0 : 𝕜) 1 :=
 by { convert segment_eq_image 𝕜 x y, ext θ, simp only [smul_sub, sub_smul, one_smul], abel }
@@ -242,6 +243,15 @@ open_segment_translate_preimage 𝕜 a b c ▸ image_preimage_eq _ $ add_left_su
 end add_comm_group
 end ordered_ring
 
+lemma same_ray_of_mem_segment [ordered_comm_ring 𝕜] [add_comm_group E] [module 𝕜 E]
+  {x y z : E} (h : x ∈ [y -[𝕜] z]) : same_ray 𝕜 (x - y) (z - x) :=
+begin
+  rw segment_eq_image' at h,
+  rcases h with ⟨θ, ⟨hθ₀, hθ₁⟩, rfl⟩,
+  simpa only [add_sub_cancel', ← sub_sub, sub_smul, one_smul]
+    using (same_ray_nonneg_smul_left (z - y) hθ₀).nonneg_smul_right (sub_nonneg.2 hθ₁)
+end
+
 section linear_ordered_ring
 variables [linear_ordered_ring 𝕜]
 
@@ -278,6 +288,17 @@ variables [linear_ordered_field 𝕜]
 section add_comm_group
 variables [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F]
 
+lemma mem_segment_iff_same_ray {x y z : E} :
+  x ∈ [y -[𝕜] z] ↔ same_ray 𝕜 (x - y) (z - x) :=
+begin
+  refine ⟨same_ray_of_mem_segment, λ h, _⟩,
+  rcases h.exists_eq_smul_add with ⟨a, b, ha, hb, hab, hxy, hzx⟩,
+  rw [add_comm, sub_add_sub_cancel] at hxy hzx,
+  rw [← mem_segment_translate _ (-x), neg_add_self],
+  refine ⟨b, a, hb, ha, add_comm a b ▸ hab, _⟩,
+  rw [← sub_eq_neg_add, ← neg_sub, hxy, ← sub_eq_neg_add, hzx, smul_neg, smul_comm, neg_add_self]
+end
+
 lemma mem_segment_iff_div {x y z : E} : x ∈ [y -[𝕜] z] ↔
   ∃ a b : 𝕜, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x :=
 begin

src/analysis/normed_space/ray.lean

@@ -0,0 +1,80 @@
+/-
+Copyright (c) 2022 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import linear_algebra.ray
+import analysis.normed_space.basic
+
+/-!
+# Rays in a real normed vector space
+
+In this file we prove some lemmas about the `same_ray` predicate in case of a real normed space. In
+this case, for two vectors `x y` in the same ray, the norm of their sum is equal to the sum of their
+norms and `∥y∥ • x = ∥x∥ • y`.
+-/
+
+variables {E : Type*} [semi_normed_group E] [normed_space ℝ E]
+  {F : Type*} [normed_group F] [normed_space ℝ F]
+
+namespace same_ray
+
+variables {x y : E}
+
+/-- If `x` and `y` are on the same ray, then the triangle inequality becomes the equality: the norm
+of `x + y` is the sum of the norms of `x` and `y`. The converse is true for a strictly convex
+space. -/
+lemma norm_add (h : same_ray ℝ x y) : ∥x + y∥ = ∥x∥ + ∥y∥ :=
+begin
+  rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩,
+  rw [← add_smul, norm_smul_of_nonneg (add_nonneg ha hb), norm_smul_of_nonneg ha,
+    norm_smul_of_nonneg hb, add_mul]
+end
+
+lemma norm_sub (h : same_ray ℝ x y) : ∥x - y∥ = |∥x∥ - ∥y∥| :=
+begin
+  rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩,
+  wlog hab : b ≤ a := le_total b a using [a b, b a] tactic.skip,
+  { rw ← sub_nonneg at hab,
+    rw [← sub_smul, norm_smul_of_nonneg hab, norm_smul_of_nonneg ha,
+      norm_smul_of_nonneg hb, ← sub_mul, abs_of_nonneg (mul_nonneg hab (norm_nonneg _))] },
+  { intros ha hb hab,
+    rw [norm_sub_rev, this hb ha hab.symm, abs_sub_comm] }
+end
+
+lemma norm_smul_eq (h : same_ray ℝ x y) : ∥x∥ • y = ∥y∥ • x :=
+begin
+  rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩,
+  simp only [norm_smul_of_nonneg, *, mul_smul, smul_comm (∥u∥)],
+  apply smul_comm
+end
+
+end same_ray
+
+lemma same_ray_iff_norm_smul_eq {x y : F} :
+  same_ray ℝ x y ↔ ∥x∥ • y = ∥y∥ • x :=
+⟨same_ray.norm_smul_eq, λ h, or_iff_not_imp_left.2 $ λ hx, or_iff_not_imp_left.2 $ λ hy,
+  ⟨∥y∥, ∥x∥, norm_pos_iff.2 hy, norm_pos_iff.2 hx, h.symm⟩⟩
+
+/-- Two nonzero vectors `x y` in a real normed space are on the same ray if and only if the unit
+vectors `∥x∥⁻¹ • x` and `∥y∥⁻¹ • y` are equal. -/
+lemma same_ray_iff_inv_norm_smul_eq_of_ne {x y : F} (hx : x ≠ 0) (hy : y ≠ 0) :
+  same_ray ℝ x y ↔ ∥x∥⁻¹ • x = ∥y∥⁻¹ • y :=
+begin
+  have : ∥x∥⁻¹ * ∥y∥⁻¹ ≠ 0, by simp *,
+  rw [same_ray_iff_norm_smul_eq, ← smul_right_inj this]; try { apply_instance },
+  rw [smul_comm, mul_smul, mul_smul, smul_inv_smul₀, inv_smul_smul₀, eq_comm],
+  exacts [norm_ne_zero_iff.2 hy, norm_ne_zero_iff.2 hx]
+end
+
+alias same_ray_iff_inv_norm_smul_eq_of_ne ↔ same_ray.inv_norm_smul_eq _
+
+/-- Two vectors `x y` in a real normed space are on the ray if and only if one of them is zero or
+the unit vectors `∥x∥⁻¹ • x` and `∥y∥⁻¹ • y` are equal. -/
+lemma same_ray_iff_inv_norm_smul_eq {x y : F} :
+  same_ray ℝ x y ↔ x = 0 ∨ y = 0 ∨ ∥x∥⁻¹ • x = ∥y∥⁻¹ • y :=
+begin
+  rcases eq_or_ne x 0 with rfl|hx, { simp [same_ray.zero_left] },
+  rcases eq_or_ne y 0 with rfl|hy, { simp [same_ray.zero_right] },
+  simp only [same_ray_iff_inv_norm_smul_eq_of_ne hx hy, *, false_or]
+end

src/linear_algebra/orientation.lean

@@ -42,40 +42,36 @@ variables (M : Type*) [add_comm_monoid M] [module R M]
 variables {N : Type*} [add_comm_monoid N] [module R N]
 variables (ι : Type*) [decidable_eq ι]
 
-local attribute [instance] ray_vector.same_ray_setoid
-
 /-- An orientation of a module, intended to be used when `ι` is a `fintype` with the same
 cardinality as a basis. -/
-abbreviation orientation [nontrivial R] := module.ray R (alternating_map R M R ι)
+abbreviation orientation := module.ray R (alternating_map R M R ι)
 
 /-- A type class fixing an orientation of a module. -/
-class module.oriented [nontrivial R] :=
+class module.oriented :=
 (positive_orientation : orientation R M ι)
 
 variables {R M}
 
 /-- An equivalence between modules implies an equivalence between orientations. -/
-def orientation.map [nontrivial R] (e : M ≃ₗ[R] N) : orientation R M ι ≃ orientation R N ι :=
+def orientation.map (e : M ≃ₗ[R] N) : orientation R M ι ≃ orientation R N ι :=
 module.ray.map $ alternating_map.dom_lcongr R R ι R e
 
-@[simp] lemma orientation.map_apply [nontrivial R] (e : M ≃ₗ[R] N) (v : alternating_map R M R ι)
+@[simp] lemma orientation.map_apply (e : M ≃ₗ[R] N) (v : alternating_map R M R ι)
   (hv : v ≠ 0) :
   orientation.map ι e (ray_of_ne_zero _ v hv) = ray_of_ne_zero _ (v.comp_linear_map e.symm)
       (mt (v.comp_linear_equiv_eq_zero_iff e.symm).mp hv) := rfl
 
-@[simp] lemma orientation.map_refl [nontrivial R] :
+@[simp] lemma orientation.map_refl :
   (orientation.map ι $ linear_equiv.refl R M) = equiv.refl _ :=
 by rw [orientation.map, alternating_map.dom_lcongr_refl, module.ray.map_refl]
 
-@[simp] lemma orientation.map_symm [nontrivial R] (e : M ≃ₗ[R] N) :
+@[simp] lemma orientation.map_symm (e : M ≃ₗ[R] N) :
   (orientation.map ι e).symm = orientation.map ι e.symm := rfl
 
 end ordered_comm_semiring
 
 section ordered_comm_ring
 
-local attribute [instance] ray_vector.same_ray_setoid
-
 variables {R : Type*} [ordered_comm_ring R]
 variables {M N : Type*} [add_comm_group M] [add_comm_group N] [module R M] [module R N]
 
@@ -93,7 +89,7 @@ by simp_rw [basis.orientation, orientation.map_apply, basis.det_map']
 
 /-- The value of `orientation.map` when the index type has the cardinality of a basis, in terms
 of `f.det`. -/
-lemma map_orientation_eq_det_inv_smul [nontrivial R] [is_domain R] (e : basis ι R M)
+lemma map_orientation_eq_det_inv_smul [is_domain R] (e : basis ι R M)
   (x : orientation R M ι) (f : M ≃ₗ[R] M) : orientation.map ι f x = (f.det)⁻¹ • x :=
 begin
   induction x using module.ray.ind with g hg,
@@ -132,19 +128,19 @@ variables [fintype ι]
 with respect to the other is positive. -/
 lemma orientation_eq_iff_det_pos (e₁ e₂ : basis ι R M) :
   e₁.orientation = e₂.orientation ↔ 0 < e₁.det e₂ :=
-by rw [basis.orientation, basis.orientation, ray_eq_iff,
-       e₁.det.eq_smul_basis_det e₂, alternating_map.smul_apply, basis.det_self, smul_eq_mul,
-       mul_one, same_ray_smul_left_iff e₂.det_ne_zero (_ : R)]
+calc e₁.orientation = e₂.orientation ↔ same_ray R e₁.det e₂.det : ray_eq_iff _ _
+... ↔ same_ray R (e₁.det e₂ • e₂.det) e₂.det : by rw [← e₁.det.eq_smul_basis_det e₂]
+... ↔ 0 < e₁.det e₂ : same_ray_smul_left_iff_of_ne e₂.det_ne_zero (e₁.is_unit_det e₂).ne_zero
 
 /-- Given a basis, any orientation equals the orientation given by that basis or its negation. -/
 lemma orientation_eq_or_eq_neg (e : basis ι R M) (x : orientation R M ι) :
   x = e.orientation ∨ x = -e.orientation :=
 begin
   induction x using module.ray.ind with x hx,
-  rw [basis.orientation, ray_eq_iff, ←ray_neg, ray_eq_iff, x.eq_smul_basis_det e,
-    same_ray_neg_smul_left_iff e.det_ne_zero (_ : R), same_ray_smul_left_iff e.det_ne_zero (_ : R),
-    lt_or_lt_iff_ne, ne_comm, alternating_map.map_basis_ne_zero_iff],
-  exact hx
+  rw ← x.map_basis_ne_zero_iff e at hx,
+  rwa [basis.orientation, ray_eq_iff, neg_ray_of_ne_zero, ray_eq_iff, x.eq_smul_basis_det e,
+    same_ray_neg_smul_left_iff_of_ne e.det_ne_zero hx,
+    same_ray_smul_left_iff_of_ne e.det_ne_zero hx, lt_or_lt_iff_ne, ne_comm]
 end
 
 /-- Given a basis, an orientation equals the negation of that given by that basis if and only