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.convexComboPair_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 : 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.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 (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 : StdSimplex R (StdSimplex R P)) : convexCombination (StdSimplex.map convexCombination f) = convexCombination f.join

@[implicit_reducible]

noncomputable instance AddTorsor.instConvexSpace {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

Equations

• AddTorsor.instConvexSpace = { convexCombination := AddTorsor.convexCombination, assoc := ⋯, single := ⋯ }

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 : StdSimplex R P) : ConvexSpace.convexCombination s = (Finset.affineCombination R s.support id) ⇑s.weights

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

theorem AddTorsor.convexComboPair_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) : convexComboPair s t hs ht h x y = (AffineMap.lineMap y x) s

convexComboPair in an affine space is the affine line map.