feat: Flat triangles have aligned vertices (#7733)

In a normed torsor over a strictly convex space, if the triangle inequality `dist a c ≤ dist a b + dist b c` is an equality, then `b` lies between `a` and `c`.



Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Analysis/Convex/Between.lean

@@ -152,6 +152,9 @@ def Sbtw (x y z : P) : Prop :=
 
 variable {R}
 
+lemma mem_segment_iff_wbtw {x y z : V} : y ∈ segment R x z ↔ Wbtw R x y z := by
+  rw [Wbtw, affineSegment_eq_segment]
+
 theorem Wbtw.map {x y z : P} (h : Wbtw R x y z) (f : P →ᵃ[R] P') : Wbtw R (f x) (f y) (f z) := by
   rw [Wbtw, ← affineSegment_image]
   exact Set.mem_image_of_mem _ h

Mathlib/Analysis/Convex/Normed.lean

@@ -3,9 +3,11 @@ Copyright (c) 2020 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alexander Bentkamp, Yury Kudryashov
 -/
+import Mathlib.Analysis.Convex.Between
 import Mathlib.Analysis.Convex.Jensen
 import Mathlib.Analysis.Convex.Topology
 import Mathlib.Analysis.Normed.Group.Pointwise
+import Mathlib.Analysis.NormedSpace.AddTorsor
 import Mathlib.Analysis.NormedSpace.Ray
 
 #align_import analysis.convex.normed from "leanprover-community/mathlib"@"a63928c34ec358b5edcda2bf7513c50052a5230f"
@@ -26,13 +28,14 @@ We prove the following facts:
 -/
 
 
-variable {ι : Type*} {E : Type*}
+variable {ι : Type*} {E P : Type*}
 
 open Metric Set
 
 open Pointwise Convex
 
-variable [SeminormedAddCommGroup E] [NormedSpace ℝ E] {s t : Set E}
+variable [SeminormedAddCommGroup E] [NormedSpace ℝ E] [PseudoMetricSpace P] [NormedAddTorsor E P]
+variable {s t : Set E}
 
 /-- The norm on a real normed space is convex on any convex set. See also `Seminorm.convexOn`
 and `convexOn_univ_norm`. -/
@@ -130,10 +133,14 @@ instance (priority := 100) NormedSpace.instLocPathConnectedSpace : LocPathConnec
     (convex_ball x r).isPathConnected <| by simp [r_pos]
 #align normed_space.loc_path_connected NormedSpace.instLocPathConnectedSpace
 
-theorem dist_add_dist_of_mem_segment {x y z : E} (h : y ∈ [x -[ℝ] z]) :
+theorem Wbtw.dist_add_dist {x y z : P} (h : Wbtw ℝ x y z) :
     dist x y + dist y z = dist x z := by
-  simp only [dist_eq_norm, mem_segment_iff_sameRay] at *
-  simpa only [sub_add_sub_cancel', norm_sub_rev] using h.norm_add.symm
+  obtain ⟨a, ⟨ha₀, ha₁⟩, rfl⟩ := h
+  simp [abs_of_nonneg, ha₀, ha₁, sub_mul]
+
+theorem dist_add_dist_of_mem_segment {x y z : E} (h : y ∈ [x -[ℝ] z]) :
+    dist x y + dist y z = dist x z :=
+  (mem_segment_iff_wbtw.1 h).dist_add_dist
 #align dist_add_dist_of_mem_segment dist_add_dist_of_mem_segment
 
 /-- The set of vectors in the same ray as `x` is connected. -/

Mathlib/Analysis/Convex/StrictConvexBetween.lean

@@ -16,10 +16,15 @@ space.
 
 -/
 
+open Metric
+open scoped Convex
 
-variable {V P : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P]
+variable {V P : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
 
-variable [NormedAddTorsor V P] [StrictConvexSpace ℝ V]
+variable [StrictConvexSpace ℝ V]
+
+section PseudoMetricSpace
+variable [PseudoMetricSpace P] [NormedAddTorsor V P]
 
 theorem Sbtw.dist_lt_max_dist (p : P) {p₁ p₂ p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) :
     dist p₂ p < max (dist p₁ p) (dist p₃ p) := by
@@ -78,3 +83,78 @@ theorem Collinear.sbtw_of_dist_eq_of_dist_lt {p p₁ p₂ p₃ : P} {r : ℝ}
   · rintro rfl
     exact hp₂.ne hp₃
 #align collinear.sbtw_of_dist_eq_of_dist_lt Collinear.sbtw_of_dist_eq_of_dist_lt
+
+end PseudoMetricSpace
+
+section MetricSpace
+variable [MetricSpace P] [NormedAddTorsor V P] {a b c : P}
+
+/-- 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 a b + dist b c = dist a c ↔ Wbtw ℝ a b c := by
+  have :
+      dist (a -ᵥ a) (b -ᵥ a) + dist (b -ᵥ a) (c -ᵥ a) = dist (a -ᵥ a) (c -ᵥ a) ↔
+        b -ᵥ a ∈ segment ℝ (a -ᵥ a) (c -ᵥ a) := by
+    simp only [mem_segment_iff_sameRay, sameRay_iff_norm_add, dist_eq_norm', sub_add_sub_cancel',
+      eq_comm]
+  simp_rw [dist_vsub_cancel_right, ← affineSegment_eq_segment, ← affineSegment_vsub_const_image]
+    at this
+  rwa [(vsub_left_injective _).mem_set_image] at this
+#align dist_add_dist_eq_iff dist_add_dist_eq_iff
+
+end MetricSpace
+
+variable {E F PE PF : Type*} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E]
+  [NormedSpace ℝ F] [StrictConvexSpace ℝ E] [MetricSpace PE] [MetricSpace PF] [NormedAddTorsor E PE]
+  [NormedAddTorsor F PF] {r : ℝ} {f : PF → PE} {x y z : PE}
+
+lemma eq_lineMap_of_dist_eq_mul_of_dist_eq_mul (hxy : dist x y = r * dist x z)
+    (hyz : dist y z = (1 - r) * dist x z) : y = AffineMap.lineMap x z r := by
+  have : y -ᵥ x ∈ [(0 : E) -[ℝ] z -ᵥ x] := by
+    rw [mem_segment_iff_wbtw, ←dist_add_dist_eq_iff, dist_zero_left, dist_vsub_cancel_right,
+      ←dist_eq_norm_vsub', ←dist_eq_norm_vsub', hxy, hyz, ←add_mul, add_sub_cancel'_right, one_mul]
+  obtain rfl | hne := eq_or_ne x z
+  · obtain rfl : y = x := by simpa
+    simp
+  · rw [← dist_ne_zero] at hne
+    obtain ⟨a, b, _, hb, _, H⟩ := this
+    rw [smul_zero, zero_add] at H
+    have H' := congr_arg norm H
+    rw [norm_smul, Real.norm_of_nonneg hb, ← dist_eq_norm_vsub', ← dist_eq_norm_vsub', hxy,
+      mul_left_inj' hne] at H'
+    rw [AffineMap.lineMap_apply, ← H', H, vsub_vadd]
+#align eq_line_map_of_dist_eq_mul_of_dist_eq_mul eq_lineMap_of_dist_eq_mul_of_dist_eq_mul
+
+lemma eq_midpoint_of_dist_eq_half (hx : dist x y = dist x z / 2) (hy : dist y z = dist x z / 2) :
+    y = midpoint ℝ x z := by
+  apply eq_lineMap_of_dist_eq_mul_of_dist_eq_mul
+  · rwa [invOf_eq_inv, ← div_eq_inv_mul]
+  · rwa [invOf_eq_inv, ← one_div, sub_half, one_div, ← div_eq_inv_mul]
+#align eq_midpoint_of_dist_eq_half eq_midpoint_of_dist_eq_half
+
+namespace Isometry
+
+/-- An isometry of `NormedAddTorsor`s for real normed spaces, strictly convex in the case of the
+codomain, is an affine isometry.  Unlike Mazur-Ulam, this does not require the isometry to be
+surjective. -/
+noncomputable def affineIsometryOfStrictConvexSpace (hi : Isometry f) : PF →ᵃⁱ[ℝ] PE :=
+  { AffineMap.ofMapMidpoint f
+      (fun x y => by
+        apply eq_midpoint_of_dist_eq_half
+        · rw [hi.dist_eq, hi.dist_eq]
+          simp only [dist_left_midpoint, Real.norm_of_nonneg zero_le_two, div_eq_inv_mul]
+        · rw [hi.dist_eq, hi.dist_eq]
+          simp only [dist_midpoint_right, Real.norm_of_nonneg zero_le_two, div_eq_inv_mul])
+      hi.continuous with
+    norm_map := fun x => by simp [AffineMap.ofMapMidpoint, ← dist_eq_norm_vsub E, hi.dist_eq] }
+#align isometry.affine_isometry_of_strict_convex_space Isometry.affineIsometryOfStrictConvexSpace
+
+@[simp] lemma coe_affineIsometryOfStrictConvexSpace (hi : Isometry f) :
+    ⇑hi.affineIsometryOfStrictConvexSpace = f := rfl
+#align isometry.coe_affine_isometry_of_strict_convex_space Isometry.coe_affineIsometryOfStrictConvexSpace
+
+@[simp] lemma affineIsometryOfStrictConvexSpace_apply (hi : Isometry f) (p : PF) :
+    hi.affineIsometryOfStrictConvexSpace p = f p := rfl
+#align isometry.affine_isometry_of_strict_convex_space_apply Isometry.affineIsometryOfStrictConvexSpace_apply
+
+end Isometry

Mathlib/Analysis/Convex/StrictConvexSpace.lean

@@ -232,77 +232,8 @@ theorem not_sameRay_iff_abs_lt_norm_sub : ¬SameRay ℝ x y ↔ |‖x‖ - ‖y
   sameRay_iff_norm_sub.not.trans <| ne_comm.trans (abs_norm_sub_norm_le _ _).lt_iff_ne.symm
 #align not_same_ray_iff_abs_lt_norm_sub not_sameRay_iff_abs_lt_norm_sub
 
-/-- 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. -/
-theorem dist_add_dist_eq_iff : dist x y + dist y z = dist x z ↔ y ∈ [x -[ℝ] z] := by
-  simp only [mem_segment_iff_sameRay, sameRay_iff_norm_add, dist_eq_norm', sub_add_sub_cancel',
-    eq_comm]
-#align dist_add_dist_eq_iff dist_add_dist_eq_iff
-
 theorem norm_midpoint_lt_iff (h : ‖x‖ = ‖y‖) : ‖(1 / 2 : ℝ) • (x + y)‖ < ‖x‖ ↔ x ≠ y := by
   rw [norm_smul, Real.norm_of_nonneg (one_div_nonneg.2 zero_le_two), ← inv_eq_one_div, ←
     div_eq_inv_mul, div_lt_iff (zero_lt_two' ℝ), mul_two, ← not_sameRay_iff_of_norm_eq h,
     not_sameRay_iff_norm_add_lt, h]
 #align norm_midpoint_lt_iff norm_midpoint_lt_iff
-
-variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
-
-variable {PF : Type u} {PE : Type*} [MetricSpace PF] [MetricSpace PE]
-
-variable [NormedAddTorsor F PF] [NormedAddTorsor E PE]
-
-theorem eq_lineMap_of_dist_eq_mul_of_dist_eq_mul {x y z : PE} (hxy : dist x y = r * dist x z)
-    (hyz : dist y z = (1 - r) * dist x z) : y = AffineMap.lineMap x z r := by
-  have : y -ᵥ x ∈ [(0 : E) -[ℝ] z -ᵥ x] := by
-    rw [← dist_add_dist_eq_iff, dist_zero_left, dist_vsub_cancel_right, ← dist_eq_norm_vsub', ←
-      dist_eq_norm_vsub', hxy, hyz, ← add_mul, add_sub_cancel'_right, one_mul]
-  rcases eq_or_ne x z with (rfl | hne)
-  · obtain rfl : y = x := by simpa
-    simp
-  · rw [← dist_ne_zero] at hne
-    rcases this with ⟨a, b, _, hb, _, H⟩
-    rw [smul_zero, zero_add] at H
-    have H' := congr_arg norm H
-    rw [norm_smul, Real.norm_of_nonneg hb, ← dist_eq_norm_vsub', ← dist_eq_norm_vsub', hxy,
-      mul_left_inj' hne] at H'
-    rw [AffineMap.lineMap_apply, ← H', H, vsub_vadd]
-#align eq_line_map_of_dist_eq_mul_of_dist_eq_mul eq_lineMap_of_dist_eq_mul_of_dist_eq_mul
-
-theorem eq_midpoint_of_dist_eq_half {x y z : PE} (hx : dist x y = dist x z / 2)
-    (hy : dist y z = dist x z / 2) : y = midpoint ℝ x z := by
-  apply eq_lineMap_of_dist_eq_mul_of_dist_eq_mul
-  · rwa [invOf_eq_inv, ← div_eq_inv_mul]
-  · rwa [invOf_eq_inv, ← one_div, sub_half, one_div, ← div_eq_inv_mul]
-#align eq_midpoint_of_dist_eq_half eq_midpoint_of_dist_eq_half
-
-namespace Isometry
-
-/-- An isometry of `NormedAddTorsor`s for real normed spaces, strictly convex in the case of
-the codomain, is an affine isometry.  Unlike Mazur-Ulam, this does not require the isometry to
-be surjective. -/
-noncomputable def affineIsometryOfStrictConvexSpace {f : PF → PE} (hi : Isometry f) :
-    PF →ᵃⁱ[ℝ] PE :=
-  { AffineMap.ofMapMidpoint f
-      (fun x y => by
-        apply eq_midpoint_of_dist_eq_half
-        · rw [hi.dist_eq, hi.dist_eq]
-          simp only [dist_left_midpoint, Real.norm_of_nonneg zero_le_two, div_eq_inv_mul]
-        · rw [hi.dist_eq, hi.dist_eq]
-          simp only [dist_midpoint_right, Real.norm_of_nonneg zero_le_two, div_eq_inv_mul])
-      hi.continuous with
-    norm_map := fun x => by simp [AffineMap.ofMapMidpoint, ← dist_eq_norm_vsub E, hi.dist_eq] }
-#align isometry.affine_isometry_of_strict_convex_space Isometry.affineIsometryOfStrictConvexSpace
-
-@[simp]
-theorem coe_affineIsometryOfStrictConvexSpace {f : PF → PE} (hi : Isometry f) :
-    ⇑hi.affineIsometryOfStrictConvexSpace = f :=
-  rfl
-#align isometry.coe_affine_isometry_of_strict_convex_space Isometry.coe_affineIsometryOfStrictConvexSpace
-
-@[simp]
-theorem affineIsometryOfStrictConvexSpace_apply {f : PF → PE} (hi : Isometry f) (p : PF) :
-    hi.affineIsometryOfStrictConvexSpace p = f p :=
-  rfl
-#align isometry.affine_isometry_of_strict_convex_space_apply Isometry.affineIsometryOfStrictConvexSpace_apply
-
-end Isometry