# Zulip Chat Archive

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

#### Kevin Buzzard (Aug 21 2020 at 22:44):

~~(or r=r'=1 :p)~~

#### Adam Topaz (Aug 21 2020 at 22:44):

~~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 ?

#### Kenny Lau (Aug 22 2020 at 14:33):

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