mathlib documentation

analysis.convex.independent

Convex independence #

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 #

References #

TODO #

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

Tags #

independence, convex position

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
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) :

A family with at most one point is convex independent.

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) :

A convex independent family is injective.

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) :

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

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.

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.

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.

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) :

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

@[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.

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.

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 ss (convex_hull 𝕜) t t
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 sx (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.

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 #

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)