# The Krein-Milman theorem #

This file proves the Krein-Milman lemma and the Krein-Milman theorem.

## The lemma #

The lemma states that a nonempty compact set `s`

has an extreme point. The proof goes:

- Using Zorn's lemma, find a minimal nonempty closed
`t`

that is an extreme subset of`s`

. We will show that`t`

is a singleton, thus corresponding to an extreme point. - By contradiction,
`t`

contains two distinct points`x`

and`y`

. - With the (geometric) Hahn-Banach theorem, find a hyperplane that separates
`x`

and`y`

. - Look at the extreme (actually exposed) subset of
`t`

obtained by going the furthest away from the separating hyperplane in the direction of`x`

. It is nonempty, closed and an extreme subset of`s`

. - It is a strict subset of
`t`

(`y`

isn't in it), so`t`

isn't minimal. Absurd.

## The theorem #

The theorem states that a compact convex set `s`

is the closure of the convex hull of its extreme
points. It is an almost immediate strengthening of the lemma. The proof goes:

- By contradiction,
`s \ closure (convexHull ℝ (extremePoints ℝ s))`

is nonempty, say with`x`

. - With the (geometric) Hahn-Banach theorem, find a hyperplane that separates
`x`

from`closure (convexHull ℝ (extremePoints ℝ s))`

. - Look at the extreme (actually exposed) subset of
`s \ closure (convexHull ℝ (extremePoints ℝ s))`

obtained by going the furthest away from the separating hyperplane. It is nonempty by assumption of nonemptiness and compactness, so by the lemma it has an extreme point. - This point is also an extreme point of
`s`

. Absurd.

## Related theorems #

When the space is finite dimensional, the `closure`

can be dropped to strengthen the result of the
Krein-Milman theorem. This leads to the Minkowski-Carathéodory theorem (currently not in mathlib).
Birkhoff's theorem is the Minkowski-Carathéodory theorem applied to the set of bistochastic
matrices, permutation matrices being the extreme points.

## References #

See chapter 8 of Barry Simon, *Convexity*

**Krein-Milman lemma**: In a LCTVS, any nonempty compact set has an extreme point.

**Krein-Milman theorem**: In a LCTVS, any compact convex set is the closure of the convex hull
of its extreme points.

A continuous affine map is surjective from the extreme points of a compact set to the extreme points of the image of that set. This inclusion is in general strict.