mathlib documentation

analysis.convex.extreme

Extreme sets #

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 #

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 #

Define intrinsic frontier and prove lemmas related to extreme sets and points.

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

def is_extreme (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ 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
def set.extreme_points (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ 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]
theorem is_extreme.refl (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] (A : set E) :
is_extreme π•œ A A
@[protected]
theorem is_extreme.rfl {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] {A : set E} :
is_extreme π•œ A A
@[protected]
theorem is_extreme.trans {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] {A B C : set E} (hAB : is_extreme π•œ A B) (hBC : is_extreme π•œ B C) :
is_extreme π•œ A C
@[protected]
theorem is_extreme.antisymm {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] :
@[protected, instance]
def is_extreme.is_partial_order {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] :
theorem is_extreme.inter {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] {A B C : set E} (hAB : is_extreme π•œ A B) (hAC : is_extreme π•œ A C) :
is_extreme π•œ A (B ∩ C)
@[protected]
theorem is_extreme.mono {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] {A B C : set E} (hAC : is_extreme π•œ A C) (hBA : B βŠ† A) (hCB : C βŠ† B) :
is_extreme π•œ B C
theorem is_extreme_Inter {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] {A : set E} {ΞΉ : Type u_3} [nonempty ΞΉ] {F : ΞΉ β†’ set E} (hAF : βˆ€ (i : ΞΉ), is_extreme π•œ A (F i)) :
is_extreme π•œ A (β‹‚ (i : ΞΉ), F i)
theorem is_extreme_bInter {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] {A : set E} {F : set (set E)} (hF : F.nonempty) (hAF : βˆ€ (B : set E), B ∈ F β†’ is_extreme π•œ A B) :
is_extreme π•œ A (β‹‚ (B : set E) (H : B ∈ F), B)
theorem is_extreme_sInter {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] {A : set E} {F : set (set E)} (hF : F.nonempty) (hAF : βˆ€ (B : set E), B ∈ F β†’ is_extreme π•œ A B) :
is_extreme π•œ A (β‹‚β‚€F)
theorem extreme_points_def {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] {A : set E} {x : E} :
x ∈ set.extreme_points π•œ A ↔ x ∈ A ∧ βˆ€ (x₁ xβ‚‚ : E), x₁ ∈ A β†’ xβ‚‚ ∈ A β†’ x ∈ open_segment π•œ x₁ xβ‚‚ β†’ x₁ = x ∧ xβ‚‚ = x
theorem mem_extreme_points_iff_extreme_singleton {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] {A : set E} {x : E} :
x ∈ set.extreme_points π•œ A ↔ is_extreme π•œ 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} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] {A : set E} :
@[simp]
theorem extreme_points_empty {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] :
@[simp]
theorem extreme_points_singleton {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] {x : E} :
set.extreme_points π•œ {x} = {x}
theorem inter_extreme_points_subset_extreme_points_of_subset {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] {A B : set E} (hBA : B βŠ† A) :
theorem is_extreme.extreme_points_subset_extreme_points {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] {A B : set E} (hAB : is_extreme π•œ A B) :
theorem is_extreme.extreme_points_eq {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] {A B : set E} (hAB : is_extreme π•œ A B) :
theorem is_extreme.convex_diff {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_group E] [module π•œ E] {A B : set E} (hA : convex π•œ A) (hAB : is_extreme π•œ A B) :
convex π•œ (A \ B)
theorem mem_extreme_points_iff_forall_segment {π•œ : Type u_1} {E : Type u_2} [linear_ordered_field π•œ] [add_comm_group E] [module π•œ E] {A : set E} {x : E} [no_zero_smul_divisors π•œ E] :
x ∈ set.extreme_points π•œ A ↔ x ∈ A ∧ βˆ€ (x₁ xβ‚‚ : E), x₁ ∈ A β†’ 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} [linear_ordered_field π•œ] [add_comm_group E] [module π•œ E] {A : set E} {x : E} (hA : convex π•œ A) :
x ∈ set.extreme_points π•œ A ↔ x ∈ A ∧ convex π•œ (A \ {x})
theorem convex.mem_extreme_points_iff_mem_diff_convex_hull_diff {π•œ : Type u_1} {E : Type u_2} [linear_ordered_field π•œ] [add_comm_group E] [module π•œ E] {A : set E} {x : E} (hA : convex π•œ A) :
x ∈ set.extreme_points π•œ A ↔ x ∈ A \ ⇑(convex_hull π•œ) (A \ {x})
theorem extreme_points_convex_hull_subset {π•œ : Type u_1} {E : Type u_2} [linear_ordered_field π•œ] [add_comm_group E] [module π•œ E] {A : set E} :
set.extreme_points π•œ (⇑(convex_hull π•œ) A) βŠ† A