Convex spaces

This file defines convex spaces as an algebraic structure supporting finite convex combinations.

Main definitions

• Convexity.StdSimplex R M: A finitely supported probability distribution over elements of M with coefficients in R. The weights are non-negative and sum to 1.
• Convexity.StdSimplex.map: Map a function over the support of a standard simplex.
• Convexity.ConvexSpace R M: A typeclass for spaces M equipped with an operation Convexity.sConvexComb : StdSimplex R M → M satisfying monadic laws.
• Convexity.iConvexComb: Indexed convex combination operator.
• Convexity.convexCombPair: Binary convex combinations of two points.

Design

The design follows a monadic structure where StdSimplex R forms a monad and convexCombination is a monadic algebra. This eliminates the need for explicit extensionality axioms and resolves universe issues with indexed families.

structure Convexity.StdSimplex (R : Type u) [LE R] [AddCommMonoid R] [One R] (M : Type v) : Type (max u v)

A finitely supported probability distribution over elements of M with coefficients in R. The weights are non-negative and sum to 1.

• weights : M →₀ R

  The weights of the StdSimplex as a Finsupp.

• nonneg : 0 ≤ self.weights

  All weights are non-negative.

• total : (self.weights.sum fun (x : M) (r : R) => r) = 1

  The weights sum to 1.

@[simp]

theorem Convexity.StdSimplex.weights_nonneg {R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} {w : StdSimplex R M} (i : M) : 0 ≤ w.weights i

@[simp]

