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 1.
def
finset.center_mass
{R : Type u_1}
{E : Type u_2}
{ι : Type u_4}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
(t : finset ι)
(w : ι → R)
(z : ι → E) :
E
Center of mass of a finite collection of points with prescribed weights.
Note that we require neither 0 ≤ w i nor ∑ w = 1.
theorem
finset.center_mass_empty
{R : Type u_1}
{E : Type u_2}
{ι : Type u_4}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
(w : ι → R)
(z : ι → E) :
∅.center_mass w z = 0
theorem
finset.center_mass_pair
{R : Type u_1}
{E : Type u_2}
{ι : Type u_4}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
(i j : ι)
(w : ι → R)
(z : ι → E)
(hne : i ≠ j) :
theorem
finset.center_mass_insert
{R : Type u_1}
{E : Type u_2}
{ι : Type u_4}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
(i : ι)
(t : finset ι)
{w : ι → R}
(z : ι → E)
(ha : i ∉ t)
(hw : t.sum (λ (j : ι), w j) ≠ 0) :
(has_insert.insert i t).center_mass w z = (w i / (w i + t.sum (λ (j : ι), w j))) • z i + (t.sum (λ (j : ι), w j) / (w i + t.sum (λ (j : ι), w j))) • t.center_mass w z
theorem
finset.center_mass_singleton
{R : Type u_1}
{E : Type u_2}
{ι : Type u_4}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
(i : ι)
{w : ι → R}
(z : ι → E)
(hw : w i ≠ 0) :
{i}.center_mass w z = z i
theorem
finset.center_mass_eq_of_sum_1
{R : Type u_1}
{E : Type u_2}
{ι : Type u_4}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
(t : finset ι)
{w : ι → R}
(z : ι → E)
(hw : t.sum (λ (i : ι), w i) = 1) :
t.center_mass w z = t.sum (λ (i : ι), w i • z i)
theorem
finset.center_mass_smul
{R : Type u_1}
{E : Type u_2}
{ι : Type u_4}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
(c : R)
(t : finset ι)
{w : ι → R}
(z : ι → E) :
t.center_mass w (λ (i : ι), c • z i) = c • t.center_mass w z
theorem
finset.center_mass_segment'
{R : Type u_1}
{E : Type u_2}
{ι : Type u_4}
{ι' : Type u_5}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
(s : finset ι)
(t : finset ι')
(ws : ι → R)
(zs : ι → E)
(wt : ι' → R)
(zt : ι' → E)
(hws : s.sum (λ (i : ι), ws i) = 1)
(hwt : t.sum (λ (i : ι'), wt i) = 1)
(a b : R)
(hab : a + b = 1) :
a • s.center_mass ws zs + b • t.center_mass wt zt = (s.disj_sum t).center_mass (sum.elim (λ (i : ι), a * ws i) (λ (j : ι'), b * wt j)) (sum.elim zs zt)
A convex combination of two centers of mass is a center of mass as well. This version deals with two different index types.
theorem
finset.center_mass_segment
{R : Type u_1}
{E : Type u_2}
{ι : Type u_4}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
(s : finset ι)
(w₁ w₂ : ι → R)
(z : ι → E)
(hw₁ : s.sum (λ (i : ι), w₁ i) = 1)
(hw₂ : s.sum (λ (i : ι), w₂ i) = 1)
(a b : R)
(hab : a + b = 1) :
a • s.center_mass w₁ z + b • s.center_mass w₂ z = s.center_mass (λ (i : ι), a * w₁ i + b * w₂ i) z
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.
theorem
finset.center_mass_ite_eq
{R : Type u_1}
{E : Type u_2}
{ι : Type u_4}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
(i : ι)
(t : finset ι)
(z : ι → E)
(hi : i ∈ t) :
t.center_mass (λ (j : ι), ite (i = j) 1 0) z = z i
theorem
finset.center_mass_subset
{R : Type u_1}
{E : Type u_2}
{ι : Type u_4}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
{t : finset ι}
{w : ι → R}
(z : ι → E)
{t' : finset ι}
(ht : t ⊆ t')
(h : ∀ (i : ι), i ∈ t' → i ∉ t → w i = 0) :
t.center_mass w z = t'.center_mass w z
theorem
finset.center_mass_filter_ne_zero
{R : Type u_1}
{E : Type u_2}
{ι : Type u_4}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
{t : finset ι}
{w : ι → R}
(z : ι → E) :
(finset.filter (λ (i : ι), w i ≠ 0) t).center_mass w z = t.center_mass w z
theorem
finset.center_mass_le_sup
{R : Type u_1}
{ι : Type u_4}
{α : Type u_6}
[linear_ordered_field R]
[linear_ordered_add_comm_group α]
[module R α]
[ordered_smul R α]
{s : finset ι}
{f : ι → α}
{w : ι → R}
(hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i)
(hw₁ : 0 < s.sum (λ (i : ι), w i)) :
s.center_mass w f ≤ s.sup' _ f
theorem
finset.inf_le_center_mass
{R : Type u_1}
{ι : Type u_4}
{α : Type u_6}
[linear_ordered_field R]
[linear_ordered_add_comm_group α]
[module R α]
[ordered_smul R α]
{s : finset ι}
{f : ι → α}
{w : ι → R}
(hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i)
(hw₁ : 0 < s.sum (λ (i : ι), w i)) :
s.inf' _ f ≤ s.center_mass w f
theorem
convex.center_mass_mem
{R : Type u_1}
{E : Type u_2}
{ι : Type u_4}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
{s : set E}
{t : finset ι}
{w : ι → R}
{z : ι → E}
(hs : convex R s) :
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.
theorem
convex.finsum_mem
{R : Type u_1}
{E : Type u_2}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
{ι : Sort u_3}
{w : ι → R}
{z : ι → E}
{s : set E}
(hs : convex R s)
(h₀ : ∀ (i : ι), 0 ≤ w i)
(h₁ : finsum (λ (i : ι), w i) = 1)
(hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s) :
A version of convex.sum_mem for finsums. If 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 R such
that z i ∈ s whenever w i ≠ 0``, then the sum∑ᶠ i, w i • z ibelongs tos. See alsopartition_of_unity.finsum_smul_mem_convex`.
theorem
finset.center_mass_mem_convex_hull
{R : Type u_1}
{E : Type u_2}
{ι : Type u_4}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
{s : set E}
(t : finset ι)
{w : ι → R}
(hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i)
(hws : 0 < t.sum (λ (i : ι), w i))
{z : ι → E}
(hz : ∀ (i : ι), i ∈ t → z i ∈ s) :
t.center_mass w z ∈ ⇑(convex_hull R) s
theorem
finset.center_mass_id_mem_convex_hull
{R : Type u_1}
{E : Type u_2}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
(t : finset E)
{w : E → R}
(hw₀ : ∀ (i : E), i ∈ t → 0 ≤ w i)
(hws : 0 < t.sum (λ (i : E), w i)) :
t.center_mass w id ∈ ⇑(convex_hull R) ↑t
A refinement of finset.center_mass_mem_convex_hull when the indexed family is a finset of
the space.
theorem
affine_combination_eq_center_mass
{R : Type u_1}
{E : Type u_2}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
{ι : Type u_3}
{t : finset ι}
{p : ι → E}
{w : ι → R}
(hw₂ : t.sum (λ (i : ι), w i) = 1) :
⇑(finset.affine_combination R t p) w = t.center_mass w p
theorem
affine_combination_mem_convex_hull
{R : Type u_1}
{E : Type u_2}
{ι : Type u_4}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
{s : finset ι}
{v : ι → E}
{w : ι → R}
(hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i)
(hw₁ : s.sum w = 1) :
⇑(finset.affine_combination R s v) w ∈ ⇑(convex_hull R) (set.range v)
@[simp]
theorem
finset.centroid_eq_center_mass
{R : Type u_1}
{E : Type u_2}
{ι : Type u_4}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
(s : finset ι)
(hs : s.nonempty)
(p : ι → E) :
finset.centroid R s p = s.center_mass (finset.centroid_weights R s) p
The centroid can be regarded as a center of mass.
theorem
finset.centroid_mem_convex_hull
{R : Type u_1}
{E : Type u_2}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
(s : finset E)
(hs : s.nonempty) :
finset.centroid R s id ∈ ⇑(convex_hull R) ↑s
theorem
convex_hull_range_eq_exists_affine_combination
{R : Type u_1}
{E : Type u_2}
{ι : Type u_4}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
(v : ι → E) :
theorem
convex_hull_eq
{R : Type u_1}
{E : Type u_2}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
(s : set E) :
Convex hull of s is equal to the set of all centers of masses of finsets t, z '' t ⊆ s.
This version allows finsets in any type in any universe.
theorem
finset.convex_hull_eq
{R : Type u_1}
{E : Type u_2}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
(s : finset E) :
theorem
finset.mem_convex_hull
{R : Type u_1}
{E : Type u_2}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
{s : finset E}
{x : E} :
theorem
set.finite.convex_hull_eq
{R : Type u_1}
{E : Type u_2}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
{s : set E}
(hs : s.finite) :
theorem
convex_hull_eq_union_convex_hull_finite_subsets
{R : Type u_1}
{E : Type u_2}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
(s : set E) :
A weak version of Carathéodory's theorem.
theorem
mk_mem_convex_hull_prod
{R : Type u_1}
{E : Type u_2}
{F : Type u_3}
[linear_ordered_field R]
[add_comm_group E]
[add_comm_group F]
[module R E]
[module R F]
{s : set E}
{t : set F}
{x : E}
{y : F}
(hx : x ∈ ⇑(convex_hull R) s)
(hy : y ∈ ⇑(convex_hull R) t) :
(x, y) ∈ ⇑(convex_hull R) (s ×ˢ t)
@[simp]
theorem
convex_hull_prod
{R : Type u_1}
{E : Type u_2}
{F : Type u_3}
[linear_ordered_field R]
[add_comm_group E]
[add_comm_group F]
[module R E]
[module R F]
(s : set E)
(t : set F) :
⇑(convex_hull R) (s ×ˢ t) = ⇑(convex_hull R) s ×ˢ ⇑(convex_hull R) t
theorem
convex_hull_add
{R : Type u_1}
{E : Type u_2}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
(s t : set E) :
⇑(convex_hull R) (s + t) = ⇑(convex_hull R) s + ⇑(convex_hull R) t
def
convex_hull_add_monoid_hom
(R : Type u_1)
(E : Type u_2)
[linear_ordered_field R]
[add_comm_group E]
[module R E] :
convex_hull is an additive monoid morphism under pointwise addition.
Equations
- convex_hull_add_monoid_hom R E = {to_fun := ⇑(convex_hull R), map_zero' := _, map_add' := _}
@[simp]
theorem
convex_hull_add_monoid_hom_apply
(R : Type u_1)
(E : Type u_2)
[linear_ordered_field R]
[add_comm_group E]
[module R E]
(ᾰ : set E) :
⇑(convex_hull_add_monoid_hom R E) ᾰ = ⇑(convex_hull R) ᾰ
theorem
convex_hull_sub
{R : Type u_1}
{E : Type u_2}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
(s t : set E) :
⇑(convex_hull R) (s - t) = ⇑(convex_hull R) s - ⇑(convex_hull R) t
theorem
convex_hull_list_sum
{R : Type u_1}
{E : Type u_2}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
(l : list (set E)) :
⇑(convex_hull R) l.sum = (list.map ⇑(convex_hull R) l).sum
theorem
convex_hull_multiset_sum
{R : Type u_1}
{E : Type u_2}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
(s : multiset (set E)) :
⇑(convex_hull R) s.sum = (multiset.map ⇑(convex_hull R) s).sum
theorem
convex_hull_sum
{R : Type u_1}
{E : Type u_2}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
{ι : Type u_3}
(s : finset ι)
(t : ι → set E) :
⇑(convex_hull R) (s.sum (λ (i : ι), t i)) = s.sum (λ (i : ι), ⇑(convex_hull R) (t i))
theorem
convex_hull_basis_eq_std_simplex
{R : Type u_1}
(ι : Type u_4)
[linear_ordered_field R]
[fintype ι] :
⇑(convex_hull R) (set.range (λ (i j : ι), ite (i = j) 1 0)) = std_simplex R ι
std_simplex 𝕜 ι is the convex hull of the canonical basis in ι → 𝕜.
theorem
set.finite.convex_hull_eq_image
{R : Type u_1}
{E : Type u_2}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
{s : set E}
(hs : s.finite) :
⇑(convex_hull R) s = ⇑(finset.univ.sum (λ (x : ↥s), (linear_map.proj x).smul_right x.val)) '' std_simplex R ↥s
The convex hull of a finite set is the image of the standard simplex in s → ℝ
under the linear map sending each function w to ∑ 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.
theorem
mem_Icc_of_mem_std_simplex
{R : Type u_1}
{ι : Type u_4}
[linear_ordered_field R]
[fintype ι]
{f : ι → R}
(hf : f ∈ std_simplex R ι)
(x : ι) :
All values of a function f ∈ std_simplex 𝕜 ι belong to [0, 1].
theorem
affine_basis.convex_hull_eq_nonneg_coord
{R : Type u_1}
{E : Type u_2}
[linear_ordered_field R]
[add_comm_group E]
[module R E]
{ι : Type u_3}
(b : affine_basis ι R E) :
The convex hull of an affine basis is the intersection of the half-spaces defined by the corresponding barycentric coordinates.