mathlib3documentation

analysis.convex.extreme

Extreme sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines extreme sets and extreme points for sets in a module.

An extreme set of A is a subset of A that is as far as it can get in any outward direction: If point x is in it and point y ∈ A, then the line passing through x and y leaves A at x. This is an analytic notion of "being on the side of". It is weaker than being exposed (see is_exposed.is_extreme).

Main declarations #

• is_extreme 𝕜 A B: States that B is an extreme set of A (in the literature, A is often implicit).
• set.extreme_points 𝕜 A: Set of extreme points of A (corresponding to extreme singletons).
• convex.mem_extreme_points_iff_convex_diff: A useful equivalent condition to being an extreme point: x is an extreme point iff A \ {x} is convex.

Implementation notes #

The exact definition of extremeness has been carefully chosen so as to make as many lemmas unconditional (in particular, the Krein-Milman theorem doesn't need the set to be convex!). In practice, A is often assumed to be a convex set.

References #

See chapter 8 of Barry Simon, Convexity

TODO #

Prove lemmas relating extreme sets and points to the intrinsic frontier.

More not-yet-PRed stuff is available on the branch sperner_again.

def is_extreme (𝕜 : Type u_1) {E : Type u_2} [ E] (A B : set E) :
Prop

A set B is an extreme subset of A if B ⊆ A and all points of B only belong to open segments whose ends are in B.

Equations
Instances for is_extreme
def set.extreme_points (𝕜 : Type u_1) {E : Type u_2} [ E] (A : set E) :
set E

A point x is an extreme point of a set A if x belongs to no open segment with ends in A, except for the obvious open_segment x x.

Equations
@[protected, refl]
theorem is_extreme.refl (𝕜 : Type u_1) {E : Type u_2} [ E] (A : set E) :
A A
@[protected]
theorem is_extreme.rfl {𝕜 : Type u_1} {E : Type u_2} [ E] {A : set E} :
A A
@[protected, trans]
theorem is_extreme.trans {𝕜 : Type u_1} {E : Type u_2} [ E] {A B C : set E} (hAB : A B) (hBC : B C) :
A C
@[protected]
theorem is_extreme.antisymm {𝕜 : Type u_1} {E : Type u_2} [ E] :
@[protected, instance]
def is_extreme.is_partial_order {𝕜 : Type u_1} {E : Type u_2} [ E] :
(is_extreme 𝕜)
theorem is_extreme.inter {𝕜 : Type u_1} {E : Type u_2} [ E] {A B C : set E} (hAB : A B) (hAC : A C) :
A (B C)
@[protected]
theorem is_extreme.mono {𝕜 : Type u_1} {E : Type u_2} [ E] {A B C : set E} (hAC : A C) (hBA : B A) (hCB : C B) :
B C
theorem is_extreme_Inter {𝕜 : Type u_1} {E : Type u_2} [ E] {A : set E} {ι : Sort u_3} [nonempty ι] {F : ι set E} (hAF : (i : ι), A (F i)) :
A ( (i : ι), F i)
theorem is_extreme_bInter {𝕜 : Type u_1} {E : Type u_2} [ E] {A : set E} {F : set (set E)} (hF : F.nonempty) (hA : (B : set E), B F A B) :
A ( (B : set E) (H : B F), B)
theorem is_extreme_sInter {𝕜 : Type u_1} {E : Type u_2} [ E] {A : set E} {F : set (set E)} (hF : F.nonempty) (hAF : (B : set E), B F A B) :
A (⋂₀ F)
theorem mem_extreme_points {𝕜 : Type u_1} {E : Type u_2} [ E] {A : set E} {x : E} :
x x A (x₁ : E), x₁ A (x₂ : E), x₂ A x x₁ x₂ x₁ = x x₂ = x
theorem mem_extreme_points_iff_extreme_singleton {𝕜 : Type u_1} {E : Type u_2} [ E] {A : set E} {x : E} :
x A {x}

x is an extreme point to A iff {x} is an extreme set of A.

theorem extreme_points_subset {𝕜 : Type u_1} {E : Type u_2} [ E] {A : set E} :
A
@[simp]
theorem extreme_points_empty {𝕜 : Type u_1} {E : Type u_2} [ E] :
@[simp]
theorem extreme_points_singleton {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} :
{x} = {x}
theorem inter_extreme_points_subset_extreme_points_of_subset {𝕜 : Type u_1} {E : Type u_2} [ E] {A B : set E} (hBA : B A) :
B
theorem is_extreme.extreme_points_subset_extreme_points {𝕜 : Type u_1} {E : Type u_2} [ E] {A B : set E} (hAB : A B) :
theorem is_extreme.extreme_points_eq {𝕜 : Type u_1} {E : Type u_2} [ E] {A B : set E} (hAB : A B) :
= B
theorem is_extreme.convex_diff {𝕜 : Type u_1} {E : Type u_2} [ E] {A B : set E} (hA : A) (hAB : A B) :
(A \ B)
@[simp]
theorem extreme_points_prod {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] (s : set E) (t : set F) :
(s ×ˢ t) =
@[simp]
theorem extreme_points_pi {𝕜 : Type u_1} {ι : Type u_4} {π : ι Type u_5} [Π (i : ι), add_comm_group (π i)] [Π (i : ι), (π i)] (s : Π (i : ι), set (π i)) :
(set.univ.pi s) = set.univ.pi (λ (i : ι), (s i))
theorem mem_extreme_points_iff_forall_segment {𝕜 : Type u_1} {E : Type u_2} [ E] {A : set E} {x : E} :
x x A (x₁ : E), x₁ A (x₂ : E), x₂ A x x₁ x₂ x₁ = x x₂ = x

A useful restatement using segment: x is an extreme point iff the only (closed) segments that contain it are those with x as one of their endpoints.

theorem convex.mem_extreme_points_iff_convex_diff {𝕜 : Type u_1} {E : Type u_2} [ E] {A : set E} {x : E} (hA : A) :
x x A (A \ {x})
theorem convex.mem_extreme_points_iff_mem_diff_convex_hull_diff {𝕜 : Type u_1} {E : Type u_2} [ E] {A : set E} {x : E} (hA : A) :
x x A \ (convex_hull 𝕜) (A \ {x})
theorem extreme_points_convex_hull_subset {𝕜 : Type u_1} {E : Type u_2} [ E] {A : set E} :
((convex_hull 𝕜) A) A