mathlib documentation

analysis.convex.krein_milman

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:

  1. 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.
  2. By contradiction, t contains two distinct points x and y.
  3. With the (geometric) Hahn-Banach theorem, find an hyperplane that separates x and y.
  4. 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.
  5. 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:

  1. By contradiction, s \ closure (convex_hull ℝ (extreme_points ℝ s)) is nonempty, say with x.
  2. With the (geometric) Hahn-Banach theorem, find an hyperplane that separates x from closure (convex_hull ℝ (extreme_points ℝ s)).
  3. Look at the extreme (actually exposed) subset of s \ closure (convex_hull ℝ (extreme_points ℝ 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.
  4. This point is also an extreme point of s. Absurd.

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

TODO #

source
theorem is_compact.has_extreme_point {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {s : set E} (hscomp : is_compact s) (hsnemp : s.nonempty) :
(set.extreme_points ℝ s).nonempty

Krein-Milman lemma: In a LCTVS (currently only in normed ℝ-spaces), any nonempty compact set has an extreme point.

source
theorem closure_convex_hull_extreme_points {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {s : set E} (hscomp : is_compact s) (hAconv : convex ℝ s) :
closure (⇑(convex_hull ℝ) (set.extreme_points ℝ s)) = s

Krein-Milman theorem: In a LCTVS (currently only in normed ℝ-spaces), any compact convex set is the closure of the convex hull of its extreme points.