Convex spaces

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

Main definitions

• 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.
• StdSimplex.map: Map a function over the support of a standard simplex.
• StdSimplex.join: Monadic join operation for standard simplices.
• ConvexSpace R M: A typeclass for spaces M equipped with an operation convexCombination : StdSimplex R M → M satisfying monadic laws.
• convexComboPair: 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.

TODO

• Show that an AffineSpace is a ConvexSpace.
• Show that lineMap agrees with convexComboPair where defined.
• Show the usual associativity law for binary convex combinations follows from the assoc axiom.

structure StdSimplex (R : Type u) [LE R] [AddCommMonoid R] [One R] (M : Type v) extends M →₀ R : 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.

• support : Finset M
• toFun : M → R
• mem_support_toFun (a : M) : a ∈ self.support ↔ self.toFun a ≠ 0
• nonneg : 0 ≤ self.weights

  All weights are non-negative.

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

  The weights sum to 1.

theorem StdSimplex.ext {R : Type u} [PartialOrder R] [Semiring R] {M : Type v} {f g : StdSimplex R M} (h : f.weights = g.weights) : f = g

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

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

The point mass distribution concentrated at x.

Equations

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

@[simp]

theorem StdSimplex.mk_single {R : Type u} [PartialOrder R] [Semiring R] {M : Type v} [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

def StdSimplex.duple {R : Type u} [PartialOrder R] [Semiring R] {M : Type v} [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

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

def 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

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

def StdSimplex.join {R : Type u} [PartialOrder R] [Semiring R] {M : Type v} [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.

Equations

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

class ConvexSpace (R : Type u) (M : Type v) [PartialOrder R] [Semiring R] [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.

• convexCombination (f : StdSimplex R M) : M

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

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

  Associativity of convex combination (monadic join law).

• single (x : M) : convexCombination (StdSimplex.single x) = x

  A convex combination of a single point is that point.

def convexComboPair {R : Type u_1} {M : Type u_2} [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) : M

Take a convex combination of two points.

Equations

• convexComboPair s t hs ht h x y = ConvexSpace.convexCombination (StdSimplex.duple x y hs ht h)

theorem convexComboPair_zero {R : Type u_2} {M : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {x y : M} : convexComboPair 0 1 ⋯ ⋯ ⋯ x y = y

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

theorem convexComboPair_one {R : Type u_2} {M : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {x y : M} : convexComboPair 1 0 ⋯ ⋯ ⋯ x y = x

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

theorem convexComboPair_same {R : Type u_1} {M : Type u_2} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {x : M} : convexComboPair s t hs ht h x x = x

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