## Stream: Is there code for X?

### Topic: convex hulls and compact convex sets

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

#### 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!

#### 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

#### 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

#### 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

#### Bhavik Mehta (Apr 11 2021 at 15:14):

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

#### 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

#### 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!

#### 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 $\mathbb{Q}$-factorial toric varieties, while I would really want all toric varieties...

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

#### 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!

#### 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

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

#### 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

#### 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!

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

#### 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!

#### 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!

#### 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?

#### Damiano Testa (Apr 15 2021 at 18:34):

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

Thank you so much!

#### Damiano Testa (Apr 15 2021 at 18:35):

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

but it does not work for me.

#### 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

#### Damiano Testa (Apr 15 2021 at 18:53):

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

#### 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!

#### 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

#### Johan Commelin (Apr 16 2021 at 03:43):

Great work! Thanks a lot!

#### Damiano Testa (Apr 16 2021 at 05:28):

This is really impressive: thank you very much!

#### 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?