Convex spaces with compatible metric structure

A convex space has a compatible metric structure if dist(∑ tᵢ xᵢ, ∑ tᵢ yᵢ) ≤ ∑ tᵢ dist(xᵢ, yᵢ). This is what one would expect from the triangle inequality.

Note that there is a separate notion of convex metric spaces in the literature that has little to do with this definition.

Main results

• Convexity.IsConvexDist: The (Prop-valued) class of convex spaces with compatible metric structure.
• Convexity.continuous_convexCombPair: Binary convex combination is continuous.
• Convexity.IsConvexDist.of_convex: 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.Geometric.Convex.ConvexSpace.AffineSpace.
• Define convex functions with domain a convex space, and redefine IsConvexDist as saying that dist : X × X → ℝ is convex.

class Convexity.IsConvexDist (X : Type u_2) [inst₁ : ConvexSpace ℝ X] [inst₂ : 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.

Note that there is a separate notion of convex metric spaces in the literature that has little to do with this definition.

• dist_iConvexComb_fst_snd_le (f : StdSimplex ℝ (X × X)) : dist (iConvexComb f Prod.fst) (iConvexComb f Prod.snd) ≤ iConvexComb f fun (x : X × X) => dist x.1 x.2

  Use dist_iConvexComb_le instead.

@[deprecated Convexity.IsConvexDist (since := "2026-05-15")]

def Convexity.IsConvexMetricSpace (X : Type u_2) [inst₁ : ConvexSpace ℝ X] [inst₂ : MetricSpace X] : Prop

Alias of Convexity.IsConvexDist.

---

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.

Note that there is a separate notion of convex metric spaces in the literature that has little to do with this definition.

Equations

• Convexity.IsConvexMetricSpace = Convexity.IsConvexDist

theorem Convexity.dist_iConvexComb_le {X : Type u_2} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexDist X] {ι : Type u_3} (f : StdSimplex ℝ ι) (x y : ι → X) : dist (iConvexComb f x) (iConvexComb f y) ≤ iConvexComb f fun (i : ι) => dist (x i) (y i)

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

@[deprecated Convexity.dist_iConvexComb_le (since := "2026-05-15")]

theorem Convexity.dist_convexCombination_right_le {X : Type u_2} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexDist X] {ι : Type u_3} (f : StdSimplex ℝ ι) (x y : ι → X) : dist (iConvexComb f x) (iConvexComb f y) ≤ iConvexComb f fun (i : ι) => dist (x i) (y i)

Alias of Convexity.dist_iConvexComb_le.

---

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

theorem Convexity.dist_iConvexComb_left_le {I : Type u_1} {X : Type u_2} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexDist X] (f : StdSimplex ℝ I) (g : I → X) (x : X) : dist (iConvexComb f g) x ≤ iConvexComb f fun (i : I) => dist (g i) x

theorem Convexity.dist_iConvexComb_right_le {I : Type u_1} {X : Type u_2} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexDist X] (x : X) (f : StdSimplex ℝ I) (g : I → X) : dist x (iConvexComb f g) ≤ iConvexComb f fun (i : I) => dist x (g i)

theorem Convexity.dist_sConvexComb_left_le {X : Type u_2} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexDist X] (f : StdSimplex ℝ X) (x : X) : dist (sConvexComb f) x ≤ iConvexComb f fun (x_1 : X) => dist x_1 x

theorem Convexity.dist_sConvexComb_right_le {X : Type u_2} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexDist X] (x : X) (f : StdSimplex ℝ X) : dist x (sConvexComb f) ≤ iConvexComb f (dist x)

@[simp]

theorem Convexity.dist_convexCombPair_left {X : Type u_2} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexDist X] {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X) : dist (convexCombPair s t hs ht h x y) x = t * dist x y

@[simp]

theorem Convexity.dist_convexCombPair_right {X : Type u_2} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexDist X] {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X) : dist (convexCombPair s t hs ht h x y) y = s * dist x y

@[simp]

theorem Convexity.dist_left_convexCombPair {X : Type u_2} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexDist X] {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X) : dist x (convexCombPair s t hs ht h x y) = t * dist x y

@[simp]

theorem Convexity.dist_right_convexCombPair {X : Type u_2} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexDist X] {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X) : dist y (convexCombPair s t hs ht h x y) = s * dist x y

theorem Convexity.dist_convexCombPair_convexCombPair {X : Type u_2} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexDist 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 (convexCombPair s t hs ht h x y) (convexCombPair 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_convexCombPair_convexCombPair_le for the version where the weights are fixed and the points change.

theorem Convexity.dist_convexCombPair_convexCombPair_le {X : Type u_2} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexDist X] {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y x' y' : X) : dist (convexCombPair s t hs ht h x y) (convexCombPair 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_convexCombPair_convexCombPair for the version where the points are fixed and the weights change.

theorem Convexity.continuous_convexCombPair {X : Type u_2} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexDist X] : Continuous fun (x : ↑(Set.Icc 0 1) × X × X) => convexCombPair (↑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.

@[deprecated Convexity.continuous_convexCombPair (since := "2026-05-15")]

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

Alias of Convexity.continuous_convexCombPair.

---

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 Convexity.continuous_convexCombPair_of_isBounded {X : Type u_2} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexDist X] {T : Type u_3} [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) => convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)

theorem Convexity.continuous_convexCombPair' {X : Type u_2} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexDist X] [BoundedSpace X] {T : Type u_3} [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) => convexCombPair (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.

@[deprecated Convexity.continuous_convexCombPair' (since := "2026-05-15")]

theorem Convexity.continuous_convexComboPair' {X : Type u_2} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexDist X] [BoundedSpace X] {T : Type u_3} [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) => convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)

Alias of Convexity.continuous_convexCombPair'.

---

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.

@[instance 100]

instance Convexity.instIsConvexDist {V : Type u_3} {P : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] : IsConvexDist P

instance Convexity.IsConvexDist.subtype {X : Type u_2} [ConvexSpace ℝ X] [MetricSpace X] [IsConvexDist X] (s : Set X) (hs : IsConvexSet ℝ s) : IsConvexDist ↑s

instance Convexity.IsConvexDist.submodule {F : Type u_3} {M : Type u_4} [AddCommGroup M] [MetricSpace M] [Module ℝ M] [ConvexSpace ℝ M] [IsModuleConvexSpace ℝ M] [IsConvexDist M] [SetLike F M] [AddSubmonoidClass F M] [SMulMemClass F ℝ M] {S : F} : IsConvexDist ↥S