convexity

Stream: maths

[Yury G. Kudryashov]

There are two natural structures that make it possible to speak about convex combinations (hence, convexity, convex functions etc): [semimodule nnreal E] and [vector_space real E] [add_torsor E P].

[Yury G. Kudryashov]

Unfortunately, in the most common case [vector_space real E] these two approaches result in non-defeq definitions.

[Yury G. Kudryashov]

For a [semimodule nnreal E] we can talk about a • x + (1 - a) • y and for an affine_space we can talk about a • (y -ᵥ x) +ᵥ x.

[Yury G. Kudryashov]

So, we either need some clever trick (I failed to come up with one) or stick to one of the approaches. @Patrick Massot @Sebastien Gouezel @Frédéric Dupuis What do think?

[Reid Barton]

There's also a separate algebraic structure of convex space which is a place where you can form convex combinations, and which you can obtain from either of these I guess. (Its free algebra on n+1 generators is the n-simplex.)

[Adam Topaz]

This abstract version has some examples which don't really come from geometry, like the quotient $[0,1]$ (as a convex set) by the equivalence relation $r \sim r'$ iff $r,r' \in [0,1)$.

[Kevin Buzzard]

(or r=r'=1 :p)

[Adam Topaz]

well yeah :)

[Patrick Massot]

I would prioritize the affine space case which seems much more common.

[Frédéric Dupuis]

Is there no way to define some sort of "pre-add_torsor" typeclass that wouldn't require an additive group but only a monoid? Even if it's only used for this, it might be worth it if it's possible.

[Yury G. Kudryashov]

Reid Barton said:

There's also a separate algebraic structure of convex space which is a place where you can form convex combinations, and which you can obtain from either of these I guess. (Its free algebra on n+1 generators is the n-simplex.)

If we go this way, then a vector_space real E will have two non-defeq instances.

[Yury G. Kudryashov]

@Frédéric Dupuis Do you have some definition?

[Adam Topaz]

FWIW, I do think that these abstract convex gadgets deserve some attention. They're (positive) Archimedean analogues of $\mathbb{Z}_p$ modules, and the silly example I mentioned above is a "torsion" module, in some sense. The "usual" convex spaces, defined as subsets of real vector spaces, are analogous to lattices in $\mathbb{Q}_p$-vector spaces.

[Yury G. Kudryashov]

We can add a typeclass convex_space but then we'll have a diamond vector_space ℝ E → add_torsor E E → convex_space E vs vector_space ℝ E → semimodule ℝ≥0 E → convex_space E, and the resulting "convex combination" instances are not defeq.

[Adam Topaz]

The second path vector_space ℝ E → semimodule ℝ≥0 E → convex_space E is essentially a restriction of scalars. Would it make sense to define something analogous to scalar_tower @Kenny Lau ?

[Kenny Lau]

I don't know

[Frédéric Dupuis]

@Yury G. Kudryashov No, I don't have a specific definition, it was probably just wishful thinking.

[Kenny Lau]

what's the definition of convex_space?

[Adam Topaz]

https://ncatlab.org/nlab/show/convex+space