eq_pos_convex_span_of_mem_convexHull
theorem eq_pos_convex_span_of_mem_convexHull :
β {π : Type u_1} {E : Type u} [inst : LinearOrderedField π] [inst_1 : AddCommGroup E] [inst_2 : Module π E]
{s : Set E} {x : E},
x β (convexHull π) s β
β ΞΉ x_1 z w,
Set.range z β s β§
AffineIndependent π z β§
(β (i : ΞΉ), 0 < w i) β§ (Finset.univ.sum fun i => w i) = 1 β§ (Finset.univ.sum fun i => w i β’ z i) = x
This theorem is a more explicit version of `convexHull_eq_union`. It states that for any given type `π` that is a linear ordered field, type `E` that is an additive commutative group and a module over `π`, a set `s` of type `E`, and an element `x` of type `E`, if `x` is in the convex hull of `s` with respect to `π`, then there exist elements `ΞΉ`, `x_1`, `z`, and `w` such that the range of `z` is a subset of `s`, `z` is affinely independent over `π`, every element of `w` is positive, the sum of all elements of `w` is 1, and the sum of all elements of `w` multiplied by the corresponding elements of `z` is equal to `x`. Essentially, it is saying that any point in the convex hull can be expressed as a positive weighted sum of affinely independent points from the set, where the weights sum up to 1.
More concisely: Given a linear ordered field `π`, an additive commutative group and `π`-module `E`, a set `s` in `E`, and an element `x` in the convex hull of `s` with respect to `π`, there exist `ΞΉ`, `x_1` in `s`, `z` in `s` affinely independent over `π`, and `w` in `π^(#s)` such that every component of `w` is positive, the sum of components of `w` is 1, and `x = β(w * z)`, where `*` denotes scalar multiplication.
|
Caratheodory.mem_minCardFinsetOfMemConvexHull
theorem Caratheodory.mem_minCardFinsetOfMemConvexHull :
β {π : Type u_1} {E : Type u} [inst : LinearOrderedField π] [inst_1 : AddCommGroup E] [inst_2 : Module π E]
{s : Set E} {x : E} (hx : x β (convexHull π) s),
x β (convexHull π) β(Caratheodory.minCardFinsetOfMemConvexHull hx)
The theorem `Caratheodory.mem_minCardFinsetOfMemConvexHull` states that for any linear ordered field `π`, any additive commutative group `E` and module `π E`, any set `s` of elements of type `E`, and any element `x` of type `E`, if `x` is an element of the convex hull of `s`, then `x` is also an element of the convex hull of the subset of `s` returned by the function `Caratheodory.minCardFinsetOfMemConvexHull`. This subset has the minimum cardinality among all subsets of `s` whose convex hull contains `x`. In other words, this theorem asserts that `x` is in the convex hull of the smallest possible subset of `s` that still includes `x` in its convex hull.
More concisely: For any linear ordered field π, additive commutative group E and its module over π, any set s of elements in E, and any x in E that belongs to the convex hull of s, x is also in the convex hull of the smallest subset of s with minimum cardinality guaranteeing x's inclusion.
|
Caratheodory.mem_convexHull_erase
theorem Caratheodory.mem_convexHull_erase :
β {π : Type u_1} {E : Type u} [inst : LinearOrderedField π] [inst_1 : AddCommGroup E] [inst_2 : Module π E]
[inst_3 : DecidableEq E] {t : Finset E},
Β¬AffineIndependent π Subtype.val β β {x : E}, x β (convexHull π) βt β β y, x β (convexHull π) β(t.erase βy)
The theorem `Caratheodory.mem_convexHull_erase` states that for any type `π`, which is a linearly ordered field, and any type `E`, which is an additive commutative group and a module over `π` with a decidable equality, if `x` is an element of `E` that lies in the convex hull of a finset `t` of `E`, and the elements of `t` are not affinely independent, then there exists an element `y` in `t` such that `x` is in the convex hull of the set obtained by erasing `y` from `t`. In simpler terms, if a point is in the smallest convex set containing a non-affinely independent set, then this point is also in the smallest convex set containing a strict subset of the original set.
More concisely: If `x` is an element of a convex set `C` in a linearly ordered field `π`, where `C` is generated by a finite, non-affinely independent set `t`, then `x` is also in the convex set generated by `t` without one of its elements.
|
convexHull_eq_union
theorem convexHull_eq_union :
β {π : Type u_1} {E : Type u} [inst : LinearOrderedField π] [inst_1 : AddCommGroup E] [inst_2 : Module π E]
{s : Set E}, (convexHull π) s = β t, β (_ : βt β s), β (_ : AffineIndependent π Subtype.val), (convexHull π) βt
**CarathΓ©odory's convexity theorem** in the given context can be described as follows:
For any set `s` of elements of type `E`, where `π` is a linear ordered field and `E` is a group with an additional operation that forms a module over `π`, the convex hull of `s` equals the union of convex hulls of all subsets `t` of `s` that are affinely independent. Here, the affine independence of a subset `t` means that no nontrivial weighted subtraction (where the sum of weights is zero) results in zero. The underlying element in the base type of a subset `t` is given by `Subtype.val`.
More concisely: The convex hull of a set in a linear ordered field with a group structure and module property is equal to the union of convex hulls of its affinely independent subsets.
|