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 #

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 #

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_smul 𝕜 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

is_extreme 𝕜 A B = (B ⊆ A ∧ ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → ∀ ⦃x : E⦄, x ∈ B → x ∈ open_segment 𝕜 x₁ x₂ → x₁ ∈ B ∧ x₂ ∈ B)

Instances for is_extreme

is_extreme.is_partial_order

def set.extreme_points (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] (A : 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

set.extreme_points 𝕜 A = {x ∈ A | ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → x ∈ open_segment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x}

@[protected, refl]

theorem is_extreme.refl (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 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_smul 𝕜 E] {A : set E} :

is_extreme 𝕜 A A

@[protected, trans]

theorem is_extreme.trans {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 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_smul 𝕜 E] :

anti_symmetric (is_extreme 𝕜)

@[protected, instance]

def is_extreme.is_partial_order {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] :

is_partial_order (set E) (is_extreme 𝕜)

theorem is_extreme.inter {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 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_smul 𝕜 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_smul 𝕜 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_smul 𝕜 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_smul 𝕜 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_smul 𝕜 E] {A : set E} {x : E} :

x ∈ set.extreme_points 𝕜 A ↔ x ∈ A ∧ ∀ (x₁ : E), x₁ ∈ A → ∀ (x₂ : E), 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_smul 𝕜 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_smul 𝕜 E] {A : set E} :

set.extreme_points 𝕜 A ⊆ A

@[simp]

theorem extreme_points_empty {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] :

set.extreme_points 𝕜 ∅ = ∅

@[simp]

theorem extreme_points_singleton {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 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_smul 𝕜 E] {A B : set E} (hBA : B ⊆ A) :

B ∩ set.extreme_points 𝕜 A ⊆ set.extreme_points 𝕜 B

theorem is_extreme.extreme_points_subset_extreme_points {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] {A B : set E} (hAB : is_extreme 𝕜 A B) :

set.extreme_points 𝕜 B ⊆ set.extreme_points 𝕜 A

theorem is_extreme.extreme_points_eq {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] {A B : set E} (hAB : is_extreme 𝕜 A B) :

set.extreme_points 𝕜 B = B ∩ set.extreme_points 𝕜 A

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_ring 𝕜] [add_comm_group E] [module 𝕜 E] [densely_ordered 𝕜] [no_zero_smul_divisors 𝕜 E] {A : set E} {x : E} :

x ∈ set.extreme_points 𝕜 A ↔ x ∈ A ∧ ∀ (x₁ : E), x₁ ∈ A → ∀ (x₂ : E), x₂ ∈ A → x ∈ segment 𝕜 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_ring 𝕜] [add_comm_group E] [module 𝕜 E] [densely_ordered 𝕜] [no_zero_smul_divisors 𝕜 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_ring 𝕜] [add_comm_group E] [module 𝕜 E] [densely_ordered 𝕜] [no_zero_smul_divisors 𝕜 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_ring 𝕜] [add_comm_group E] [module 𝕜 E] [densely_ordered 𝕜] [no_zero_smul_divisors 𝕜 E] {A : set E} :

set.extreme_points 𝕜 (⇑(convex_hull 𝕜) A) ⊆ A