Status of Convex on affine spaces

Stream: mathlib4

[Weiyi Wang]

In https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Convex/Basic.html it says "TODO: Generalize all this file to affine spaces". What is the progress on this? For context, if this becomes usable for affine spaces, it will make some of my intermediate lemma cleaner at #34826 (e.g. this would be just Convex s.closedInterior)

[Joseph Myers]

See #34594 - but note (a) even with that in, all the theory of convexity would need adapting to ConvexSpace, and (b) I'm not sure this should be an instance, as opposed to a def, because of the diamond issue (semimodules over ordered semirings should also be convex spaces, but then you get a diamond for a module over a ring, which can be a convex space either through the module structure or as an affine space for itself, and the two convex space structures would be equal but not defeq).

[Yury G. Kudryashov]

One way is to use the same typeclass for affine spaces and convex spaces.

[Yury G. Kudryashov]

(and don't use AddTorsor)

[Yury G. Kudryashov]

This means even more refactors.

[Yury G. Kudryashov]

I mean, ConvexSpace R X := AffineSpace {x : R // 0 \le x} X, where AffineSpace is defined in the way we define ConvexSpace. Then we'll have a def going from AddTorsor to AffineSpace.

[Joseph Myers]

That would still need to be a def not an instance to avoid a diamond (on the basis that semimodules over semirings would also be that kind of AffineSpace directly). I think the diamond is essential to anything involving affine combinations of points both in semimodules and in torsors for modules (though you could have a Prop typeclass to assert that the affine combinations in a torsor are the expected ones).