Affine spaces are convex spaces

This file shows that every affine space is a convex space.

Main results

• AddTorsor.instConvexSpace: An affine space over a module is a convex space.
• AddTorsor.convexCombination_eq_affineCombination: The convex combination equals the affine combination.
• AddTorsor.convexCombPair_eq_lineMap: Binary convex combinations are given by lineMap.

noncomputable def AddTorsor.convexCombination {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] (s : Convexity.StdSimplex R P) : P

The convex combination of points in an affine space, given a probability distribution.

Equations

• AddTorsor.convexCombination s = (Finset.affineCombination R s.weights.support id) ⇑s.weights

theorem AddTorsor.convexCombination_single {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x : P) : convexCombination (Convexity.StdSimplex.single x) = x

theorem AddTorsor.convexCombination_assoc {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (f : Convexity.StdSimplex R (Convexity.StdSimplex R P)) : convexCombination (Convexity.StdSimplex.map convexCombination f) = convexCombination f.join

@[implicit_reducible]

noncomputable def AddTorsor.toConvexSpace {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] : Convexity.ConvexSpace R P

Any affine space is a convex space.

This is not an instance because its convex combination operation is defined through the choice of an arbitrary basepoint, which makes it very diamond-prone.

Equations

• AddTorsor.toConvexSpace = { sConvexComb := AddTorsor.convexCombination, sConvexComb_single := ⋯, assoc := ⋯ }

theorem AddTorsor.sConvexComb_eq_affineCombination {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (s : Convexity.StdSimplex R P) : Convexity.sConvexComb s = (Finset.affineCombination R s.weights.support id) ⇑s.weights

ConvexSpace.sConvexComb in an affine space is the affine combination.

@[deprecated AddTorsor.sConvexComb_eq_affineCombination (since := "2026-05-15")]

theorem AddTorsor.convexCombination_eq_affineCombination {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (s : Convexity.StdSimplex R P) : Convexity.sConvexComb s = (Finset.affineCombination R s.weights.support id) ⇑s.weights

Alias of AddTorsor.sConvexComb_eq_affineCombination.

---

ConvexSpace.sConvexComb in an affine space is the affine combination.

theorem AddTorsor.iConvexComb_eq_affineCombination {R : Type u_1} {V : Type u_2} {P : Type u_3} {I : Type u_4} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (s : Convexity.StdSimplex R I) (f : I → P) : Convexity.iConvexComb s f = (Finset.affineCombination R s.weights.support f) ⇑s.weights

theorem AddTorsor.convexCombPair_eq_lineMap {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (s t : R) (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : P) : Convexity.convexCombPair s t hs ht h x y = (AffineMap.lineMap y x) s

convexCombPair in an affine space is the affine line map.

theorem Convexity.sConvexComb_eq_sum {R : Type u_1} {V : Type u_2} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] (f : StdSimplex R V) : sConvexComb f = f.weights.sum fun (i : V) (r : R) => r • i

@[deprecated Convexity.sConvexComb_eq_sum (since := "2026-04-03")]

theorem convexCombination_eq_sum {R : Type u_1} {V : Type u_2} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] (f : Convexity.StdSimplex R V) : Convexity.sConvexComb f = f.weights.sum fun (i : V) (r : R) => r • i

Alias of Convexity.sConvexComb_eq_sum.

theorem Convexity.iConvexComb_eq_sum {R : Type u_1} {V : Type u_2} {I : Type u_4} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] (f : StdSimplex R I) (g : I → V) : iConvexComb f g = f.weights.sum fun (i : I) (r : R) => r • g i

theorem Convexity.convexCombPair_eq_add {R : Type u_1} {V : Type u_2} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : V) : convexCombPair s t hs ht h x y = s • x + t • y

theorem Convexity.StdSimplex.isAffineMap_weights (R : Type u_1) (I : Type u_4) [Ring R] [PartialOrder R] [IsStrictOrderedRing R] : IsAffineMap R weights