Documentation

Mathlib.Analysis.Convex.KreinMilman

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 a 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 (convexHull ℝ (extremePoints ℝ s)) is nonempty, say with x.
  2. With the (geometric) Hahn-Banach theorem, find a hyperplane that separates x from closure (convexHull ℝ (extremePoints ℝ s)).
  3. 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.
  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][simon2011]

source
theorem IsCompact.extremePoints_nonempty {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [T2Space E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {s : Set E} (hscomp : IsCompact s) (hsnemp : s.Nonempty) :
(Set.extremePoints ℝ s).Nonempty

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

source
theorem closure_convexHull_extremePoints {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [T2Space E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {s : Set E} (hscomp : IsCompact s) (hAconv : Convex ℝ s) :
closure ((convexHull ℝ) (Set.extremePoints ℝ s)) = s

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

source
theorem surjOn_extremePoints_image {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [T2Space E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {s : Set E} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [T1Space F] (f : E →ᴬ[ℝ] F) (hs : IsCompact s) :
Set.SurjOn (⇑f) (Set.extremePoints ℝ s) (Set.extremePoints ℝ (⇑f '' s))

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.