Convex spaces

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

Main definitions

• Convexity.StdSimplex R X: A finitely supported probability distribution over elements of X 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 X: A typeclass for spaces X equipped with an operation Convexity.sConvexComb : StdSimplex R X → X 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] (X : Type v) : Type (max u v)

The space of nonnegative functions X → R which take finitely many non-zero values summing to 1.

One can interpret this as the standard simplex in R^⊕X (R^X for finite X), with the embedding being the map weights : StdSimplex R X → R^⊕X.

Note in particular that, in the common case where X := M is a R-module, StdSimplex R M is NOT the standard simplex in M. Indeed, the notion of a standard simplex depends on a choice of basis, and M isn't given one.

• weights : X →₀ R

  The weights of the StdSimplex as a Finsupp.

• nonneg : 0 ≤ self.weights

  All weights are non-negative.

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

  The weights sum to 1.

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

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

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

@[simp]

theorem Convexity.StdSimplex.total_of_fintype {X : Type u_2} {R : Type u} [PartialOrder R] [Semiring R] [Fintype X] (w : StdSimplex R X) : ∑ i : X, w.weights i = 1

@[simp]

theorem Convexity.StdSimplex.total_fin_two {R : Type u} [PartialOrder R] [Semiring R] (w : StdSimplex R (Fin 2)) : w.weights 0 + w.weights 1 = 1

theorem Convexity.StdSimplex.range_toFun_comp_weights {X : Type u_2} {R : Type u} [PartialOrder R] [Semiring R] [Fintype X] : (Set.range fun (t : StdSimplex R X) => ⇑t.weights) = (⋂ (i : X), {s : X → R | 0 ≤ s i}) ∩ {s : X → R | ∑ i : X, s i = 1}

@[simp]

theorem Convexity.StdSimplex.weights_apply_eq_one {X : Type u_2} {R : Type u} [PartialOrder R] [Semiring R] [Subsingleton X] (s : StdSimplex R X) (m : X) : s.weights m = 1

instance Convexity.StdSimplex.instSubsingleton {X : Type u_2} {R : Type u} [PartialOrder R] [Semiring R] [Subsingleton X] : Subsingleton (StdSimplex R X)

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

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 {X : Type u_2} {R : Type u} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (x : X) : (single x).weights = Finsupp.single x 1

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

@[simp]

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

theorem Convexity.StdSimplex.single_injective {X : Type u_2} {R : Type u} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] : Function.Injective single

@[simp]

theorem Convexity.StdSimplex.weights_apply_le_one {X : Type u_2} {R : Type u} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (s : StdSimplex R X) (m : X) : s.weights m ≤ 1

@[instance_reducible]

noncomputable instance Convexity.StdSimplex.instInhabited {X : Type u_2} {R : Type u} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Inhabited X] : Inhabited (StdSimplex R X)

Equations

• Convexity.StdSimplex.instInhabited = { default := Convexity.StdSimplex.single default }

instance Convexity.StdSimplex.instNonempty {X : Type u_2} {R : Type u} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Nonempty X] : Nonempty (StdSimplex R X)

instance Convexity.StdSimplex.instNontrivial {X : Type u_2} {R : Type u} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Nontrivial X] : Nontrivial (StdSimplex R X)

@[instance_reducible]

noncomputable instance Convexity.StdSimplex.instUnique {X : Type u_2} {R : Type u} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Unique X] : Unique (StdSimplex R X)

Equations

• Convexity.StdSimplex.instUnique = { toInhabited := Convexity.StdSimplex.instInhabited, uniq := ⋯ }

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

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 {X : Type u_2} {R : Type u} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (x y : X) {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] {X : Type v} {Y : Type w} (g : X → Y) (f : StdSimplex R X) : StdSimplex R Y

Map a function over the support of a standard simplex. For each n : Y, the weight is the sum of weights of all m : X 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] {X : Type v} {Y : Type w} (g : X → Y) (f : StdSimplex R X) : (map g f).weights = Finsupp.mapDomain g f.weights

@[simp]

theorem Convexity.StdSimplex.map_const {X : Type u_2} {Y : Type u_3} {R : Type u} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (f : StdSimplex R X) (x : Y) : map (fun (x_1 : X) => x) f = single x

@[simp]

theorem Convexity.StdSimplex.map_single {X : Type u_2} {Y : Type u_3} {R : Type u} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (x : X) (f : X → Y) : map f (single x) = single (f x)

@[simp]

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

@[simp]

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

theorem Convexity.StdSimplex.map_id' {X : Type u_2} {R : Type u} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] : map id = id

