Zulip Chat Archive

Stream: Is there code for X?

Topic: convex hulls and compact convex sets


view this post on Zulip Damiano Testa (Apr 11 2021 at 10:44):

Dear All,

in the process ot proving Gordan's lemma, one of the tools that would be useful to have is the version below of the Krein-Milman: does it appear already in mathlib, in one form or another?

Thanks!

Let K be a compact, convex subset of a finite-dimensional real vector space. Then, K is the convex hull of its extreme points.

view this post on Zulip Damiano Testa (Apr 11 2021 at 10:45):

Note: I am happy to assume further nice properties about K: for instance, in the application to Gordan's lemma, the set K is cut out by finitely many linear inequalities.

Thus, if something is close to this result, it might already be enough for my purposes!

view this post on Zulip Bhavik Mehta (Apr 11 2021 at 15:09):

@Yaël Dillies and I have some results in this direction, but not quite as general as you're looking for, I think: https://github.com/leanprover-community/mathlib/blob/sperner-again/src/combinatorics/simplicial_complex/extreme_point.lean

view this post on Zulip Bhavik Mehta (Apr 11 2021 at 15:11):

Specifically

lemma eq_of_convex_hull_eq_convex_hull_of_linearly_independent
  {X Y : finset E}
  (hX : affine_independent  (λ p, p : (X : set E)  E))
  (hY : affine_independent  (λ p, p : (Y : set E)  E))
  (h : convex_hull (X : set E) = convex_hull (Y : set E)) :
  X = Y :=

which says that if two affinely independent finite sets in a normed space have the same convex hull, then they're the same

view this post on Zulip Bhavik Mehta (Apr 11 2021 at 15:12):

As well as

lemma mem_of_is_extreme_to_convex_hull {X : set E} {x : E} (hx : is_extreme (convex_hull X) x) :
  x  X :=

ie that if x is an extreme point of the convex hull of X, then it's in X

view this post on Zulip Bhavik Mehta (Apr 11 2021 at 15:14):

I think this gives the special case of Krein-Milman for simplices?

view this post on Zulip Bhavik Mehta (Apr 11 2021 at 15:19):

If that's not strong enough I think it wouldn't be too hard to formalise the proof here: http://mathonline.wikidot.com/the-krein-milman-theorem

view this post on Zulip Damiano Testa (Apr 11 2021 at 16:40):

Bhavik, thank you very much! I am glad to see that there is stuff in this direction already in mathlib!

In my intended application, the set is given by finitely many linear inequalities. However, I would want to use this result for any finite set of affine linear inequalities. So, if I am going to follow this route, I would have to formalize the more general version first.

Thanks!

view this post on Zulip Damiano Testa (Apr 11 2021 at 16:43):

I also think that this gives Krein-Milman for simplices. In the toric analogy, these are, I think, the Q\mathbb{Q}-factorial toric varieties, while I would really want all toric varieties...

view this post on Zulip Bhavik Mehta (Apr 11 2021 at 16:47):

Damiano Testa said:

Bhavik, thank you very much! I am glad to see that there is stuff in this direction already in mathlib!

In my intended application, the set is given by finitely many linear inequalities. However, I would want to use this result for any finite set of affine linear inequalities. So, if I am going to follow this route, I would have to formalize the more general version first.

Thanks!

It's not yet in mathlib, it's just in a branch for now - we'll PR it soon :)

view this post on Zulip Damiano Testa (Apr 11 2021 at 16:51):

Ah, ok! Anyway, the application that I have in mind is in lean-liquid, which also is not in mathlib!

view this post on Zulip Bhavik Mehta (Apr 11 2021 at 18:21):

Damiano Testa said:

Note: I am happy to assume further nice properties about K: for instance, in the application to Gordan's lemma, the set K is cut out by finitely many linear inequalities.

Thus, if something is close to this result, it might already be enough for my purposes!

Thinking about this a bit more, perhaps my result in combination with Caratheodory's lemma might help? Specifically I think you could show that if K is the convex hull of finitely many points, then those points are the extreme points of K, by considering the (d+1)-tuples of K - though again maybe this still isn't strong enough

view this post on Zulip Damiano Testa (Apr 11 2021 at 19:05):

Hmm, I would have to think if Caratheodory's lemma is enough. I do not see a direct argument, straight away...

view this post on Zulip David Wärn (Apr 11 2021 at 21:59):

Farkas lemma might be what you want?
http://www.ma.rhul.ac.uk/~uvah099/Maths/Farkas.pdf

