Zulip Chat Archive

Stream: Is there code for X?

Topic: convex polyhedra


view this post on Zulip Reid Barton (Dec 01 2020 at 18:44):

Do we have anything like this?
If a bounded subset of Qn\mathbb{Q}^n is the intersection of finitely many half-spaces, then it is also the convex hull of finitely many points.

view this post on Zulip 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?

view this post on Zulip Reid Barton (Dec 01 2020 at 18:50):

it's not bounded

view this post on Zulip Reid Barton (Dec 01 2020 at 18:50):

that said, I may easily have given the wrong hypotheses

view this post on Zulip Adam Topaz (Dec 01 2020 at 18:50):

Ah ok

view this post on Zulip Adam Topaz (Dec 01 2020 at 18:50):

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

view this post on Zulip 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.

view this post on Zulip 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 ?

view this post on Zulip Adam Topaz (Dec 01 2020 at 18:56):

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

view this post on Zulip Adam Topaz (Dec 01 2020 at 19:09):

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

view this post on Zulip Bryan Gin-ge Chen (Dec 01 2020 at 19:44):

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

view this post on Zulip 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

view this post on Zulip 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 }

view this post on Zulip Adam Topaz (Dec 01 2020 at 20:27):

I think you want strict inequality in the definition of is_strictly_between right?

view this post on Zulip Adam Topaz (Dec 01 2020 at 20:28):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Dec 01 2020 at 21:05):

Ooh polymake looks cool!

view this post on Zulip 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.

view this post on Zulip Reid Barton (Dec 01 2020 at 21:11):

Does this problem have easily checkable certificates?

view this post on Zulip 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