Commit 2025-12-19 22:50 97c2b335

feat: definition of ConvexSpace (#31984) This PR introduces ConvexSpace, an algebraic structure for spaces equipped with finite convex combinations. The main definitions are:

• StdSimplex R M: A finitely supported probability distribution over M with non-negative coefficients in R that sum to 1.
• StdSimplex.single, StdSimplex.duple: Constructors for point mass and two-point distributions.
• StdSimplex.map, StdSimplex.join: Monadic operations on standard simplices.
• ConvexSpace R M: A typeclass with convexCombination : StdSimplex R M → M satisfying monadic laws (assoc and single).
• convexCombo₂: Binary convex combinations of two points. 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 avoids universe issues with indexed families. 🤖 Prepared with Claude Code