Affine spaces are convex spaces

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

Main results

• AddTorsor.toConvexSpace: An affine space over a module is a convex space.
• AddTorsor.sConvexComb_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 Convexity.ConvexSpace.ofAddTorsor {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] : 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

• Convexity.ConvexSpace.ofAddTorsor = { sConvexComb := AddTorsor.convexCombination, sConvexComb_single := ⋯, assoc := ⋯ }

@[implicit_reducible, deprecated Convexity.ConvexSpace.ofAddTorsor (since := "2026-07-02")]

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

Alias of Convexity.ConvexSpace.ofAddTorsor.

---

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 = @Convexity.ConvexSpace.ofAddTorsor

class Convexity.IsAffineConvexSpace (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] [ConvexSpace R P] : Prop

Typeclass for a convex space structure on an affine space to be given by affine combinations.

• sConvexComb_eq_convexComb (w : StdSimplex R P) : sConvexComb w = AddTorsor.convexCombination w

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

instance Convexity.IsAffineConvexSpace.ofAddTorsor {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] : IsAffineConvexSpace R V P

instance Convexity.IsModuleConvexSpace.isAffineConvexSpace {R : Type u_1} {V : Type u_2} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [ConvexSpace R V] [IsModuleConvexSpace R V] : IsAffineConvexSpace R V V

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] [Convexity.ConvexSpace R P] [Convexity.IsAffineConvexSpace R 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] [Convexity.ConvexSpace R P] [Convexity.IsAffineConvexSpace R 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] [Convexity.ConvexSpace R P] [Convexity.IsAffineConvexSpace R 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] [Convexity.ConvexSpace R P] [Convexity.IsAffineConvexSpace R 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.