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

• ConvexIndependent 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.
• convexIndependent_iff_finset: Carathéodory's theorem allows us to only check finsets to conclude convex independence.
• Convex.convexIndependent_extremePoints: Extreme points of a convex set are convex independent.

References

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

TODO

Prove AffineIndependent.convexIndependent. This requires some glue between affineCombination and Finset.centerMass.

Tags

independence, convex position

def ConvexIndependent (𝕜 : Type u_1) {E : Type u_2} {ι : Type u_3} [OrderedSemiring 𝕜] [AddCommGroup 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

• ConvexIndependent 𝕜 p = ∀ (s : Set ι) (x : ι), p x ∈ (convexHull 𝕜) (p '' s) → x ∈ s

theorem Subsingleton.convexIndependent {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [OrderedSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] [Subsingleton ι] (p : ι → E) : ConvexIndependent 𝕜 p

A family with at most one point is convex independent.

theorem ConvexIndependent.injective {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [OrderedSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : ι → E} (hc : ConvexIndependent 𝕜 p) : Function.Injective p

A convex independent family is injective.

theorem ConvexIndependent.comp_embedding {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [OrderedSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] {ι' : Type u_4} (f : ι' ↪ ι) {p : ι → E} (hc : ConvexIndependent 𝕜 p) : ConvexIndependent 𝕜 (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.

theorem ConvexIndependent.subtype {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [OrderedSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : ι → E} (hc : ConvexIndependent 𝕜 p) (s : Set ι) : ConvexIndependent 𝕜 fun (i : ↑s) => p ↑i

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

theorem ConvexIndependent.range {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [OrderedSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : ι → E} (hc : ConvexIndependent 𝕜 p) : ConvexIndependent 𝕜 Subtype.val

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

theorem ConvexIndependent.mono {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] {s t : Set E} (hc : ConvexIndependent 𝕜 Subtype.val) (hs : s ⊆ t) : ConvexIndependent 𝕜 Subtype.val

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

theorem Function.Injective.convexIndependent_iff_set {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [OrderedSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : ι → E} (hi : Function.Injective p) : ConvexIndependent 𝕜 Subtype.val ↔ ConvexIndependent 𝕜 p

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

@[simp]

theorem ConvexIndependent.mem_convexHull_iff {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [OrderedSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : ι → E} (hc : ConvexIndependent 𝕜 p) (s : Set ι) (i : ι) : p i ∈ (convexHull 𝕜) (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 convexIndependent_iff_not_mem_convexHull_diff {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [OrderedSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : ι → E} : ConvexIndependent 𝕜 p ↔ ∀ (i : ι) (s : Set ι), p i ∉ (convexHull 𝕜) (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 convexIndependent_set_iff_not_mem_convexHull_diff for the Set version.

theorem convexIndependent_set_iff_inter_convexHull_subset {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} : ConvexIndependent 𝕜 Subtype.val ↔ ∀ t ⊆ s, s ∩ (convexHull 𝕜) t ⊆ t

theorem convexIndependent_set_iff_not_mem_convexHull_diff {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} : ConvexIndependent 𝕜 Subtype.val ↔ ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})

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

theorem convexIndependent_iff_finset {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : ι → E} : ConvexIndependent 𝕜 p ↔ ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(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.convexIndependent_extremePoints {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) : ConvexIndependent 𝕜 Subtype.val