Convex metric spaces

A convex metric space is a convex space with a compatible metric structure. Concretely, we ask for dist(∑ tᵢ xᵢ, ∑ tᵢ yᵢ) ≤ ∑ tᵢ dist(xᵢ, yᵢ), which is what one would expect from the triangle inequality.

Main results

• IsConvexMetricSpace: The (Prop-valued) class of convex metric spaces.
• continuous_convexComboPair: Binary convex combination is continuous.
• Convex.isConvexMetricSpace: Convex subspaces of normed spaces are convex metric spaces.

TODO

• Equip StdSimplex with a topology and show the analogous continuity result for n-ary convex combinations.
• Tidy up the imports with Mathlib.LinearAlgebra.ConvexSpace.AffineSpace etc once those files are moved to proper places.

class IsConvexMetricSpace (X : Type u_1) [ConvexSpace ℝ X] [MetricSpace X] : Prop

A convex metric space is a real convex space with a compatible metric structure. Concretely, we ask for dist(∑ tᵢ xᵢ, ∑ tᵢ yᵢ) ≤ ∑ tᵢ dist(xᵢ, yᵢ), which is what one would expect from the triangle inequality.

In particular, convex subsets of normed affine spaces are convex metric spaces.

• dist_convexCombination_map_le' (f : StdSimplex ℝ ℕ) (x y : ℕ → X) : dist (ConvexSpace.convexCombination (StdSimplex.map x f)) (ConvexSpace.convexCombination (StdSimplex.map y f)) ≤ f.sum fun (i : ℕ) (r : ℝ) => r * dist (x i) (y i)

  Use dist_convexCombination_map_le instead.

theorem dist_convexCombination_map_le {X : Type u_1} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexMetricSpace X] {ι : Type u_2} (f : StdSimplex ℝ ι) (x y : ι → X) : dist (ConvexSpace.convexCombination (StdSimplex.map x f)) (ConvexSpace.convexCombination (StdSimplex.map y f)) ≤ f.sum fun (i : ι) (r : ℝ) => r * dist (x i) (y i)

dist(∑ tᵢ xᵢ, ∑ tᵢ yᵢ) ≤ ∑ tᵢ dist(xᵢ, yᵢ)

theorem dist_convexCombination_left_le {X : Type u_1} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexMetricSpace X] (f : StdSimplex ℝ X) (x : X) : dist (ConvexSpace.convexCombination f) x ≤ f.sum fun (i : X) (r : ℝ) => r * dist i x

theorem dist_convexCombination_right_le {X : Type u_1} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexMetricSpace X] (f : StdSimplex ℝ X) (x : X) : dist x (ConvexSpace.convexCombination f) ≤ f.sum fun (i : X) (r : ℝ) => r * dist x i

@[simp]

theorem dist_convexComboPair_left {X : Type u_1} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexMetricSpace X] {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X) : dist (convexComboPair s t hs ht h x y) x = t * dist x y

@[simp]

theorem dist_convexComboPair_right {X : Type u_1} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexMetricSpace X] {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X) : dist (convexComboPair s t hs ht h x y) y = s * dist x y

@[simp]

theorem dist_left_convexComboPair {X : Type u_1} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexMetricSpace X] {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X) : dist x (convexComboPair s t hs ht h x y) = t * dist x y

@[simp]

theorem dist_right_convexComboPair {X : Type u_1} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexMetricSpace X] {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X) : dist y (convexComboPair s t hs ht h x y) = s * dist x y

theorem dist_convexComboPair_convexComboPair {X : Type u_1} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexMetricSpace X] {s t s' t' : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (hs' : 0 ≤ s') (ht' : 0 ≤ t') (h' : s' + t' = 1) (x y : X) : dist (convexComboPair s t hs ht h x y) (convexComboPair s' t' hs' ht' h' x y) = |s - s'| * dist x y

dist(sx + (1-s)y, s'x + (1-s')y) = |s - s'| dist(x, y).

See dist_convexComboPair_convexComboPair_le for the version where the weights are fixed and the points change.

theorem dist_convexComboPair_convexComboPair_le {X : Type u_1} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexMetricSpace X] {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y x' y' : X) : dist (convexComboPair s t hs ht h x y) (convexComboPair s t hs ht h x' y') ≤ s * dist x x' + t * dist y y'

dist(sx + (1-s)y, sx' + (1-s)y') ≤ s dist(x, x') + (1-s) dist(y, y').

See dist_convexComboPair_convexComboPair for the version where the points are fixed and the weights change.

theorem continuous_convexComboPair {X : Type u_1} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexMetricSpace X] : Continuous fun (x : ↑(Set.Icc 0 1) × X × X) => convexComboPair (↑x.1) (1 - ↑x.1) ⋯ ⋯ ⋯ x.2.1 x.2.2

The convex combination (t, p, q) ↦ t • p + (1 - t) • q is continuous on [0, 1] × X × X for a convex metric space X.

theorem continuous_convexComboPair_of_isBounded {X : Type u_1} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexMetricSpace X] {T : Type u_2} [TopologicalSpace T] (f : T → ℝ) (hf : Continuous f) (hf0 : ∀ (t : T), 0 ≤ f t) (hf1 : ∀ (t : T), f t ≤ 1) (x y : T → X) (hx : ContinuousOn x (f ⁻¹' {0}ᶜ)) (hy : ContinuousOn y (f ⁻¹' {1}ᶜ)) (hx' : Bornology.IsBounded (Set.range x)) (hy' : Bornology.IsBounded (Set.range y)) : Continuous fun (i : T) => convexComboPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)

theorem continuous_convexComboPair' {X : Type u_1} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexMetricSpace X] [BoundedSpace X] {T : Type u_2} [TopologicalSpace T] (f : T → ℝ) (hf : Continuous f) (hf0 : ∀ (t : T), 0 ≤ f t) (hf1 : ∀ (t : T), f t ≤ 1) (x y : T → X) (hx : ContinuousOn x (f ⁻¹' {0}ᶜ)) (hy : ContinuousOn y (f ⁻¹' {1}ᶜ)) : Continuous fun (i : T) => convexComboPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)

When X is a bounded convex metric space, to check continuity of t ↦ f(t) • x(t) + (1 - f(t)) • y(t) it suffices to show that f is continuous, x is continuous away from f(t) = 0, and y is continuous away from f(t) = 1.

@[implicit_reducible]

noncomputable def ConvexSpace.ofConvex {R : Type u_2} {E : Type u_3} [LinearOrder R] [Field R] [IsStrictOrderedRing R] [AddCommGroup E] [Module R E] {S : Set E} (H : Convex R S) : ConvexSpace R ↑S

A convex subset of a vector space is a convex space.

Equations

• ConvexSpace.ofConvex H = { convexCombination := fun (f : StdSimplex R ↑S) => ⟨ConvexSpace.convexCombination (StdSimplex.map Subtype.val f), ⋯⟩, assoc := ⋯, single := ⋯ }

@[simp]

theorem ConvexSpace.ofConvex.coe_convexCombination {R : Type u_2} {E : Type u_3} [LinearOrder R] [Field R] [IsStrictOrderedRing R] [AddCommGroup E] [Module R E] (S : Set E) (H : Convex R S) (f : StdSimplex R ↑S) : ↑(convexCombination f) = convexCombination (StdSimplex.map Subtype.val f)

@[instance 100]

instance instIsConvexMetricSpace {V : Type u_2} {P : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] : IsConvexMetricSpace P

theorem IsConvexMetricSpace.of_convex {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {S : Set E} (H : Convex ℝ S) : IsConvexMetricSpace ↑S