Convex combinations #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
A version of
s is a convex set,
w : ι → R is a family of
nonnegative weights with sum one and
z : ι → E is a family of elements of a module over
z i ∈ s whenever
w i ≠ 0``, then the sum∑ᶠ i, w i • z i
. See alsopartition_of_unity.finsum_smul_mem_convex`.
A refinement of
finset.center_mass_mem_convex_hull when the indexed family is a
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.
A weak version of Carathéodory's theorem.
std_simplex 𝕜 ι is the convex hull of the canonical basis in
ι → 𝕜.
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.
All values of a function
f ∈ std_simplex 𝕜 ι belong to
The convex hull of an affine basis is the intersection of the half-spaces defined by the corresponding barycentric coordinates.