# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: convex polyhedra

#### Reid Barton (Dec 01 2020 at 18:44):

Do we have anything like this?

If a bounded subset of $\mathbb{Q}^n$ is the intersection of finitely many half-spaces, then it is also the convex hull of finitely many points.

#### Adam Topaz (Dec 01 2020 at 18:50):

Is this true? How is the upper half plane the convex hull of finitely many points? Am I misunderstanding the assertion?

#### Reid Barton (Dec 01 2020 at 18:50):

it's not bounded

#### Reid Barton (Dec 01 2020 at 18:50):

that said, I may easily have given the wrong hypotheses

#### Adam Topaz (Dec 01 2020 at 18:50):

Ah ok

#### Adam Topaz (Dec 01 2020 at 18:50):

Oh, so bounded + intersection of half spaces is a funny condition!

#### Adam Topaz (Dec 01 2020 at 18:52):

I guess the general statement is that a convex subset which is defined piecewise linearly and is bounded is the convex hull of finitely many points.

#### Bryan Gin-ge Chen (Dec 01 2020 at 18:55):

From quickly browsing over analysis.convex.basic and other stuff in `analysis.convex`

, I don't think we have this yet. I don't know what @Yury G. Kudryashov's plans are, but maybe this would depend on #2910 ?

#### Adam Topaz (Dec 01 2020 at 18:56):

This is the kind of intuitive statement that seems very difficult to formalize...

#### Adam Topaz (Dec 01 2020 at 19:09):

Does mathlib have the definition of extremal points in a convex set?

#### Bryan Gin-ge Chen (Dec 01 2020 at 19:44):

We have docs#convex_hull and you could look at the boundary of that.

#### Adam Topaz (Dec 01 2020 at 19:44):

That's not the same. E.g. the extremal points of the filled in square are the vertices, not the boundary

#### Bryan Gin-ge Chen (Dec 01 2020 at 20:24):

Oh, whoops! Right, I don't think we have that `def`

yet either, but the definition on Wikipedia seems easy enough to formalize:

```
import analysis.convex.basic
universes u v'
variables {E : Type u} {α : Type v'}
[add_comm_group E] [vector_space ℝ E]
[linear_ordered_field α]
{s : set E}
def is_strictly_between {x y : E} (h : x ≠ y) (z : E) : Prop :=
∀ (a b : ℝ) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1), a • x + b • y = z
def extremal_points : set E :=
{ t | t ∈ s ∧ ∀ (x y : E) (hx : x ∈ s) (hy : y ∈ s) (h : x ≠ y), ¬ is_strictly_between h t }
```

#### Adam Topaz (Dec 01 2020 at 20:27):

I think you want strict inequality in the definition of `is_strictly_between`

right?

#### Adam Topaz (Dec 01 2020 at 20:28):

Oh, and looks like I misremembered the name... wiki calls these "extreme points"

#### Adam Topaz (Dec 01 2020 at 20:34):

Anyway, I agree the definition is not too hard to write down. I mostly mentioned this because if I understand correctly the finite set that Reid is asking for in the original question in this thread would just be the set of extreme points. I imagine there is a more general statement one can formulate that holds true without the boundedness condition.

#### Bryan Gin-ge Chen (Dec 01 2020 at 20:53):

Yeah, understood.

While we're on this topic, I've used polymake before to compute the V-representation (V for vertex) of convex polytopes from the H-representation (H for half-space) and vice versa. Maybe as a long term goal we could look into formalizing some of the algorithms used there.

#### Adam Topaz (Dec 01 2020 at 21:05):

Ooh polymake looks cool!

#### Bryan Gin-ge Chen (Dec 01 2020 at 21:11):

Yeah, and it was actually much easier to use than I thought it would be! (Though I was only doing fairly simple stuff with it.) It looks like they have some kind of jupyter notebook integration now too which looks interesting.

#### Reid Barton (Dec 01 2020 at 21:11):

Does this problem have easily checkable certificates?

#### Bryan Gin-ge Chen (Dec 01 2020 at 21:20):

Seems to be easy in one direction and hard in the other? https://www.cs.mcgill.ca/~fukuda/soft/polyfaq/node21.html

I also found something about the "Verified Polyhedron Library" which uses Coq: https://hal.archives-ouvertes.fr/hal-02100006/

Last updated: May 16 2021 at 05:21 UTC