Finset.centerMass_id_mem_convexHull
theorem Finset.centerMass_id_mem_convexHull :
∀ {R : Type u_1} {E : Type u_3} [inst : LinearOrderedField R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
(t : Finset E) {w : E → R},
(∀ i ∈ t, 0 ≤ w i) → (0 < t.sum fun i => w i) → t.centerMass w id ∈ (convexHull R) ↑t
This theorem, `Finset.centerMass_id_mem_convexHull`, states that for any finset `t` of a certain type `E` in a space with a linear ordered field `R` and an additive commutative group structure, and any weight function `w` from `E` to `R`, if each weight is non-negative and the total sum of weights is positive, then the center of mass of `t` with respect to `w` lies in the convex hull of `t`. Here, the center of mass is calculated straightforwardly as the weighted average of the elements in `t`, using the identity function `id` to choose the elements. The convex hull of a set `s` is defined as the smallest convex set that contains `s`.
More concisely: For any finset `t` in a linear ordered field `R` with additive commutative group structure, and non-negative weight function `w` from `t` to `R` with positive total sum, the center of mass of `t` with respect to `w` lies in the convex hull of `t`.
|
Finset.centroid_eq_centerMass
theorem Finset.centroid_eq_centerMass :
∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : LinearOrderedField R] [inst_1 : AddCommGroup E]
[inst_2 : Module R E] (s : Finset ι),
s.Nonempty → ∀ (p : ι → E), Finset.centroid R s p = s.centerMass (Finset.centroidWeights R s) p
This theorem states that for any set of points, the centroid of these points can be regarded as their center of mass. More specifically, given a linearly ordered field `R`, a commutative additive group `E`, and a finset `s` indexed by `ι`, if `s` is nonempty and `p` is a function mapping each index to a point in `E`, then the centroid of the points given by `p` with respect to `s` is equivalent to the center of mass of these points weighted by the centroid weights of `s`. The centroid weights are defined as the reciprocal of the number of points in the set.
More concisely: Given a linearly ordered field `R`, a commutative additive group `E`, and a nonempty finset `s` with points `p : ι → E`, the centroid of `s` with respect to `p` equals the center of mass of `s` weighted by the centroid weights `1 / |s|`.
|
Finset.centerMass_id_mem_convexHull_of_nonpos
theorem Finset.centerMass_id_mem_convexHull_of_nonpos :
∀ {R : Type u_1} {E : Type u_3} [inst : LinearOrderedField R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
(t : Finset E) {w : E → R},
(∀ i ∈ t, w i ≤ 0) → (t.sum fun i => w i) < 0 → t.centerMass w id ∈ (convexHull R) ↑t
The theorem `Finset.centerMass_id_mem_convexHull_of_nonpos` states that for any finite set `t` of elements of an `AddCommGroup` `E` over a `LinearOrderedField` `R`, given a weight function `w : E → R` such that all weights are nonpositive (i.e., `w i ≤ 0` for all `i ∈ t`), if the sum of all weights is negative, then the center of mass of the set `t`, computed with these weights, belongs to the convex hull of the set `t`. The convex hull is the minimal convex set that includes `t`.
In mathematical terms, if $t$ is a finite set in a vector space and $w$ is a weight function with nonpositive values such that the sum of all weights is negative, then the center of mass of the set, computed with these weights, belongs to the convex hull of the set.
More concisely: If $t$ is a finite set in a vector space over a Linear Ordered Field, and $w : t \rightarrow \mathbb{R}$ is a weight function with all weights nonpositive and the sum negative, then the center of mass of $t$ with respect to $w$ lies in the convex hull of $t$.
|
Finset.centerMass_mem_convexHull_of_nonpos
theorem Finset.centerMass_mem_convexHull_of_nonpos :
∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : LinearOrderedField R] [inst_1 : AddCommGroup E]
[inst_2 : Module R E] {s : Set E} {w : ι → R} {z : ι → E} (t : Finset ι),
(∀ i ∈ t, w i ≤ 0) → (t.sum fun i => w i) < 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ (convexHull R) s
The theorem `Finset.centerMass_mem_convexHull_of_nonpos` states that, for any set `s` of type `E` in a module over a linear ordered field `R`, and any finite set `t` with weights `w` and elements `z` of type `ι`, if all the weights are nonpositive (i.e., less than or equal to zero), the sum of the weights is negative, and all the elements of `t` are in `s`, then the center of mass of `t` (calculated with weights `w` and elements `z`) is in the convex hull of `s`. Here, the convex hull of `s` is the minimal convex set that contains `s`. In the context of this theorem, a convex set is a set where, for any two points within the set, every point on the straight line segment that joins them is also within the set.
More concisely: If `s` is a set in an R-module, `t` is a finite subset of `s` with nonpositive weights summing to a negative value, then the center of mass of `t` lies in the convex hull of `s`.
|
Finset.centerMass_mem_convexHull
theorem Finset.centerMass_mem_convexHull :
∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : LinearOrderedField R] [inst_1 : AddCommGroup E]
[inst_2 : Module R E] {s : Set E} (t : Finset ι) {w : ι → R},
(∀ i ∈ t, 0 ≤ w i) →
(0 < t.sum fun i => w i) → ∀ {z : ι → E}, (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ (convexHull R) s
The theorem `Finset.centerMass_mem_convexHull` states that for any type `R` that is a linear ordered field, a type `E` that is an add commutative group and a module over `R`, a type `ι`, a set `s` of type `E`, a finite set `t` of type `ι`, a weight function `w` from `ι` to `R`, and a point function `z` from `ι` to `E`, if all weights are nonnegative and the sum of the weights is positive, and each point `z i` for `i` in `t` is in the set `s`, then the center of mass of the points given by `z` with weights given by `w` is in the convex hull of the set `s`. The center of mass is computed as the scaled sum of the weighted points, where the scaling factor is the inverse of the sum of the weights. The convex hull of a set is the minimal convex set that includes the given set.
More concisely: Given a linear ordered field R, an add commutative group and R-module E, a set s of points in E, a finite index set ι, a weight function w : ι -> R with nonnegative and positive sum, and a point function z : ι -> s, if every z(i) is in s, then the center of mass of z with weights w is in the convex hull of s.
|
Finset.centerMass_segment
theorem Finset.centerMass_segment :
∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : LinearOrderedField R] [inst_1 : AddCommGroup E]
[inst_2 : Module R E] (s : Finset ι) (w₁ w₂ : ι → R) (z : ι → E),
(s.sum fun i => w₁ i) = 1 →
(s.sum fun i => w₂ i) = 1 →
∀ (a b : R),
a + b = 1 → a • s.centerMass w₁ z + b • s.centerMass w₂ z = s.centerMass (fun i => a * w₁ i + b * w₂ i) z
This theorem states that a convex combination of two centers of mass is also a center of mass. Specifically, in a setting where we have a linear ordered field `R`, an additive commutative group `E`, and a module structure on `E` over `R`, given a finite set `s` indexed by `ι`, and two weight functions `w₁` and `w₂` from `ι` to `R`, if the sum of the weights under both functions is 1, then for any two real numbers `a` and `b` that sum to 1, the center of mass calculated with weights `a * w₁ i + b * w₂ i` is the same as the convex combination of the centers of mass calculated independently with weights `w₁` and `w₂`. This particular version of the theorem applies when the two centers of mass are calculated from the same original set of points.
More concisely: Given a finite set with mass function, if two weight functions sum to 1 and their respective center of masses are `m₁` and `m₂`, then the center of mass of the convex combination `a * m₁ + b * m₂` is equal to the center of mass calculated using weights `a * w + b * w₂` with respect to the original set.
|
convexHull_eq_union_convexHull_finite_subsets
theorem convexHull_eq_union_convexHull_finite_subsets :
∀ {R : Type u_1} {E : Type u_3} [inst : LinearOrderedField R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
(s : Set E), (convexHull R) s = ⋃ t, ⋃ (_ : ↑t ⊆ s), (convexHull R) ↑t
This is a weaker version of the Carathéodory's theorem. The theorem states that for any set `s` of type `E` in a linear ordered field `R` that is also a module over `R`, the convex hull of `s` is equal to the union of the convex hulls of all of its finite subsets `t` where `t` is a subset of `s`. In other words, the smallest convex set that contains `s` can be expressed as the union of the smallest convex sets containing its finite subsets.
More concisely: The convex hull of a linear ordered field module `s` equals the union of the convex hulls of its finite subsets.
|
convexHull_basis_eq_stdSimplex
theorem convexHull_basis_eq_stdSimplex :
∀ {R : Type u_1} (ι : Type u_5) [inst : LinearOrderedField R] [inst_1 : Fintype ι],
(convexHull R) (Set.range fun i j => if i = j then 1 else 0) = stdSimplex R ι
The theorem `convexHull_basis_eq_stdSimplex` states that for any linear ordered field `R` and any type `ι` with a finite number of elements (`Fintype ι`), the standard simplex in the space of functions from `ι` to `R` is equal to the convex hull of the canonical basis in the function space `ι → R`. Here the canonical basis is defined as the set of functions which output `1` if the input is equal to a specific element of `ι` and `0` otherwise. In other words, the standard simplex, which is the set of vectors with non-negative coordinates that sum to `1`, is the smallest convex set containing all basis vectors.
More concisely: The standard simplex in the space of functions from a finite type `ι` to a linear ordered field `R` equals the convex hull of the canonical basis in this function space.
|
AffineBasis.convexHull_eq_nonneg_coord
theorem AffineBasis.convexHull_eq_nonneg_coord :
∀ {R : Type u_1} {E : Type u_3} [inst : LinearOrderedField R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
{ι : Type u_8} (b : AffineBasis ι R E), (convexHull R) (Set.range ⇑b) = {x | ∀ (i : ι), 0 ≤ (b.coord i) x}
The theorem `AffineBasis.convexHull_eq_nonneg_coord` states that for any Affine basis `b` of a module `E` over an ordered field `R`, the convex hull of the set of all points in `E` that can be reached by `b` is exactly the set of points `x` in `E` for which all the barycentric coordinates `(b.coord i) x` corresponding to `b` are non-negative. In other words, the convex hull of an affine basis is the intersection of all half-spaces defined by non-negative barycentric coordinates.
More concisely: The convex hull of an affine basis of a module over an ordered field is the set of points with non-negative barycentric coordinates with respect to that basis.
|
Convex.finsum_mem
theorem Convex.finsum_mem :
∀ {R : Type u_1} {E : Type u_3} [inst : LinearOrderedField R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
{ι : Sort u_8} {w : ι → R} {z : ι → E} {s : Set E},
Convex R s →
(∀ (i : ι), 0 ≤ w i) →
(finsum fun i => w i) = 1 → (∀ (i : ι), w i ≠ 0 → z i ∈ s) → (finsum fun i => w i • z i) ∈ s
This theorem, `Convex.finsum_mem`, states that, given a convex set `s` of elements from a module over a linear ordered field `R`, a family `w : ι → R` of nonnegative weights that sum up to one, and `z : ι → E`, a family of elements from the module such that each `z i` is in the set `s` whenever `w i` is non-zero, then the finite sum of the elements `w i • z i`, otherwise known as the weighted sum, also belongs to the set `s`. This theorem is a version of `Convex.sum_mem` tailored for finite sums (`finsum`).
More concisely: Given a convex set `s` in a module over a linear ordered field, a family `w : ι → R` of nonnegative weights summing up to one, and a family `z : ι → E` of elements in `s` indexed by `ι` such that `w i = 0` implies `z i = 0`, the weighted finite sum `∑ i ∈ ι w i * z i` belongs to `s`.
|
AffineIndependent.convexHull_inter
theorem AffineIndependent.convexHull_inter :
∀ {R : Type u_1} {E : Type u_3} [inst : LinearOrderedField R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
{s t₁ t₂ : Finset E},
AffineIndependent R Subtype.val →
t₁ ⊆ s → t₂ ⊆ s → (convexHull R) (↑t₁ ∩ ↑t₂) = (convexHull R) ↑t₁ ∩ (convexHull R) ↑t₂
This theorem states that if we have a set of points in a vector space that constitute an affinely independent set (i.e., no nontrivial weighted subtraction of these points, where the sum of the weights equals zero, results in the zero vector), and two subsets of these points, then the intersection of the convex hulls of the two subsets is equal to the convex hull of the intersection of the two subsets. Simply put, if the union of the vertices of two geometric shapes (simplices) is affinely independent, the intersection of the convex hulls of the shapes behaves well and is the same as the convex hull of their intersection.
More concisely: If two subsets of an affinely independent set in a vector space have the property that their convex hulls intersect only at the origin, then the convex hull of their intersection equals the intersection of their convex hulls.
|
Finset.centerMass_segment'
theorem Finset.centerMass_segment' :
∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} {ι' : Type u_6} [inst : LinearOrderedField R]
[inst_1 : AddCommGroup E] [inst_2 : Module R E] (s : Finset ι) (t : Finset ι') (ws : ι → R) (zs : ι → E)
(wt : ι' → R) (zt : ι' → E),
(s.sum fun i => ws i) = 1 →
(t.sum fun i => wt i) = 1 →
∀ (a b : R),
a + b = 1 →
a • s.centerMass ws zs + b • t.centerMass wt zt =
(s.disjSum t).centerMass (Sum.elim (fun i => a * ws i) fun j => b * wt j) (Sum.elim zs zt)
The theorem `Finset.centerMass_segment'` states that given two sets of indices `s` and `t` of types `ι` and `ι'` respectively, two corresponding weight functions `ws` and `wt`, and two corresponding point functions `zs` and `zt` in an additively commutative group `E` over a linearly ordered field `R`, if the sum of weights in each set equals 1, then for any two numbers `a` and `b` in `R` such that `a + b = 1`, the weighted sum of the center of mass of set `s` and the center of mass of set `t` (with weights `a` and `b` respectively) is equal to the center of mass of the disjoint sum of the two sets, where the weights and points are extended by multiplying `a` and `b` with the weights from `s` and `t` respectively. In simpler terms, the theorem establishes a property about the center of mass in a convex combination scenario with two different types of indices.
More concisely: Given sets of indices `s` and `t` with equal weighted sums 1 in an additively commutative group `E` over a linearly ordered field `R`, the center of mass of the weighted disjoint sum of `s` and `t` is equal to the weighted sum of the centers of mass of `s` and `t` with coefficients from `R` summing to 1.
|
convexHull_eq
theorem convexHull_eq :
∀ {R : Type u_1} {E : Type u_3} [inst : LinearOrderedField R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
(s : Set E),
(convexHull R) s =
{x | ∃ ι t w z, (∀ i ∈ t, 0 ≤ w i) ∧ (t.sum fun i => w i) = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x}
The theorem `convexHull_eq` states that for any set `s` of elements of Type `E` in a module over a linear ordered field `R`, the convex hull of `s` is equal to the set of all possible centers of mass of finsets `t`, where each point in the image of `t` under a function `z` is an element of `s`. Additionally, every element `i` in `t` has a corresponding weight `w i` which is nonnegative, the sum of all these weights is 1, and the center of mass of `t` with respect to weights `w` and function `z` is `x`. The theorem advises not to use it to prove a given center of mass belongs to the convex hull due to universe reasons, and recommends using the convexity of the convex hull instead.
More concisely: The convex hull of a set of elements in a module over a linear ordered field is equal to the set of centers of mass of weighted finsets whose images under a given function are elements of the set, where the weights are nonnegative and their sum is 1.
|
Finset.centerMass_eq_of_sum_1
theorem Finset.centerMass_eq_of_sum_1 :
∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : LinearOrderedField R] [inst_1 : AddCommGroup E]
[inst_2 : Module R E] (t : Finset ι) {w : ι → R} (z : ι → E),
(t.sum fun i => w i) = 1 → t.centerMass w z = t.sum fun i => w i • z i
This theorem states that for any linear ordered field `R`, additively commutative group `E`, and arbitrary type `ι`, if we have a finite set `t` of type `ι`, a weight function `w: ι → R`, and a point function `z: ι → E` such that the sum of the weights equals 1, then the center of mass of the finite collection of points (derived from `z`) with the prescribed weights (derived from `w`) is equal to the weighted sum of the points. In other words, it says that if the weights sum up to 1, then the center of mass is just the weighted sum of the points in the set.
More concisely: Given a linear ordered field `R`, an additively commutative group `E`, a finite set `t` of type `ι`, a weight function `w: ι → R`, and a point function `z: ι → E` with sum of weights equal to 1, the center of mass of `z` with respect to `w` equals the weighted sum of `z`.
|
Set.Finite.convexHull_eq_image
theorem Set.Finite.convexHull_eq_image :
∀ {R : Type u_1} {E : Type u_3} [inst : LinearOrderedField R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
{s : Set E} (hs : s.Finite),
(convexHull R) s = ⇑(Finset.univ.sum fun x => (LinearMap.proj x).smulRight ↑x) '' stdSimplex R ↑s
The theorem `Set.Finite.convexHull_eq_image` states that for any finite set `s` of elements from a module `E` over a linearly ordered field `R`, the convex hull of `s` is the image of the standard simplex in `s → R` under the linear map that sends each function `w` to the weighted sum of elements in `s` where the weights are given by `w`. It's important to note that the sum is taken over the universe finite set of `s` due to the lack of sums over finite sets in Lean. The map is defined in terms of operations on `(s → R) →ₗ[R] R` to alleviate the need to prove that this map is linear later on.
More concisely: The convex hull of a finite set `s` in a module `E` over a linearly ordered field `R` is equal to the image of the standard simplex under the linear map that sends a function `w` to the weighted sum of elements in `s` using weights `w(x)` for each `x` in `s`.
|
Convex.centerMass_mem
theorem Convex.centerMass_mem :
∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : LinearOrderedField R] [inst_1 : AddCommGroup E]
[inst_2 : Module R E] {s : Set E} {t : Finset ι} {w : ι → R} {z : ι → E},
Convex R s → (∀ i ∈ t, 0 ≤ w i) → (0 < t.sum fun i => w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
The theorem `Convex.centerMass_mem` states that for any linearly ordered field `R`, a commutative group `E` under addition, and a type `ι`, given a convex set `s` of type `E`, a finite set `t` of type `ι`, a function `w` mapping values of type `ι` to `R`, and a function `z` mapping values of type `ι` to `E`, if the set `s` is convex, all weights defined by function `w` for elements in the set `t` are non-negative, the sum of all these weights is positive, and all elements mapped from the set `t` by function `z` belong to the set `s`, then the center of mass of the finite set `t` with the weights defined by `w` and positions defined by `z` belongs to the convex set `s`. In other words, the weighted average of points in a convex set, under certain conditions, is still in the convex set.
More concisely: Given a convex set in a commutative group under addition, a finite set of points with non-negative weights summing to a positive value, and the points mapped to the set by a function, the center of mass of the weighted points lies within the convex set.
|
Finset.mem_convexHull'
theorem Finset.mem_convexHull' :
∀ {R : Type u_1} {E : Type u_3} [inst : LinearOrderedField R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
{s : Finset E} {x : E},
x ∈ (convexHull R) ↑s ↔ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ (s.sum fun y => w y) = 1 ∧ (s.sum fun y => w y • y) = x
This theorem, `Finset.mem_convexHull'`, asserts that for any linear ordered field `R`, any additive commutative group `E`, and any module over `R` and `E`, for any finite set `s` of type `E` and any element `x` of type `E`, `x` is in the convex hull of `s` if and only if there exists a function `w` such that for all `y` in `s`, `w(y)` is non-negative, the sum of `w(y)` for all `y` in `s` is 1, and the sum of `w(y) * y` for all `y` in `s` is `x`. In simpler terms, an element is in the convex hull of a finite set if and only if it can be expressed as a convex combination of the elements in the set.
More concisely: An element is in the convex hull of a finite set if and only if it can be expressed as a convex combination of the elements in the set.
|
AffineIndependent.convexHull_inter'
theorem AffineIndependent.convexHull_inter' :
∀ {R : Type u_1} {E : Type u_3} [inst : LinearOrderedField R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
{t₁ t₂ : Finset E},
AffineIndependent R Subtype.val → (convexHull R) (↑t₁ ∩ ↑t₂) = (convexHull R) ↑t₁ ∩ (convexHull R) ↑t₂
The theorem `AffineIndependent.convexHull_inter'` states that, for any two finite sets of points `t1` and `t2` in a vector space over an ordered field, if the union of these two sets is affinely independent, then the convex hull of the intersection of `t1` and `t2` is equal to the intersection of the convex hulls of `t1` and `t2`. This theorem essentially ensures that the process of taking convex hulls is compatible with intersection under the condition of affine independence. The theorem also notes that `AffineIndependent.convexHull_inter` is generally more versatile for most use cases.
More concisely: If two finite sets of points in a vector space over an ordered field are affinely independent, then the convex hull of their intersection is equal to the intersection of their convex hulls.
|
mem_Icc_of_mem_stdSimplex
theorem mem_Icc_of_mem_stdSimplex :
∀ {R : Type u_1} {ι : Type u_5} [inst : LinearOrderedField R] [inst_1 : Fintype ι] {f : ι → R},
f ∈ stdSimplex R ι → ∀ (x : ι), f x ∈ Set.Icc 0 1
The theorem `mem_Icc_of_mem_stdSimplex` states that for any linear ordered field `R` and finite set `ι`, if a function `f` from `ι` to `R` is in the standard simplex (meaning that its values are non-negative and sum to 1), then all values of the function `f` belong to the closed interval from 0 to 1. In other words, every element `x` in `ι` maps to a value between 0 and 1 (inclusive) under the function `f`.
More concisely: For any linear ordered field R and finite set ι, if f : ι → R is a function with non-negative values and whose components sum to 1, then for all x ∈ ι, f(x) ∈ [0, 1].
|