Documentation

Mathlib.Analysis.Convex.StrictConvexBetween

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} {p₃ : P} (h : Sbtw p₁ p₂ p₃) :
dist p₂ p < max (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} {p₃ : P} (h : Wbtw p₁ p₂ p₃) :
dist p₂ p max (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₂ : 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₂ : 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 : P} {b : P} {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 : PE} {y : PE} {z : PE} (hxy : dist x y = r * dist x z) (hyz : dist y z = (1 - r) * dist x z) :
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 : PE} {y : PE} {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 : PFPE} (hi : Isometry f) :

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
Instances For
    @[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 : PFPE} (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 : PFPE} (hi : Isometry f) (p : PF) :
    hi.affineIsometryOfStrictConvexSpace p = f p