Convex combinations #
This file defines convex combinations of points in a vector space.
Main declarations #
finset.center_mass: Center of mass of a finite family of points.
Implementation notes #
We divide by the sum of the weights in the definition of
finset.center_mass because of the way
mathematical arguments go: one doesn't change weights, but merely adds some. This also makes a few
lemmas unconditional on the sum of the weights being
Center of mass of a finite collection of points with prescribed weights.
Note that we require neither
0 ≤ w i nor
∑ w = 1.
A convex combination of two centers of mass is a center of mass as well. This version deals with two different index types.
A convex combination of two centers of mass is a center of mass as well. This version works if two centers of mass share the set of original points.
The center of mass of a finite subset of a convex set belongs to the set provided that all weights are non-negative, and the total weight is positive.
The centroid can be regarded as a center of mass.
Convex hull of
s is equal to the set of all centers of masses of
z '' t ⊆ s.
This version allows finsets in any type in any universe.
The convex hull of a finite set is the image of the standard simplex in
s → ℝ
under the linear map sending each function
∑ x in s, w x • x.
Since we have no sums over finite sets, we use sum over
@finset.univ _ hs.fintype.
The map is defined in terms of operations on
(s → ℝ) →ₗ[ℝ] ℝ so that later we will not need
to prove that this map is linear.
The convex hull of an affine basis is the intersection of the half-spaces defined by the corresponding barycentric coordinates.