theorem Convexity.StdSimplex.map_comp {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {R : Type u} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (f : StdSimplex R X) (g₁ : X → Y) (g₂ : Y → Z) : map (g₂ ∘ g₁) f = map g₂ (map g₁ f)

theorem Convexity.StdSimplex.map_comp' {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {R : Type u} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (g₁ : X → Y) (g₂ : Y → Z) : map (g₂ ∘ g₁) = map g₂ ∘ map g₁

theorem Convexity.StdSimplex.map_map {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {R : Type u} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (f : StdSimplex R X) (g₁ : X → Y) (g₂ : Y → Z) : map g₂ (map g₁ f) = map (fun (x : X) => g₂ (g₁ x)) f

theorem Convexity.StdSimplex.mem_range_map_iff {X : Type u_2} {Y : Type u_3} {R : Type u} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (f : X → Y) (s : StdSimplex R Y) : s ∈ Set.range (map f) ↔ ∀ x ∉ Set.range f, s.weights x = 0

noncomputable def Convexity.StdSimplex.equivIcc {R' : Type u_8} [Ring R'] [PartialOrder R'] [IsStrictOrderedRing R'] : StdSimplex R' (Fin 2) ≃ ↑(Set.Icc 0 1)

The bijection between the one dimensional standard simplex and the interval [0, 1].

Equations

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

theorem Convexity.StdSimplex.equivIcc_apply_coe {R' : Type u_8} [Ring R'] [PartialOrder R'] [IsStrictOrderedRing R'] (s : StdSimplex R' (Fin 2)) : ↑(equivIcc s) = s.weights 1

theorem Convexity.StdSimplex.equivIcc_symm_apply {R' : Type u_8} [Ring R'] [PartialOrder R'] [IsStrictOrderedRing R'] (t : ↑(Set.Icc 0 1)) : equivIcc.symm t = duple 0 1 ⋯ ⋯ ⋯

@[simp]

theorem Convexity.StdSimplex.equivIcc_single_zero {R' : Type u_8} [Ring R'] [PartialOrder R'] [IsStrictOrderedRing R'] : equivIcc (single 0) = 0

@[simp]

theorem Convexity.StdSimplex.equivIcc_single_one {R' : Type u_8} [Ring R'] [PartialOrder R'] [IsStrictOrderedRing R'] : equivIcc (single 1) = 1

@[simp]

theorem Convexity.StdSimplex.equivIcc_symm_zero {R' : Type u_8} [Ring R'] [PartialOrder R'] [IsStrictOrderedRing R'] : equivIcc.symm 0 = single 0

@[simp]

theorem Convexity.StdSimplex.equivIcc_symm_one {R' : Type u_8} [Ring R'] [PartialOrder R'] [IsStrictOrderedRing R'] : equivIcc.symm 1 = single 1

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

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 X) (r : R) => r • d.weights, nonneg := ⋯, total := ⋯ }

@[simp]

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

noncomputable def Convexity.StdSimplex.restrict {X : Type u_2} {K : Type u_7} [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_7} [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_7} [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_7} [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) (X : 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 X) : X

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

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

  A convex combination of a single point is that point.

• assoc (f : StdSimplex R (StdSimplex R X)) : 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} {X : Type v} [inst₁ : PartialOrder R] [inst₂ : Semiring R] [inst₃ : IsStrictOrderedRing R] [self : ConvexSpace R X] (f : StdSimplex R X) : X

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} {X : Type v} {inst₁ : PartialOrder R} {inst₂ : Semiring R} {inst₃ : IsStrictOrderedRing R} [self : ConvexSpace R X] (x : X) : 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} {X : Type u_2} {I : Type u_5} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] (s : StdSimplex R I) (f : I → X) : X

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} {X : Type u_2} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] (s t : R) (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t = 1) (x y : X) : X

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} {X : Type u_2} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] (s t : R) (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t = 1) (x y : X) : X

Alias of Convexity.convexCombPair.

---

Take a convex combination of two points.

Equations

• @Convexity.convexComboPair = @Convexity.convexCombPair

@[instance_reducible]

noncomputable instance Convexity.StdSimplex.instConvexSpace {R : Type u_1} {I : Type u_5} [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_5} [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_5} [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_5} [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_5} {J : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (s : StdSimplex R (StdSimplex R I)) (f : I → J) : map f (sConvexComb s) = sConvexComb (map (map f) s)

@[simp]

theorem Convexity.StdSimplex.iConvexComb_single {R : Type u_1} {I : Type u_5} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (x : StdSimplex R I) : iConvexComb x single = x

theorem Convexity.StdSimplex.convexCombPair_restrict_restrict_compl {I : Type u_5} {K : Type u_7} [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} {X : Type u_2} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] (f : StdSimplex R (StdSimplex R X)) : sConvexComb (sConvexComb f) = sConvexComb (StdSimplex.map sConvexComb f)

theorem Convexity.sConvexComb_convexCombPair {R : Type u_1} {X : Type u_2} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] (s t : R) (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t = 1) (w w' : StdSimplex R X) : 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] {X : Type u_8} (sConvexComb : StdSimplex R X → X) (single : ∀ (x : X), sConvexComb (StdSimplex.single x) = x) (assoc : ∀ (f : StdSimplex R (StdSimplex R X)), sConvexComb (StdSimplex.map sConvexComb f) = sConvexComb (Convexity.sConvexComb f)) : ConvexSpace R X

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) {X : Type u_2} {Y : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] [ConvexSpace R Y] (f : X → Y) : 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 X) : f (sConvexComb s) = sConvexComb (StdSimplex.map f s)

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

