feat: port Analysis.Convex.StrictConvexBetween (#4220)

Mathlib.lean

@@ -412,6 +412,7 @@ import Mathlib.Analysis.Convex.Slope
 import Mathlib.Analysis.Convex.Star
 import Mathlib.Analysis.Convex.StoneSeparation
 import Mathlib.Analysis.Convex.Strict
+import Mathlib.Analysis.Convex.StrictConvexBetween
 import Mathlib.Analysis.Convex.StrictConvexSpace
 import Mathlib.Analysis.Convex.Topology
 import Mathlib.Analysis.Convex.Uniform

Mathlib/Analysis/Convex/StrictConvexBetween.lean

@@ -0,0 +1,83 @@
+/-
+Copyright (c) 2022 Joseph Myers. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Myers
+
+! This file was ported from Lean 3 source module analysis.convex.strict_convex_between
+! leanprover-community/mathlib commit e1730698f86560a342271c0471e4cb72d021aabf
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Analysis.Convex.Between
+import Mathlib.Analysis.Convex.StrictConvexSpace
+
+/-!
+# Betweenness in affine spaces for strictly convex spaces
+
+This file proves results about betweenness for points in an affine space for a strictly convex
+space.
+
+-/
+
+
+variable {V P : Type _} [NormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P]
+
+variable [NormedAddTorsor V P] [StrictConvexSpace ℝ V]
+
+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
+  have hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p := by simpa using h.left_ne_right
+  rw [Sbtw, ← wbtw_vsub_const_iff p, Wbtw, affineSegment_eq_segment, ← insert_endpoints_openSegment,
+    Set.mem_insert_iff, Set.mem_insert_iff] at h
+  rcases h with ⟨h | h | h, hp₂p₁, hp₂p₃⟩
+  · rw [vsub_left_cancel_iff] at h
+    exact False.elim (hp₂p₁ h)
+  · rw [vsub_left_cancel_iff] at h
+    exact False.elim (hp₂p₃ h)
+  · rw [openSegment_eq_image, Set.mem_image] at h
+    rcases h with ⟨r, ⟨hr0, hr1⟩, hr⟩
+    simp_rw [@dist_eq_norm_vsub V, ← hr]
+    exact
+      norm_combo_lt_of_ne (le_max_left _ _) (le_max_right _ _) hp₁p₃ (sub_pos.2 hr1) hr0 (by abel)
+#align sbtw.dist_lt_max_dist Sbtw.dist_lt_max_dist
+
+theorem Wbtw.dist_le_max_dist (p : P) {p₁ p₂ p₃ : P} (h : Wbtw ℝ p₁ p₂ p₃) :
+    dist p₂ p ≤ max (dist p₁ p) (dist p₃ p) := by
+  by_cases hp₁ : p₂ = p₁; · simp [hp₁]
+  by_cases hp₃ : p₂ = p₃; · simp [hp₃]
+  have hs : Sbtw ℝ p₁ p₂ p₃ := ⟨h, hp₁, hp₃⟩
+  exact (hs.dist_lt_max_dist _).le
+#align wbtw.dist_le_max_dist Wbtw.dist_le_max_dist
+
+/-- Given three collinear points, two (not equal) with distance `r` from `p` and one with
+distance at most `r` from `p`, the third point is weakly between the other two points. -/
+theorem Collinear.wbtw_of_dist_eq_of_dist_le {p p₁ p₂ p₃ : P} {r : ℝ}
+    (h : Collinear ℝ ({p₁, p₂, p₃} : Set P)) (hp₁ : dist p₁ p = r) (hp₂ : dist p₂ p ≤ r)
+    (hp₃ : dist p₃ p = r) (hp₁p₃ : p₁ ≠ p₃) : Wbtw ℝ p₁ p₂ p₃ := by
+  rcases h.wbtw_or_wbtw_or_wbtw with (hw | hw | hw)
+  · exact hw
+  · by_cases hp₃p₂ : p₃ = p₂
+    · simp [hp₃p₂]
+    have hs : Sbtw ℝ p₂ p₃ p₁ := ⟨hw, hp₃p₂, hp₁p₃.symm⟩
+    have hs' := hs.dist_lt_max_dist p
+    rw [hp₁, hp₃, lt_max_iff, lt_self_iff_false, or_false_iff] at hs'
+    exact False.elim (hp₂.not_lt hs')
+  · by_cases hp₁p₂ : p₁ = p₂
+    · simp [hp₁p₂]
+    have hs : Sbtw ℝ p₃ p₁ p₂ := ⟨hw, hp₁p₃, hp₁p₂⟩
+    have hs' := hs.dist_lt_max_dist p
+    rw [hp₁, hp₃, lt_max_iff, lt_self_iff_false, false_or_iff] at hs'
+    exact False.elim (hp₂.not_lt hs')
+#align collinear.wbtw_of_dist_eq_of_dist_le Collinear.wbtw_of_dist_eq_of_dist_le
+
+/-- Given three collinear points, two (not equal) with distance `r` from `p` and one with
+distance less than `r` from `p`, the third point is strictly between the other two points. -/
+theorem Collinear.sbtw_of_dist_eq_of_dist_lt {p p₁ p₂ p₃ : P} {r : ℝ}
+    (h : Collinear ℝ ({p₁, p₂, p₃} : Set P)) (hp₁ : dist p₁ p = r) (hp₂ : dist p₂ p < r)
+    (hp₃ : dist p₃ p = r) (hp₁p₃ : p₁ ≠ p₃) : Sbtw ℝ p₁ p₂ p₃ := by
+  refine' ⟨h.wbtw_of_dist_eq_of_dist_le hp₁ hp₂.le hp₃ hp₁p₃, _, _⟩
+  · rintro rfl
+    exact hp₂.ne hp₁
+  · rintro rfl
+    exact hp₂.ne hp₃
+#align collinear.sbtw_of_dist_eq_of_dist_lt Collinear.sbtw_of_dist_eq_of_dist_lt