theorem Convexity.StdSimplex.weights_ne_zero {R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [Nontrivial R] (w : StdSimplex R M) : w.weights ≠ 0

theorem Convexity.StdSimplex.support_weights_nonempty {R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [Nontrivial R] (w : StdSimplex R M) : w.weights.support.Nonempty

theorem Convexity.StdSimplex.nonempty {R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [Nontrivial R] (w : StdSimplex R M) : Nonempty M

@[simp]

theorem Convexity.StdSimplex.weights_inj {R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} {f g : StdSimplex R M} : f.weights = g.weights ↔ f = g

theorem Convexity.StdSimplex.ext {R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} {f g : StdSimplex R M} : f.weights = g.weights → f = g

Alias of the forward direction of Convexity.StdSimplex.weights_inj.

theorem Convexity.StdSimplex.ext_iff {R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} {f g : StdSimplex R M} : f = g ↔ f.weights = g.weights

noncomputable def Convexity.StdSimplex.single {R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [IsStrictOrderedRing R] (x : M) : StdSimplex R M

The point mass distribution concentrated at x.

Equations

• Convexity.StdSimplex.single x = { weights := Finsupp.single x 1, nonneg := ⋯, total := ⋯ }

@[simp]

theorem Convexity.StdSimplex.weights_single {R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [IsStrictOrderedRing R] (x : M) : (single x).weights = Finsupp.single x 1

theorem Convexity.StdSimplex.mk_single {R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [IsStrictOrderedRing R] (x : M) {nonneg : 0 ≤ Finsupp.single x 1} {total : ((Finsupp.single x 1).sum fun (x : M) (r : R) => r) = 1} : { weights := Finsupp.single x 1, nonneg := nonneg, total := total } = single x

@[simp]

theorem Convexity.StdSimplex.support_weights_eq_singleton {R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} {w : StdSimplex R M} {x : M} [IsStrictOrderedRing R] : w.weights.support = {x} ↔ w = single x

noncomputable def Convexity.StdSimplex.duple {R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [IsStrictOrderedRing R] (x y : M) {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) : StdSimplex R M

A probability distribution with weight s on x and weight t on y.

Equations

• Convexity.StdSimplex.duple x y hs ht h = { weights := Finsupp.single x s + Finsupp.single y t, nonneg := ⋯, total := ⋯ }

@[simp]

theorem Convexity.StdSimplex.weights_duple {R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [IsStrictOrderedRing R] (x y : M) {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) : (duple x y hs ht h).weights = Finsupp.single x s + Finsupp.single y t

noncomputable def Convexity.StdSimplex.map {R : Type u} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type v} {N : Type w} (g : M → N) (f : StdSimplex R M) : StdSimplex R N

Map a function over the support of a standard simplex. For each n : N, the weight is the sum of weights of all m : M with g m = n.

Equations

• Convexity.StdSimplex.map g f = { weights := Finsupp.mapDomain g f.weights, nonneg := ⋯, total := ⋯ }

@[simp]

theorem Convexity.StdSimplex.weights_map {R : Type u} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type v} {N : Type w} (g : M → N) (f : StdSimplex R M) : (map g f).weights = Finsupp.mapDomain g f.weights

@[simp]

theorem Convexity.StdSimplex.map_const {R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} {N : Type u_10} [IsStrictOrderedRing R] (f : StdSimplex R M) (x : N) : map (fun (x_1 : M) => x) f = single x

@[simp]

theorem Convexity.StdSimplex.map_single {R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} {N : Type u_10} [IsStrictOrderedRing R] (x : M) (f : M → N) : map f (single x) = single (f x)

@[simp]

theorem Convexity.StdSimplex.map_duple {R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} {N : Type u_10} [IsStrictOrderedRing R] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : M) (f : M → N) : map f (duple x y hs ht h) = duple (f x) (f y) hs ht h

@[simp]

theorem Convexity.StdSimplex.map_id {R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [IsStrictOrderedRing R] (f : StdSimplex R M) : map id f = f

theorem Convexity.StdSimplex.map_comp {R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} {N : Type u_10} {P : Type u_11} [IsStrictOrderedRing R] (f : StdSimplex R M) (g₁ : M → N) (g₂ : N → P) : map (g₂ ∘ g₁) f = map g₂ (map g₁ f)

theorem Convexity.StdSimplex.map_map {R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} {N : Type u_10} {P : Type u_11} [IsStrictOrderedRing R] (f : StdSimplex R M) (g₁ : M → N) (g₂ : N → P) : map g₂ (map g₁ f) = map (fun (x : M) => g₂ (g₁ x)) f

noncomputable def Convexity.StdSimplex.join {R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [IsStrictOrderedRing R] (f : StdSimplex R (StdSimplex R M)) : StdSimplex R M

Join operation for standard simplices (monadic join). Given a distribution over distributions, flattens it to a single distribution.

Use ConvexSpace.sConvexComb instead.

Equations

• f.join = { weights := f.weights.sum fun (d : Convexity.StdSimplex R M) (r : R) => r • d.weights, nonneg := ⋯, total := ⋯ }

@[simp]

theorem Convexity.StdSimplex.weights_join {R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [IsStrictOrderedRing R] (f : StdSimplex R (StdSimplex R M)) : f.join.weights = f.weights.sum fun (d : StdSimplex R M) (r : R) => r • d.weights

noncomputable def Convexity.StdSimplex.restrict {X : Type u_2} {K : Type u_8} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] (w : StdSimplex K X) (s : Set X) (hs : ∃ x ∈ s, w.weights x ≠ 0) : StdSimplex K X

Project an element of the standard simplex to a lower-dimensional standard simplex, assuming at least one non-zero weight subsists.

Equations

• One or more equations did not get rendered due to their size.

theorem Convexity.StdSimplex.weights_restrict {X : Type u_2} {K : Type u_8} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] (w : StdSimplex K X) (s : Set X) (hs : ∃ x ∈ s, w.weights x ≠ 0) [DecidablePred fun (x : X) => x ∈ s] : (w.restrict s hs).weights = ((Finsupp.filter (fun (x : X) => x ∈ s) w.weights).sum fun (_x : X) (k : K) => k)⁻¹ • Finsupp.filter (fun (x : X) => x ∈ s) w.weights

@[simp]

theorem Convexity.StdSimplex.support_weights_restrict {X : Type u_2} {K : Type u_8} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [IsDomain K] (w : StdSimplex K X) (s : Set X) (hs : ∃ x ∈ s, w.weights x ≠ 0) [DecidablePred fun (x : X) => x ∈ s] : (w.restrict s hs).weights.support = {x ∈ w.weights.support | x ∈ s}

@[simp]

theorem Convexity.StdSimplex.restrict_singleton {X : Type u_2} {K : Type u_8} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [IsDomain K] (w : StdSimplex K X) (x : X) (hx : ∃ x_1 ∈ {x}, w.weights x_1 ≠ 0) : w.restrict {x} hx = single x

class Convexity.ConvexSpace (R : Type u) (M : Type v) [inst₁ : PartialOrder R] [inst₂ : Semiring R] [inst₃ : IsStrictOrderedRing R] : Type (max u v)

A set equipped with an operation of finite convex combinations, where the coefficients must be non-negative and sum to 1.

• mk' :: (
• sConvexComb (f : StdSimplex R M) : M

  Take a convex combination with the given probability distribution over points.

• sConvexComb_single (x : M) : sConvexComb (StdSimplex.single x) = x

  A convex combination of a single point is that point.

• assoc (f : StdSimplex R (StdSimplex R M)) : sConvexComb (StdSimplex.map sConvexComb f) = sConvexComb f.join

  Associativity of convex combination (monadic join law).

  Use sConvexComb_sConvexComb instead.

• )

@[deprecated Convexity.ConvexSpace.sConvexComb (since := "2026-05-04")]

def Convexity.ConvexSpace.convexCombination {R : Type u} {M : Type v} [inst₁ : PartialOrder R] [inst₂ : Semiring R] [inst₃ : IsStrictOrderedRing R] [self : ConvexSpace R M] (f : StdSimplex R M) : M

Alias of Convexity.ConvexSpace.sConvexComb.

---

Take a convex combination with the given probability distribution over points.

Equations

• @Convexity.ConvexSpace.convexCombination = @Convexity.sConvexComb

@[deprecated Convexity.ConvexSpace.sConvexComb_single (since := "2026-05-04")]

theorem Convexity.ConvexSpace.convexCombination_single {R : Type u} {M : Type v} {inst₁ : PartialOrder R} {inst₂ : Semiring R} {inst₃ : IsStrictOrderedRing R} [self : ConvexSpace R M] (x : M) : sConvexComb (StdSimplex.single x) = x

Alias of Convexity.ConvexSpace.sConvexComb_single.

---

A convex combination of a single point is that point.

noncomputable def Convexity.iConvexComb {R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] (s : StdSimplex R I) (f : I → M) : M

Take a convex combination with the given weight distribution of an indexed family of points.

Equations

• Convexity.iConvexComb s f = Convexity.sConvexComb (Convexity.StdSimplex.map f s)

noncomputable def Convexity.convexCombPair {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] (s t : R) (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t = 1) (x y : M) : M

Take a convex combination of two points.

Equations

• Convexity.convexCombPair s t hs ht hst x y = Convexity.sConvexComb (Convexity.StdSimplex.duple x y hs ht hst)

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

def Convexity.convexComboPair {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] (s t : R) (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t = 1) (x y : M) : M

Alias of Convexity.convexCombPair.

---

Take a convex combination of two points.

Equations

• @Convexity.convexComboPair = @Convexity.convexCombPair

@[implicit_reducible]

noncomputable instance Convexity.StdSimplex.instConvexSpace {R : Type u_1} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] : ConvexSpace R (StdSimplex R I)

Equations

• Convexity.StdSimplex.instConvexSpace = { sConvexComb := fun (σ : Convexity.StdSimplex R (Convexity.StdSimplex R I)) => σ.join, sConvexComb_single := ⋯, assoc := ⋯ }

@[simp]

theorem Convexity.StdSimplex.weights_sConvexComb {R : Type u_1} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (f : StdSimplex R (StdSimplex R I)) : (sConvexComb f).weights = f.weights.sum fun (d : StdSimplex R I) (r : R) => r • d.weights

@[simp]

theorem Convexity.StdSimplex.weights_iConvexComb {R : Type u_1} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (w : StdSimplex R I) (f : I → StdSimplex R I) : (iConvexComb w f).weights = w.weights.sum fun (i : I) (r : R) => r • (f i).weights

@[simp]

theorem Convexity.StdSimplex.weights_convexCombPair {R : Type u_1} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (w w' : StdSimplex R I) (s t : R) (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t = 1) : (convexCombPair s t hs ht hst w w').weights = s • w.weights + t • w'.weights

theorem Convexity.StdSimplex.map_sConvexComb {R : Type u_1} {I : Type u_6} {J : Type u_7} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (s : StdSimplex R (StdSimplex R I)) (f : I → J) : map f (sConvexComb s) = sConvexComb (map (map f) s)

theorem Convexity.StdSimplex.convexCombPair_restrict_restrict_compl {I : Type u_6} {K : Type u_8} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] (w : StdSimplex K I) (s : Set I) (hs : ∃ x ∈ s, w.weights x ≠ 0) (hs' : ∃ x ∈ sᶜ, w.weights x ≠ 0) [DecidablePred fun (x : I) => x ∈ s] : convexCombPair ((Finsupp.filter (fun (x : I) => x ∈ s) w.weights).sum fun (_x : I) (k : K) => k) ((Finsupp.filter (fun (x : I) => x ∉ s) w.weights).sum fun (_x : I) (k : K) => k) ⋯ ⋯ ⋯ (w.restrict s hs) (w.restrict sᶜ hs') = w

theorem Convexity.sConvexComb_sConvexComb {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] (f : StdSimplex R (StdSimplex R M)) : sConvexComb (sConvexComb f) = sConvexComb (StdSimplex.map sConvexComb f)

theorem Convexity.sConvexComb_convexCombPair {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] (s t : R) (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t = 1) (w w' : StdSimplex R M) : sConvexComb (convexCombPair s t hs ht hst w w') = convexCombPair s t hs ht hst (sConvexComb w) (sConvexComb w')

@[reducible, inline]

abbrev Convexity.ConvexSpace.mk {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_9} (sConvexComb : StdSimplex R M → M) (single : ∀ (x : M), sConvexComb (StdSimplex.single x) = x) (assoc : ∀ (f : StdSimplex R (StdSimplex R M)), sConvexComb (StdSimplex.map sConvexComb f) = sConvexComb (Convexity.sConvexComb f)) : ConvexSpace R M

The public constructor for ConvexSpace.

Equations

• Convexity.ConvexSpace.mk sConvexComb single assoc = { sConvexComb := sConvexComb, sConvexComb_single := single, assoc := assoc }

structure Convexity.IsAffineMap (R : Type u_1) {M : Type u_3} {N : Type u_4} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] [ConvexSpace R N] (f : M → N) : Prop

A map between convex spaces is affine if it preserves convex combinations.

TODO: Show that this generalises affine maps between affine spaces, see AffineMap.

• map_sConvexComb (s : StdSimplex R M) : f (sConvexComb s) = sConvexComb (StdSimplex.map f s)

theorem Convexity.IsAffineMap.id {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] : IsAffineMap R id

theorem Convexity.IsAffineMap.comp {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] [ConvexSpace R N] [ConvexSpace R P] {g : N → P} (hg : IsAffineMap R g) {f : M → N} (hf : IsAffineMap R f) : IsAffineMap R (g ∘ f)

theorem Convexity.StdSimplex.isAffineMap_map (R : Type u_1) {I : Type u_6} {J : Type u_7} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (f : I → J) : IsAffineMap R (map f)

theorem Convexity.sConvexComb_map {R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] (w : StdSimplex R I) (f : I → M) : sConvexComb (StdSimplex.map f w) = iConvexComb w f

@[simp]

theorem Convexity.iConvexComb_const {R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] (s : StdSimplex R I) (m : M) : (iConvexComb s fun (x : I) => m) = m

@[simp]

theorem Convexity.iConvexComb_single {R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] (i : I) (f : I → M) : iConvexComb (StdSimplex.single i) f = f i

theorem Convexity.iConvexComb_id {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] (w : StdSimplex R M) : iConvexComb w id = sConvexComb w

@[simp]

theorem Convexity.iConvexComb_id' {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] (w : StdSimplex R M) : (iConvexComb w fun (x : M) => x) = sConvexComb w

@[simp]

theorem Convexity.iConvexComb_map {R : Type u_1} {M : Type u_3} {I : Type u_6} {J : Type u_7} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] (s : StdSimplex R I) (f : I → J) (g : J → M) : iConvexComb (StdSimplex.map f s) g = iConvexComb s fun (i : I) => g (f i)

theorem Convexity.iConvexComb_congr {R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {w : StdSimplex R I} {f g : I → M} (hfg : ∀ (i : I), w.weights i ≠ 0 → f i = g i) : iConvexComb w f = iConvexComb w g

theorem Convexity.iConvexComb_reindex {R : Type u_1} {M : Type u_3} {I : Type u_6} {J : Type u_7} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] (s : StdSimplex R I) (f : I ≃ J) (g : I → M) : iConvexComb s g = iConvexComb (StdSimplex.map (⇑f) s) (g ∘ ⇑f.symm)

theorem Convexity.iConvexComb_assoc'' {R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {J : I → Type u_9} (s : StdSimplex R I) (f : (i : I) → StdSimplex R (J i)) (g : (i : I) → J i → M) : (iConvexComb s fun (i : I) => iConvexComb (f i) (g i)) = iConvexComb (iConvexComb s fun (i : I) => StdSimplex.map (fun (x : J i) => ⟨i, x⟩) (f i)) (Sigma.uncurry g)

Flattening nested iConvexCombs.

See iConvexComb_assoc' and iConvexComb_assoc for non-dependent versions.

theorem Convexity.iConvexComb_assoc' {R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {J : Type u_9} (s : StdSimplex R I) (f : I → StdSimplex R J) (g : I → J → M) : (iConvexComb s fun (i : I) => iConvexComb (f i) (g i)) = iConvexComb (iConvexComb s fun (i : I) => StdSimplex.map (fun (x : J) => (i, x)) (f i)) (Function.uncurry g)

Flattening nested iConvexCombs.

See iConvexComb_assoc'' for a more dependent version, and iConvexComb_assoc for a less dependent one.

theorem Convexity.iConvexComb_assoc {R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {J : Type u_9} (s : StdSimplex R I) (f : I → StdSimplex R J) (g : J → M) : (iConvexComb s fun (i : I) => iConvexComb (f i) g) = iConvexComb (iConvexComb s f) g

Flattening nested iConvexCombs.

See iConvexComb_assoc', iConvexComb_assoc'' for more dependent versions.

theorem Convexity.iConvexComb_comm {R : Type u_9} {M : Type u_10} {I : Type u_11} {J : Type u_12} [PartialOrder R] [CommSemiring R] [IsStrictOrderedRing R] [ConvexSpace R M] (f : StdSimplex R I) (g : StdSimplex R J) (e : I → J → M) : (iConvexComb f fun (i : I) => iConvexComb g (e i)) = iConvexComb g fun (j : J) => iConvexComb f fun (i : I) => e i j

theorem Convexity.IsAffineMap.map_iConvexComb {R : Type u_1} {M : Type u_3} {N : Type u_4} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] [ConvexSpace R N] {f : M → N} (hf : IsAffineMap R f) (s : StdSimplex R I) (g : I → M) : f (iConvexComb s g) = iConvexComb s (f ∘ g)

theorem Convexity.map_iConvexComb {R : Type u_1} {I : Type u_6} {J : Type u_7} {K : Type u_8} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {f : J → K} (s : StdSimplex R I) (g : I → StdSimplex R J) : StdSimplex.map f (iConvexComb s g) = iConvexComb s (StdSimplex.map f ∘ g)

theorem Convexity.convexCombPair_def {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (p q : M) : convexCombPair s t hs ht h p q = iConvexComb (StdSimplex.duple 0 1 hs ht h) ![p, q]

@[simp]

theorem Convexity.convexCombPair_zero {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {x y : M} : convexCombPair 0 1 ⋯ ⋯ ⋯ x y = y

A binary convex combination with weight 0 on the first point returns the second point.

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

theorem Convexity.convexComboPair_zero {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {x y : M} : convexCombPair 0 1 ⋯ ⋯ ⋯ x y = y

Alias of Convexity.convexCombPair_zero.

---

A binary convex combination with weight 0 on the first point returns the second point.

@[simp]

theorem Convexity.convexCombPair_one {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {x y : M} : convexCombPair 1 0 ⋯ ⋯ ⋯ x y = x

A binary convex combination with weight 1 on the first point returns the first point.

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

theorem Convexity.convexComboPair_one {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {x y : M} : convexCombPair 1 0 ⋯ ⋯ ⋯ x y = x

Alias of Convexity.convexCombPair_one.

---

A binary convex combination with weight 1 on the first point returns the first point.

@[simp]

theorem Convexity.convexCombPair_same {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {x : M} : convexCombPair s t hs ht h x x = x

A convex combination of a point with itself is that point.

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

theorem Convexity.convexComboPair_symm {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {x : M} : convexCombPair s t hs ht h x x = x

Alias of Convexity.convexCombPair_same.

---

A convex combination of a point with itself is that point.

theorem Convexity.convexCombPair_symm {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {x y : M} : convexCombPair s t hs ht h x y = convexCombPair t s ht hs ⋯ y x

theorem Convexity.IsAffineMap.map_convexCombPair {R : Type u_1} {M : Type u_3} {N : Type u_4} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] [ConvexSpace R N] {f : M → N} (hf : IsAffineMap R f) {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : M) : f (convexCombPair s t hs ht h x y) = convexCombPair s t hs ht h (f x) (f y)

theorem Convexity.convexCombPair_iConvexComb_iConvexComb {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {J₁ : Type u₁} {J₂ : Type u₂} (g₁ : StdSimplex R J₁) (g₂ : StdSimplex R J₂) (m₁ : J₁ → M) (m₂ : J₂ → M) : convexCombPair s t hs ht h (iConvexComb g₁ m₁) (iConvexComb g₂ m₂) = sConvexComb (convexCombPair s t hs ht h (StdSimplex.map m₁ g₁) (StdSimplex.map m₂ g₂))

Flattening with the outer combination specialized to convexCombPair.

theorem Convexity.iConvexComb_convexCombPair {R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] (s t : I → R) (hs : ∀ (i : I), 0 ≤ s i) (ht : ∀ (i : I), 0 ≤ t i) (h : ∀ (i : I), s i + t i = 1) (f : StdSimplex R I) (m₁ m₂ : I → M) : (iConvexComb f fun (i : I) => convexCombPair (s i) (t i) ⋯ ⋯ ⋯ (m₁ i) (m₂ i)) = sConvexComb (iConvexComb f fun (i : I) => StdSimplex.duple (m₁ i) (m₂ i) ⋯ ⋯ ⋯)

Flattening with the inner combination specialized to convexCombPair.

theorem Convexity.convexCombPair_iConvexComb_left {R : Type u_1} {M : Type u_3} {J : Type u_7} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (g : StdSimplex R J) (e : J → M) (m : M) : convexCombPair s t hs ht h (iConvexComb g e) m = sConvexComb (convexCombPair s t hs ht h (StdSimplex.map e g) (StdSimplex.single m))

theorem Convexity.convexCombPair_iConvexComb_right {R : Type u_1} {M : Type u_3} {J : Type u_7} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (m : M) (g : StdSimplex R J) (e : J → M) : convexCombPair s t hs ht h m (iConvexComb g e) = sConvexComb (convexCombPair s t hs ht h (StdSimplex.single m) (StdSimplex.map e g))

theorem Convexity.convexCombPair_convexCombPair_left_eq_sConvexComb {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {s' t' : R} (hs' : 0 ≤ s') (ht' : 0 ≤ t') (h' : s' + t' = 1) (m₁ m₂ m₃ : M) : convexCombPair s t hs ht h (convexCombPair s' t' hs' ht' h' m₁ m₂) m₃ = sConvexComb (convexCombPair s t hs ht h (StdSimplex.duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃))

Flattening nested binary convex combination into a single convex combination.

theorem Convexity.convexCombPair_convexCombPair_right_eq_sConvexComb {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {s' t' : R} (hs' : 0 ≤ s') (ht' : 0 ≤ t') (h' : s' + t' = 1) (m₁ m₂ m₃ : M) : convexCombPair s t hs ht h m₁ (convexCombPair s' t' hs' ht' h' m₂ m₃) = sConvexComb (convexCombPair s t hs ht h (StdSimplex.single m₁) (StdSimplex.duple m₂ m₃ hs' ht' h'))

Flattening nested binary convex combination into a single convex combination.

theorem Convexity.convexCombPair_convexCombPair_assoc_left {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {s' t' : R} (hs' : 0 ≤ s') (ht' : 0 ≤ t') (h' : s' + t' = 1) {s'' t'' : R} (hs'' : 0 ≤ s'') (ht'' : 0 ≤ t'') (h'' : s'' + t'' = 1) (H : t * s'' = s * t' * t'') (m₁ m₂ m₃ : M) : convexCombPair s t hs ht h (convexCombPair s' t' hs' ht' h' m₁ m₂) m₃ = convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ m₁ (convexCombPair s'' t'' hs'' ht'' h'' m₂ m₃)

theorem Convexity.convexCombPair_convexCombPair_assoc_right {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {s' t' : R} (hs' : 0 ≤ s') (ht' : 0 ≤ t') (h' : s' + t' = 1) {s'' t'' : R} (hs'' : 0 ≤ s'') (ht'' : 0 ≤ t'') (h'' : s'' + t'' = 1) (H : s * t'' = t * s' * s'') (m₁ m₂ m₃ : M) : convexCombPair s t hs ht h m₁ (convexCombPair s' t' hs' ht' h' m₂ m₃) = convexCombPair (s + t * s') (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃

theorem Convexity.iConvexComb_convexCombPair_comm {R : Type u_9} {M : Type u_10} {I : Type u_11} [PartialOrder R] [CommSemiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (f : StdSimplex R I) (e₁ e₂ : I → M) : (iConvexComb f fun (x : I) => convexCombPair s t hs ht h (e₁ x) (e₂ x)) = convexCombPair s t hs ht h (iConvexComb f e₁) (iConvexComb f e₂)

theorem Convexity.iConvexComb_convexCombPair_comm_left {R : Type u_9} {M : Type u_10} {I : Type u_11} [PartialOrder R] [CommSemiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (f : StdSimplex R I) (m : M) (e : I → M) : (iConvexComb f fun (x : I) => convexCombPair s t hs ht h (e x) m) = convexCombPair s t hs ht h (iConvexComb f e) m

theorem Convexity.iConvexComb_convexCombPair_comm_right {R : Type u_9} {M : Type u_10} {I : Type u_11} [PartialOrder R] [CommSemiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (f : StdSimplex R I) (m : M) (e : I → M) : (iConvexComb f fun (x : I) => convexCombPair s t hs ht h m (e x)) = convexCombPair s t hs ht h m (iConvexComb f e)

theorem Convexity.isAffineMap_convexCombPair {R : Type u_9} {M : Type u_10} [PartialOrder R] [CommSemiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (m : M) : IsAffineMap R (convexCombPair s t hs ht h m)