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.

theorem Sbtw.dist_lt_max_dist {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [StrictConvexSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] (p : P) {p₁ p₂ p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) : dist p₂ p < dist p₁ p ⊔ dist p₃ p

theorem Wbtw.dist_le_max_dist {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [StrictConvexSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] (p : P) {p₁ p₂ p₃ : P} (h : Wbtw ℝ p₁ p₂ p₃) : dist p₂ p ≤ dist p₁ p ⊔ dist p₃ p

theorem Collinear.wbtw_of_dist_eq_of_dist_le {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [StrictConvexSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] {p p₁ p₂ p₃ : P} {r : ℝ} (h : Collinear ℝ {p₁, p₂, p₃}) (hp₁ : dist p₁ p = r) (hp₂ : dist p₂ p ≤ r) (hp₃ : dist p₃ p = r) (hp₁p₃ : p₁ ≠ p₃) : Wbtw ℝ p₁ p₂ p₃

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.sbtw_of_dist_eq_of_dist_lt {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [StrictConvexSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] {p p₁ p₂ p₃ : P} {r : ℝ} (h : Collinear ℝ {p₁, p₂, p₃}) (hp₁ : dist p₁ p = r) (hp₂ : dist p₂ p < r) (hp₃ : dist p₃ p = r) (hp₁p₃ : p₁ ≠ p₃) : Sbtw ℝ p₁ p₂ p₃

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 dist_add_dist_eq_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [StrictConvexSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {a b c : P} : dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c

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 eq_lineMap_of_dist_eq_mul_of_dist_eq_mul {E : Type u_3} {PE : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [StrictConvexSpace ℝ E] [MetricSpace PE] [NormedAddTorsor E PE] {r : ℝ} {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

theorem eq_midpoint_of_dist_eq_half {E : Type u_3} {PE : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [StrictConvexSpace ℝ E] [MetricSpace PE] [NormedAddTorsor E PE] {x y z : PE} (hx : dist x y = dist x z / 2) (hy : dist y z = dist x z / 2) : y = midpoint ℝ x z

noncomputable def Isometry.affineIsometryOfStrictConvexSpace {E : Type u_3} {F : Type u_4} {PE : Type u_5} {PF : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] [StrictConvexSpace ℝ E] [MetricSpace PE] [MetricSpace PF] [NormedAddTorsor E PE] [NormedAddTorsor F PF] {f : PF → PE} (hi : Isometry f) : PF →ᵃⁱ[ℝ] PE

An isometry of NormedAddTorsors 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.

Equations

• hi.affineIsometryOfStrictConvexSpace = { toAffineMap := AffineMap.ofMapMidpoint f ⋯ ⋯, norm_map := ⋯ }

@[simp]

theorem Isometry.coe_affineIsometryOfStrictConvexSpace {E : Type u_3} {F : Type u_4} {PE : Type u_5} {PF : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] [StrictConvexSpace ℝ E] [MetricSpace PE] [MetricSpace PF] [NormedAddTorsor E PE] [NormedAddTorsor F PF] {f : PF → PE} (hi : Isometry f) : ⇑hi.affineIsometryOfStrictConvexSpace = f

@[simp]

theorem Isometry.affineIsometryOfStrictConvexSpace_apply {E : Type u_3} {F : Type u_4} {PE : Type u_5} {PF : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] [StrictConvexSpace ℝ E] [MetricSpace PE] [MetricSpace PF] [NormedAddTorsor E PE] [NormedAddTorsor F PF] {f : PF → PE} (hi : Isometry f) (p : PF) : hi.affineIsometryOfStrictConvexSpace p = f p