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: Dec 20 2023 at 11:08 UTC