view this post on Zulip Damiano Testa (Apr 12 2021 at 01:29):

David, thank you! I would have to think a little, but I had forgotten about Farkas's lemma and i do believe that this would work!

Thank you so much!

view this post on Zulip Yaël Dillies (Apr 13 2021 at 08:13):

@Bhavik Mehta and I are now on our way to prove Krein-Milman for normed spaces, because locally convex topological vector spaces aren't yet in mathlib. Is that general enough for you? If not, I guess we could ask someone to write an API for LCTVS and then it should be a matter of minutes to adapt the file we're currently writing.

view this post on Zulip Damiano Testa (Apr 13 2021 at 08:24):

Yaël, normed spaces would be enough: I want to apply this result to finite dimensional real vector spaces!

Thanks a lot!

view this post on Zulip Yaël Dillies (Apr 13 2021 at 14:17):

Okay great! I'll keep you updated. I've never PRed, so this will be fun!

view this post on Zulip Yaël Dillies (Apr 15 2021 at 18:30):

The implication from the geometrical version to Hahn-Banach to Krein-Milman is now done! Bhavik Mehta is currently proving the said Hahn-Banach. If anybody has ideas of what to add to our files about extreme and exposed sets, feel free to tell. In particular, @Damiano Testa, is there anything you should know about the set of extreme points of convex hulls?

view this post on Zulip Damiano Testa (Apr 15 2021 at 18:34):

That is great! I will take a look, though not today!

Thank you so much!

view this post on Zulip Damiano Testa (Apr 15 2021 at 18:35):

Btw... where is this? I tried the link above

(https://github.com/leanprover-community/mathlib/blob/sperner-again/src/combinatorics/simplicial_complex/extreme_point.lean)

but it does not work for me.

view this post on Zulip Yaël Dillies (Apr 15 2021 at 18:42):

Ah sorry I've shuffled files around since we posted this link. Here's the one: https://github.com/leanprover-community/mathlib/blob/sperner-again/src/combinatorics/simplicial_complex/krein-milman.lean

view this post on Zulip Damiano Testa (Apr 15 2021 at 18:53):

Thanks! I will need some time to digest it, but this looks very good!

view this post on Zulip Bhavik Mehta (Apr 15 2021 at 19:13):

Yup, I've almost finished the two sorried statements at the top in a different branch, which I'll try to PR to mathlib directly!

view this post on Zulip Bhavik Mehta (Apr 15 2021 at 23:19):

Now finished, specifically the following statements (all for normed spaces):

theorem geometric_hahn_banach_open {A B : set E}
  (hA₂ : convex A) (hA₃ : is_open A) (hB₂ : convex B)
  (disj : disjoint A B) :
 (f : E L[] ) (s : ), ( a  A, f a < s)  ( b  B, s  f b) := ...

theorem geometric_hahn_banach_open_open {A B : set E}
  (hA₂ : convex A) (hA₃ : is_open A) (hB₂ : convex B) (hB₃ : is_open B)
  (disj : disjoint A B) :
 (f : E L[] ) (s : ), ( a  A, f a < s)  ( b  B, s < f b) := ...

theorem geometric_hahn_banach_closed_closed_compact {A B : set E}
  (hA₂ : convex A) (hA₄ : is_compact A) (hB₂ : convex B) (hA₃ : is_closed B)
  (disj : disjoint A B) :
   (f : E L[] ) (s t : ), ( a  A, f a < s)  s < t  ( b  B, t < f b) := ...

theorem geometric_hahn_banach_point_point {x y : E} (hxy : x  y) :
   (f : E L[] ), f x < f y := ...

so now Krein-Milman should be entirely sorry-free

view this post on Zulip Johan Commelin (Apr 16 2021 at 03:43):

Great work! Thanks a lot!

view this post on Zulip Damiano Testa (Apr 16 2021 at 05:28):

This is really impressive: thank you very much!

view this post on Zulip Patrick Massot (Apr 17 2021 at 10:07):

What happened to @Yury G. Kudryashov convexity refactor from last summer? Did it ever reach mathlib? Or are we still adding stuff that would need to be refactored?

view this post on Zulip Yaël Dillies (Apr 17 2021 at 11:39):

What was this refactor about? Is it because we haven't yet defined LCTVS?

view this post on Zulip David Wärn (Apr 17 2021 at 19:34):

I wonder if these results can also be used to close #2601? "Strong duality for linear programming" should be a corollary of this stuff, at least over the reals.


Last updated: May 17 2021 at 15:13 UTC