closure_convexHull_extremePoints
theorem closure_convexHull_extremePoints :
∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [inst_3 : T2Space E]
[inst_4 : TopologicalAddGroup E] [inst_5 : ContinuousSMul ℝ E] [inst_6 : LocallyConvexSpace ℝ E] {s : Set E},
IsCompact s → Convex ℝ s → closure ((convexHull ℝ) (Set.extremePoints ℝ s)) = s
The **Krein-Milman theorem** states that, in a locally convex topological vector space (LCTVS), any compact convex set can be represented as the closure of the convex hull of its extreme points. In other words, if we have a set that is both compact (for any nontrivial filter that contains the set, there exists a point in the set such that every set of the filter meets every neighborhood of this point) and convex (for any point in the set, the set is star-convex with respect to this point), then the smallest closed set containing the hull of the points that belong to no open segment with ends in the set, except for the trivial open segment from a point to itself, is the set itself.
More concisely: In a locally convex topological vector space, a compact convex set is the closure of its extreme points.
|
IsCompact.extremePoints_nonempty
theorem IsCompact.extremePoints_nonempty :
∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [inst_3 : T2Space E]
[inst_4 : TopologicalAddGroup E] [inst_5 : ContinuousSMul ℝ E] [inst_6 : LocallyConvexSpace ℝ E] {s : Set E},
IsCompact s → s.Nonempty → (Set.extremePoints ℝ s).Nonempty
The **Krein-Milman lemma** states that for any nonempty compact set in a real Locally Convex Topological Vector Space (LCTVS), there is at least one extreme point. In other words, given a nonempty compact set in such a space, there exists a point in the set that belongs to no open segment with ends in the set, except for the open segment from the point to itself.
More concisely: In a real Locally Convex Topological Vector Space, every nonempty compact set has at least one extreme point, which is a point not in any open line segment with ends in the set, except for the segment from the point to itself.
|
surjOn_extremePoints_image
theorem surjOn_extremePoints_image :
∀ {E : Type u_1} {F : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E]
[inst_3 : T2Space E] [inst_4 : TopologicalAddGroup E] [inst_5 : ContinuousSMul ℝ E]
[inst_6 : LocallyConvexSpace ℝ E] {s : Set E} [inst_7 : AddCommGroup F] [inst_8 : Module ℝ F]
[inst_9 : TopologicalSpace F] [inst_10 : T1Space F] (f : E →A[ℝ] F),
IsCompact s → Set.SurjOn (⇑f) (Set.extremePoints ℝ s) (Set.extremePoints ℝ (⇑f '' s))
The theorem `surjOn_extremePoints_image` states that for any continuous affine map `f`, if a set `s` is compact (that is, for every nontrivial filter `f` that contains `s`, there exists a point `a` in `s` such that every set of `f` meets every neighborhood of `a`), then `f` is surjective from the extreme points of `s` to the extreme points of the image of `s`. The extreme points of a set `A` are those points which belong to no open segment with ends in `A`, except for the segment from a point to itself. This inclusion of extreme points in the image is generally not an equality, meaning that the image may have additional extreme points not in the preimage.
More concisely: If a continuous affine map `f` maps the extreme points of a compact set `s` to the extreme points of `f(s)`.
|