LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.Convex.Independent

`ConvexIndependent.subtype` theorem ConvexIndependent.subtype : ∀ {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {p : ι → E}, ConvexIndependent 𝕜 p → ∀ (s : Set ι), ConvexIndependent 𝕜 fun i => p ↑i The theorem `ConvexIndependent.subtype` states that if a family of points is convex independent, then any subfamily indexed by a subtype of the index type is also convex independent. In mathematical terms, given an ordered semiring `𝕜`, an additive commutative group `E`, a module `E` over `𝕜`, and a function `p` from an index set `ι` to `E`, if `p` represents a convex independent family, then for any subset `s` of the index set `ι`, the family indexed by `s` via `p` is also convex independent. This is essentially a property of preservation of convex independence under the operation of taking subfamilies. More concisely: If a family of points is convex independent in an ordered semiring, then any subfamily indexed by a subtype of the index type is also convex independent.
`convexIndependent_set_iff_not_mem_convexHull_diff` theorem convexIndependent_set_iff_not_mem_convexHull_diff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {s : Set E}, ConvexIndependent 𝕜 Subtype.val ↔ ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x}) This theorem states that a set is convex independent if and only if, for any point in the set, that point does not belong to the convex hull of the rest of the set. In other words, the point cannot be represented as a convex combination of the other points in the set. Here, the term "convex hull" refers to the smallest convex set that contains all the points in the given set, and a "convex combination" of points is a weighted average of the points where all weights are non-negative and sum to one. This theorem has a more general version for indexed families of points. More concisely: A set is convex independent if and only if no point in the set belongs to the convex hull generated by the other points.
`ConvexIndependent.mono` theorem ConvexIndependent.mono : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {s t : Set E}, ConvexIndependent 𝕜 Subtype.val → s ⊆ t → ConvexIndependent 𝕜 Subtype.val The theorem `ConvexIndependent.mono` states that for any ordered semiring type `𝕜`, and any additive commutative group type `E` which also forms a module over `𝕜`, if we have two sets `s` and `t` of type `E`, then if the set `t` is convex independent, and `s` is a subset of `t`, then `s` is also convex independent. In other words, the property of being convex independent is preserved under the operation of taking subsets. In the context of convex geometry, this theorem asserts that any subset of a convex independent set of points is also convex independent. More concisely: If `E` is an additive commutative group that is a module over an ordered semiring `𝕜`, and `s` is a subset of the convex independent set `t` in `E`, then `s` is also convex independent.
`convexIndependent_iff_not_mem_convexHull_diff` theorem convexIndependent_iff_not_mem_convexHull_diff : ∀ {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {p : ι → E}, ConvexIndependent 𝕜 p ↔ ∀ (i : ι) (s : Set ι), p i ∉ (convexHull 𝕜) (p '' (s \ {i})) The theorem `convexIndependent_iff_not_mem_convexHull_diff` states that for any types `𝕜`, `E`, and `ι` with the appropriate structures (an ordered semiring, an additive commutative group, and a module over `𝕜`, respectively), a family `p` of elements of type `E` indexed by `ι` is convex independent if and only if for any index `i` and any set `s` of indices, the `i`-th element of the family does not belong to the convex hull of the images of the elements of `s`, excluding `i`. This means that no point in a convex independent family can be expressed as a convex combination of the other points in the family. More concisely: A family of elements in an additive commutative group is convex independent if and only if none of its elements belongs to the convex hull of the others when the index is excluded.
`Subsingleton.convexIndependent` theorem Subsingleton.convexIndependent : ∀ {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : Subsingleton ι] (p : ι → E), ConvexIndependent 𝕜 p This theorem states that a family with at most one point is convex independent. In other words, if we have a family that has no more than one point, then every point in that family belongs only to convex hulls of sets that contain it. The family is represented as a function from the index set `ι` to some vector space `E` over a semiring `𝕜`, and the statement of the theorem is applicable to all such families when `ι` is a subsingleton, i.e., a set with at most one element. More concisely: A family of size at most 1 in a vector space over a semiring is convex independent.
`ConvexIndependent.mem_convexHull_iff` theorem ConvexIndependent.mem_convexHull_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {p : ι → E}, ConvexIndependent 𝕜 p → ∀ (s : Set ι) (i : ι), p i ∈ (convexHull 𝕜) (p '' s) ↔ i ∈ s The theorem `ConvexIndependent.mem_convexHull_iff` states that for any indexed family `p` that is convex independent and for any set `s` of indices, a point `i` from the index set `ι` belongs to the convex hull of the points indexed by `s` if and only if `i` is an element of `s`. In other words, a point from a convex independent family is in the convex hull of particular points from the family, if and only if the point's index belongs to the set of indices that index those particular points. Convex independence here implies that each point contributes uniquely to the convex combination of the set, allowing this bi-conditional relationship between belonging to a convex hull and belonging to the indexing set. More concisely: A point indexed by i belongs to the convex hull of a convex independent family if and only if i is in the set of indices of the points in the family.
`Function.Injective.convexIndependent_iff_set` theorem Function.Injective.convexIndependent_iff_set : ∀ {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {p : ι → E}, Function.Injective p → (ConvexIndependent 𝕜 Subtype.val ↔ ConvexIndependent 𝕜 p) The theorem `Function.Injective.convexIndependent_iff_set` states that for any types `𝕜`, `E`, `ι` with `𝕜` being an ordered semiring, `E` being an additive commutative group, and `𝕜` and `E` forming a module, and any function `p` mapping from `ι` to `E`, if `p` is injective, then the range of this indexed family of points is convex independent if and only if the family itself is convex independent. In other words, a family of points is convex independent (meaning that each point is only contained in the convex hulls of sets containing it) if and only if the same property holds for the set of points obtained by applying the injective function `p` to each element of the family. More concisely: For any injective function from an indexed family of points in an ordered semiring-module over an additive commutative group to that group, the range of the function is convex independent if and only if the original family is.
`convexIndependent_iff_finset` theorem convexIndependent_iff_finset : ∀ {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {p : ι → E}, ConvexIndependent 𝕜 p ↔ ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(Finset.image p s) → x ∈ s This theorem states that to verify if an indexed family is convex independent over a linear ordered field and an additive commutative group that forms a module over the field, it is sufficient to check this property for finsets due to Carathéodory's theorem. In other words, an indexed family is convex independent if and only if for any finset and any element, the image of the element under the family mapping is in the convex hull of the image of the finset under the family mapping, then the element must be in the finset. More concisely: According to Carathéodory's theorem, an indexed family is convex independent over a linear ordered field and an additive commutative group if and only if for every finset and any element, the element is in the finset if and only if its image under the family mapping is in the convex hull of the image of the finset under the family mapping.
`ConvexIndependent.range` theorem ConvexIndependent.range : ∀ {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {p : ι → E}, ConvexIndependent 𝕜 p → ConvexIndependent 𝕜 Subtype.val The theorem `ConvexIndependent.range` states that for any ordered semiring `𝕜`, any additive commutative group `E`, any type `ι`, and any function `p` from `ι` to `E`, if the indexed family of points given by `p` is convex independent, then the corresponding set of points is also convex independent. Here, a family of points is said to be convex independent if each point belongs to the convex hull of only the sets that contain it. In this context, `Subtype.val` is used to extract the points in `E` from the subtype defined by the predicate of convex independence. More concisely: If a family of points in an additive commutative group with respect to an ordered semiring is convex independent, then the set of extracted points is also convex independent.
`ConvexIndependent.comp_embedding` theorem ConvexIndependent.comp_embedding : ∀ {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {ι' : Type u_4} (f : ι' ↪ ι) {p : ι → E}, ConvexIndependent 𝕜 p → ConvexIndependent 𝕜 (p ∘ ⇑f) This theorem states that if we have a family of points that is convex independent in some vector space over an ordered semiring, then any subfamily obtained by composing an embedding function into the index type with the original family is also convex independent. In other words, a family of points is convex independent if every point only belongs to the convex hulls of sets containing it, and this property is preserved when considering subfamilies that are formed by subsets of the original index set. More concisely: If a family of points in a vector space over an ordered semiring is convex independent, then any subfamily obtained by applying an embedding function into the index type also is convex independent.
`ConvexIndependent.injective` theorem ConvexIndependent.injective : ∀ {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {p : ι → E}, ConvexIndependent 𝕜 p → Function.Injective p This theorem states that a convex independent family is injective. In more detail, if we have a family of points, parameterized by `p : ι → E`, in a vector space `E` over a scalar field `𝕜`, and this family is convex independent, then the function `p` that maps each index `ι` to a point in `E` is injective. An injective function is one where different inputs always yield different outputs. In this case, different indices in `ι` will always map to different points in `E` if the family is convex independent. More concisely: If `p : ι → E` is a convex independent family of points in a vector space `E` over a scalar field `𝕜`, then `p` is an injective function.