convex hulls and compact convex sets

Stream: Is there code for X?

[Damiano Testa]

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.

[Damiano Testa]

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!

[Bhavik Mehta]

@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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Damiano Testa]

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!

[Damiano Testa]

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

[Bhavik Mehta]

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 :)

[Damiano Testa]

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

[Bhavik Mehta]

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

[Damiano Testa]

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

[David Wärn]

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

[Damiano Testa]

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!

[Yaël Dillies]

@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.

[Damiano Testa]

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

Thanks a lot!

[Yaël Dillies]

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

[Yaël Dillies]

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?

[Damiano Testa]

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

Thank you so much!

[Damiano Testa]

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.

[Yaël Dillies]

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

[Damiano Testa]

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

[Bhavik Mehta]

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!

[Bhavik Mehta]

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

[Johan Commelin]

Great work! Thanks a lot!

[Damiano Testa]

This is really impressive: thank you very much!

[Patrick Massot]

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?

[Yaël Dillies]

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

[David Wärn]

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.