theorem Convexity.IsAffineMap.comp {R : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] [ConvexSpace R Y] [ConvexSpace R Z] {g : Y → Z} (hg : IsAffineMap R g) {f : X → Y} (hf : IsAffineMap R f) : IsAffineMap R (g ∘ f)

theorem Convexity.IsAffineMap.const {R : Type u_1} {X : Type u_2} {Y : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] [ConvexSpace R Y] (x : Y) : IsAffineMap R fun (x_1 : X) => x

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

theorem Convexity.iConvexComb_congr {R : Type u_1} {X : Type u_2} {I : Type u_5} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] {w : StdSimplex R I} {f g : I → X} (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} {X : Type u_2} {I : Type u_5} {J : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] (s : StdSimplex R I) (f : I ≃ J) (g : I → X) : iConvexComb s g = iConvexComb (StdSimplex.map (⇑f) s) (g ∘ ⇑f.symm)

theorem Convexity.iConvexComb_assoc'' {R : Type u_1} {X : Type u_2} {I : Type u_5} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] {J : I → Type u_8} (s : StdSimplex R I) (f : (i : I) → StdSimplex R (J i)) (g : (i : I) → J i → X) : (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} {X : Type u_2} {I : Type u_5} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] {J : Type u_8} (s : StdSimplex R I) (f : I → StdSimplex R J) (g : I → J → X) : (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} {X : Type u_2} {I : Type u_5} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] {J : Type u_8} (s : StdSimplex R I) (f : I → StdSimplex R J) (g : J → X) : (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_8} {X : Type u_9} {I : Type u_10} {J : Type u_11} [PartialOrder R] [CommSemiring R] [IsStrictOrderedRing R] [ConvexSpace R X] (f : StdSimplex R I) (g : StdSimplex R J) (e : I → J → X) : (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} {X : Type u_2} {Y : Type u_3} {I : Type u_5} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] [ConvexSpace R Y] {f : X → Y} (hf : IsAffineMap R f) (s : StdSimplex R I) (g : I → X) : f (iConvexComb s g) = iConvexComb s (f ∘ g)

theorem Convexity.map_iConvexComb {R : Type u_1} {I : Type u_5} {J : Type u_6} {K : Type u_7} [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)

@[simp]

theorem Convexity.sConvexComb_map_iConvexComb {R : Type u_1} {X : Type u_2} {I : Type u_5} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] (f : I → X) (s : StdSimplex R (StdSimplex R I)) : sConvexComb (StdSimplex.map (fun (s : StdSimplex R I) => iConvexComb s f) s) = iConvexComb (sConvexComb s) f

theorem Convexity.convexCombPair_def {R : Type u_1} {X : Type u_2} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (p q : X) : 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} {X : Type u_2} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] {x y : X} : 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} {X : Type u_2} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] {x y : X} : 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} {X : Type u_2} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] {x y : X} : 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} {X : Type u_2} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] {x y : X} : 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} {X : Type u_2} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {x : X} : 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} {X : Type u_2} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {x : X} : 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} {X : Type u_2} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {x y : X} : convexCombPair s t hs ht h x y = convexCombPair t s ht hs ⋯ y x

theorem Convexity.IsAffineMap.map_convexCombPair {R : Type u_1} {X : Type u_2} {Y : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] [ConvexSpace R Y] {f : X → Y} (hf : IsAffineMap R f) {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X) : 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} {X : Type u_2} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] {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₁ → X) (m₂ : J₂ → X) : 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} {X : Type u_2} {I : Type u_5} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] (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 → X) : (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} {X : Type u_2} {J : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (g : StdSimplex R J) (e : J → X) (m : X) : 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} {X : Type u_2} {J : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (m : X) (g : StdSimplex R J) (e : J → X) : 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} {X : Type u_2} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] {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₃ : X) : 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} {X : Type u_2} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] {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₃ : X) : 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} {X : Type u_2} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] {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₃ : X) : 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} {X : Type u_2} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R X] {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₃ : X) : 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_8} {X : Type u_9} {I : Type u_10} [PartialOrder R] [CommSemiring R] [IsStrictOrderedRing R] [ConvexSpace R X] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (f : StdSimplex R I) (e₁ e₂ : I → X) : (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_8} {X : Type u_9} {I : Type u_10} [PartialOrder R] [CommSemiring R] [IsStrictOrderedRing R] [ConvexSpace R X] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (f : StdSimplex R I) (m : X) (e : I → X) : (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_8} {X : Type u_9} {I : Type u_10} [PartialOrder R] [CommSemiring R] [IsStrictOrderedRing R] [ConvexSpace R X] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (f : StdSimplex R I) (m : X) (e : I → X) : (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_8} {X : Type u_9} [PartialOrder R] [CommSemiring R] [IsStrictOrderedRing R] [ConvexSpace R X] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (m : X) : IsAffineMap R (convexCombPair s t hs ht h m)