Convex independence #

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

This file defines convex independent families of points.

Convex independence is closely related to affine independence. In both cases, no point can be written as a combination of others. When the combination is affine (that is, any coefficients), this yields affine independence. When the combination is convex (that is, all coefficients are nonnegative), then this yields convex independence. In particular, affine independence implies convex independence.

Main declarations #

convex_independent p: Convex independence of the indexed family p : ι → E. Every point of the family only belongs to convex hulls of sets of the family containing it.
convex_independent_iff_finset: Carathéodory's theorem allows us to only check finsets to conclude convex independence.
convex.extreme_points_convex_independent: Extreme points of a convex set are convex independent.

References #

https://en.wikipedia.org/wiki/Convex_position

TODO #

Prove affine_independent.convex_independent. This requires some glue between affine_combination and finset.center_mass.

Tags #

independence, convex position

source

def convex_independent (𝕜 : Type u_1) {E : Type u_2} {ι : Type u_3} [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] (p : ι → E) :

Prop

An indexed family is said to be convex independent if every point only belongs to convex hulls of sets containing it.

Equations

convex_independent 𝕜 p = ∀ (s : set ι) (x : ι), p x ∈ ⇑(convex_hull 𝕜) (p '' s) → x ∈ s

source

theorem subsingleton.convex_independent {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] [subsingleton ι] (p : ι → E) :

convex_independent 𝕜 p

A family with at most one point is convex independent.

source

@[protected]

theorem convex_independent.injective {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] {p : ι → E} (hc : convex_independent 𝕜 p) :

function.injective p

A convex independent family is injective.

source

theorem convex_independent.comp_embedding {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] {ι' : Type u_4} (f : ι' ↪ ι) {p : ι → E} (hc : convex_independent 𝕜 p) :

convex_independent 𝕜 (p ∘ ⇑f)

If a family is convex independent, so is any subfamily given by composition of an embedding into index type with the original family.

source

@[protected]

theorem convex_independent.subtype {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] {p : ι → E} (hc : convex_independent 𝕜 p) (s : set ι) :

convex_independent 𝕜 (λ (i : ↥s), p ↑i)

If a family is convex independent, so is any subfamily indexed by a subtype of the index type.

source

@[protected]

theorem convex_independent.range {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] {p : ι → E} (hc : convex_independent 𝕜 p) :

convex_independent 𝕜 (λ (x : ↥(set.range p)), ↑x)

If an indexed family of points is convex independent, so is the corresponding set of points.

source

@[protected]

theorem convex_independent.mono {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] {s t : set E} (hc : convex_independent 𝕜 (λ (x : ↥t), ↑x)) (hs : s ⊆ t) :

convex_independent 𝕜 (λ (x : ↥s), ↑x)

A subset of a convex independent set of points is convex independent as well.

source

theorem function.injective.convex_independent_iff_set {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] {p : ι → E} (hi : function.injective p) :

convex_independent 𝕜 (λ (x : ↥(set.range p)), ↑x) ↔ convex_independent 𝕜 p

The range of an injective indexed family of points is convex independent iff that family is.

source

@[protected, simp]

theorem convex_independent.mem_convex_hull_iff {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] {p : ι → E} (hc : convex_independent 𝕜 p) (s : set ι) (i : ι) :

p i ∈ ⇑(convex_hull 𝕜) (p '' s) ↔ i ∈ s

If a family is convex independent, a point in the family is in the convex hull of some of the points given by a subset of the index type if and only if the point's index is in this subset.

source

theorem convex_independent_iff_not_mem_convex_hull_diff {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] {p : ι → E} :

convex_independent 𝕜 p ↔ ∀ (i : ι) (s : set ι), p i ∉ ⇑(convex_hull 𝕜) (p '' (s \ {i}))

If a family is convex independent, a point in the family is not in the convex hull of the other points. See convex_independent_set_iff_not_mem_convex_hull_diff for the set version.

source

theorem convex_independent_set_iff_inter_convex_hull_subset {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} :

convex_independent 𝕜 (λ (x : ↥s), ↑x) ↔ ∀ (t : set E), t ⊆ s → s ∩ ⇑(convex_hull 𝕜) t ⊆ t

source

theorem convex_independent_set_iff_not_mem_convex_hull_diff {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} :

convex_independent 𝕜 (λ (x : ↥s), ↑x) ↔ ∀ (x : E), x ∈ s → x ∉ ⇑(convex_hull 𝕜) (s \ {x})

If a set is convex independent, a point in the set is not in the convex hull of the other points. See convex_independent_iff_not_mem_convex_hull_diff for the indexed family version.

source

theorem convex_independent_iff_finset {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {p : ι → E} :

convex_independent 𝕜 p ↔ ∀ (s : finset ι) (x : ι), p x ∈ ⇑(convex_hull 𝕜) ↑(finset.image p s) → x ∈ s

To check convex independence, one only has to check finsets thanks to Carathéodory's theorem.

Extreme points #

source

theorem convex.convex_independent_extreme_points {𝕜 : Type u_1} {E : Type u_2} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} (hs : convex 𝕜 s) :

convex_independent 𝕜 (λ (p : ↥(set.extreme_points 𝕜 s)), ↑p)