## Stream: maths

### Topic: convexity

#### Yury G. Kudryashov (Aug 21 2020 at 22:16):

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 (Aug 21 2020 at 22:18):

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

#### Yury G. Kudryashov (Aug 21 2020 at 22:21):

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 (Aug 21 2020 at 22:25):

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 (Aug 21 2020 at 22:32):

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 (Aug 21 2020 at 22:40):

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)$.

(or r=r'=1 :p)

well yeah :)

#### Patrick Massot (Aug 22 2020 at 00:04):

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

#### Frédéric Dupuis (Aug 22 2020 at 00:08):

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 (Aug 22 2020 at 02:01):

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 (Aug 22 2020 at 02:04):

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

#### Adam Topaz (Aug 22 2020 at 02:10):

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 (Aug 22 2020 at 04:11):

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 (Aug 22 2020 at 14:32):

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 ?

I don't know

#### Frédéric Dupuis (Aug 22 2020 at 14:56):

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

#### Kenny Lau (Aug 22 2020 at 15:03):

what's the definition of convex_space?

#### Adam Topaz (Aug 22 2020 at 15:05):

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

Last updated: May 11 2021 at 15:12 UTC