Convex combinations #
This file defines convex combinations of points in a vector space.
Main declarations #
Finset.centerMass: Center of mass of a finite family of points.
Implementation notes #
We divide by the sum of the weights in the definition of Finset.centerMass 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.centerMass
{R : Type u_1}
{E : Type u_3}
{ι : Type u_5}
[LinearOrderedField R]
[AddCommGroup 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.
Equations
- Finset.centerMass t w z = (Finset.sum t fun i => w i)⁻¹ • Finset.sum t fun i => w i • z i
Instances For
theorem
Finset.centerMass_empty
{R : Type u_1}
{E : Type u_3}
{ι : Type u_5}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
(w : ι → R)
(z : ι → E)
:
Finset.centerMass ∅ w z = 0
theorem
Finset.centerMass_pair
{R : Type u_1}
{E : Type u_3}
{ι : Type u_5}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
(i : ι)
(j : ι)
(w : ι → R)
(z : ι → E)
(hne : i ≠ j)
:
theorem
Finset.centerMass_insert
{R : Type u_1}
{E : Type u_3}
{ι : Type u_5}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
(i : ι)
(t : Finset ι)
{w : ι → R}
(z : ι → E)
(ha : ¬i ∈ t)
(hw : (Finset.sum t fun j => w j) ≠ 0)
:
Finset.centerMass (insert i t) w z = (w i / (w i + Finset.sum t fun j => w j)) • z i + ((Finset.sum t fun j => w j) / (w i + Finset.sum t fun j => w j)) • Finset.centerMass t w z
theorem
Finset.centerMass_singleton
{R : Type u_1}
{E : Type u_3}
{ι : Type u_5}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
(i : ι)
{w : ι → R}
(z : ι → E)
(hw : w i ≠ 0)
:
Finset.centerMass {i} w z = z i
@[simp]
theorem
Finset.centerMass_neg_left
{R : Type u_1}
{E : Type u_3}
{ι : Type u_5}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
(t : Finset ι)
{w : ι → R}
(z : ι → E)
:
Finset.centerMass t (-w) z = Finset.centerMass t w z
theorem
Finset.centerMass_smul_left
{R : Type u_1}
{R' : Type u_2}
{E : Type u_3}
{ι : Type u_5}
[LinearOrderedField R]
[LinearOrderedField R']
[AddCommGroup E]
[Module R E]
(t : Finset ι)
{w : ι → R}
(z : ι → E)
{c : R'}
[Module R' R]
[Module R' E]
[SMulCommClass R' R R]
[IsScalarTower R' R R]
[SMulCommClass R R' E]
[IsScalarTower R' R E]
(hc : c ≠ 0)
:
Finset.centerMass t (c • w) z = Finset.centerMass t w z
theorem
Finset.centerMass_eq_of_sum_1
{R : Type u_1}
{E : Type u_3}
{ι : Type u_5}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
(t : Finset ι)
{w : ι → R}
(z : ι → E)
(hw : (Finset.sum t fun i => w i) = 1)
:
Finset.centerMass t w z = Finset.sum t fun i => w i • z i
theorem
Finset.centerMass_smul
{R : Type u_1}
{E : Type u_3}
{ι : Type u_5}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
(c : R)
(t : Finset ι)
{w : ι → R}
(z : ι → E)
:
(Finset.centerMass t w fun i => c • z i) = c • Finset.centerMass t w z
theorem
Finset.centerMass_segment'
{R : Type u_1}
{E : Type u_3}
{ι : Type u_5}
{ι' : Type u_6}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
(s : Finset ι)
(t : Finset ι')
(ws : ι → R)
(zs : ι → E)
(wt : ι' → R)
(zt : ι' → E)
(hws : (Finset.sum s fun i => ws i) = 1)
(hwt : (Finset.sum t fun i => wt i) = 1)
(a : R)
(b : R)
(hab : a + b = 1)
:
a • Finset.centerMass s ws zs + b • Finset.centerMass t wt zt = Finset.centerMass (Finset.disjSum s t) (Sum.elim (fun i => a * ws i) fun 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.centerMass_segment
{R : Type u_1}
{E : Type u_3}
{ι : Type u_5}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
(s : Finset ι)
(w₁ : ι → R)
(w₂ : ι → R)
(z : ι → E)
(hw₁ : (Finset.sum s fun i => w₁ i) = 1)
(hw₂ : (Finset.sum s fun i => w₂ i) = 1)
(a : R)
(b : R)
(hab : a + b = 1)
:
a • Finset.centerMass s w₁ z + b • Finset.centerMass s w₂ z = Finset.centerMass s (fun 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.centerMass_ite_eq
{R : Type u_1}
{E : Type u_3}
{ι : Type u_5}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
(i : ι)
(t : Finset ι)
(z : ι → E)
(hi : i ∈ t)
:
Finset.centerMass t (fun j => if i = j then 1 else 0) z = z i
theorem
Finset.centerMass_subset
{R : Type u_1}
{E : Type u_3}
{ι : Type u_5}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
{t : Finset ι}
{w : ι → R}
(z : ι → E)
{t' : Finset ι}
(ht : t ⊆ t')
(h : ∀ (i : ι), i ∈ t' → ¬i ∈ t → w i = 0)
:
Finset.centerMass t w z = Finset.centerMass t' w z
theorem
Finset.centerMass_filter_ne_zero
{R : Type u_1}
{E : Type u_3}
{ι : Type u_5}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
{t : Finset ι}
{w : ι → R}
(z : ι → E)
:
Finset.centerMass (Finset.filter (fun i => w i ≠ 0) t) w z = Finset.centerMass t w z
theorem
Finset.centerMass_le_sup
{R : Type u_1}
{ι : Type u_5}
{α : Type u_7}
[LinearOrderedField R]
[LinearOrderedAddCommGroup α]
[Module R α]
[OrderedSMul R α]
{s : Finset ι}
{f : ι → α}
{w : ι → R}
(hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i)
(hw₁ : 0 < Finset.sum s fun i => w i)
:
Finset.centerMass s w f ≤ Finset.sup' s (_ : Finset.Nonempty s) f
theorem
Finset.inf_le_centerMass
{R : Type u_1}
{ι : Type u_5}
{α : Type u_7}
[LinearOrderedField R]
[LinearOrderedAddCommGroup α]
[Module R α]
[OrderedSMul R α]
{s : Finset ι}
{f : ι → α}
{w : ι → R}
(hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i)
(hw₁ : 0 < Finset.sum s fun i => w i)
:
Finset.inf' s (_ : Finset.Nonempty s) f ≤ Finset.centerMass s w f
theorem
Finset.centerMass_of_sum_add_sum_eq_zero
{R : Type u_1}
{E : Type u_3}
{ι : Type u_5}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
{w : ι → R}
{z : ι → E}
{s : Finset ι}
{t : Finset ι}
(hw : ((Finset.sum s fun i => w i) + Finset.sum t fun i => w i) = 0)
(hz : ((Finset.sum s fun i => w i • z i) + Finset.sum t fun i => w i • z i) = 0)
:
Finset.centerMass s w z = Finset.centerMass t w z
theorem
Convex.centerMass_mem
{R : Type u_1}
{E : Type u_3}
{ι : Type u_5}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
{s : Set E}
{t : Finset ι}
{w : ι → R}
{z : ι → E}
(hs : Convex R s)
:
(∀ (i : ι), i ∈ t → 0 ≤ w i) →
(0 < Finset.sum t fun i => w i) → (∀ (i : ι), i ∈ t → z i ∈ s) → Finset.centerMass t w z ∈ 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.sum_mem
{R : Type u_1}
{E : Type u_3}
{ι : Type u_5}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
{s : Set E}
{t : Finset ι}
{w : ι → R}
{z : ι → E}
(hs : Convex R s)
(h₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i)
(h₁ : (Finset.sum t fun i => w i) = 1)
(hz : ∀ (i : ι), i ∈ t → z i ∈ s)
:
(Finset.sum t fun i => w i • z i) ∈ s
theorem
Convex.finsum_mem
{R : Type u_1}
{E : Type u_3}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
{ι : Sort u_8}
{w : ι → R}
{z : ι → E}
{s : Set E}
(hs : Convex R s)
(h₀ : ∀ (i : ι), 0 ≤ w i)
(h₁ : ∑ᶠ (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 i belongs to s. See also
PartitionOfUnity.finsum_smul_mem_convex.
theorem
convex_iff_sum_mem
{R : Type u_1}
{E : Type u_3}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
{s : Set E}
:
theorem
Finset.centerMass_mem_convexHull
{R : Type u_1}
{E : Type u_3}
{ι : Type u_5}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
{s : Set E}
(t : Finset ι)
{w : ι → R}
(hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i)
(hws : 0 < Finset.sum t fun i => w i)
{z : ι → E}
(hz : ∀ (i : ι), i ∈ t → z i ∈ s)
:
Finset.centerMass t w z ∈ ↑(convexHull R) s
theorem
Finset.centerMass_mem_convexHull_of_nonpos
{R : Type u_1}
{E : Type u_3}
{ι : Type u_5}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
{s : Set E}
{w : ι → R}
{z : ι → E}
(t : Finset ι)
(hw₀ : ∀ (i : ι), i ∈ t → w i ≤ 0)
(hws : (Finset.sum t fun i => w i) < 0)
(hz : ∀ (i : ι), i ∈ t → z i ∈ s)
:
Finset.centerMass t w z ∈ ↑(convexHull R) s
A version of Finset.centerMass_mem_convexHull for when the weights are nonpositive.
theorem
Finset.centerMass_id_mem_convexHull
{R : Type u_1}
{E : Type u_3}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
(t : Finset E)
{w : E → R}
(hw₀ : ∀ (i : E), i ∈ t → 0 ≤ w i)
(hws : 0 < Finset.sum t fun i => w i)
:
Finset.centerMass t w id ∈ ↑(convexHull R) ↑t
A refinement of Finset.centerMass_mem_convexHull when the indexed family is a Finset of
the space.
theorem
Finset.centerMass_id_mem_convexHull_of_nonpos
{R : Type u_1}
{E : Type u_3}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
(t : Finset E)
{w : E → R}
(hw₀ : ∀ (i : E), i ∈ t → w i ≤ 0)
(hws : (Finset.sum t fun i => w i) < 0)
:
Finset.centerMass t w id ∈ ↑(convexHull R) ↑t
A version of Finset.centerMass_mem_convexHull for when the weights are nonpositive.
theorem
affineCombination_eq_centerMass
{R : Type u_1}
{E : Type u_3}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
{ι : Type u_8}
{t : Finset ι}
{p : ι → E}
{w : ι → R}
(hw₂ : (Finset.sum t fun i => w i) = 1)
:
↑(Finset.affineCombination R t p) w = Finset.centerMass t w p
theorem
affineCombination_mem_convexHull
{R : Type u_1}
{E : Type u_3}
{ι : Type u_5}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
{s : Finset ι}
{v : ι → E}
{w : ι → R}
(hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i)
(hw₁ : Finset.sum s w = 1)
:
↑(Finset.affineCombination R s v) w ∈ ↑(convexHull R) (Set.range v)
@[simp]
theorem
Finset.centroid_eq_centerMass
{R : Type u_1}
{E : Type u_3}
{ι : Type u_5}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
(s : Finset ι)
(hs : Finset.Nonempty s)
(p : ι → E)
:
Finset.centroid R s p = Finset.centerMass s (Finset.centroidWeights R s) p
The centroid can be regarded as a center of mass.
theorem
Finset.centroid_mem_convexHull
{R : Type u_1}
{E : Type u_3}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
(s : Finset E)
(hs : Finset.Nonempty s)
:
Finset.centroid R s id ∈ ↑(convexHull R) ↑s
theorem
convexHull_range_eq_exists_affineCombination
{R : Type u_1}
{E : Type u_3}
{ι : Type u_5}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
(v : ι → E)
:
↑(convexHull R) (Set.range v) = {x | ∃ s w x_1 x_2, ↑(Finset.affineCombination R s v) w = x}
theorem
convexHull_eq
{R : Type u_1}
{E : Type u_3}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
(s : Set E)
:
↑(convexHull R) s = {x | ∃ ι t w z x_1 x_2 x_3, Finset.centerMass t w z = x}
Convex hull of s is equal to the set of all centers of masses of Finsets t, z '' t ⊆ s.
For universe reasons, you shouldn't use this lemma to prove that a given center of mass belongs
to the convex hull. Use convexity of the convex hull instead.
theorem
Finset.convexHull_eq
{R : Type u_1}
{E : Type u_3}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
(s : Finset E)
:
↑(convexHull R) ↑s = {x | ∃ w x_1 x_2, Finset.centerMass s w id = x}
theorem
Finset.mem_convexHull
{R : Type u_1}
{E : Type u_3}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
{s : Finset E}
{x : E}
:
x ∈ ↑(convexHull R) ↑s ↔ ∃ w x_1 x_2, Finset.centerMass s w id = x
theorem
Set.Finite.convexHull_eq
{R : Type u_1}
{E : Type u_3}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
{s : Set E}
(hs : Set.Finite s)
:
↑(convexHull R) s = {x | ∃ w x_1 x_2, Finset.centerMass (Set.Finite.toFinset hs) w id = x}
theorem
convexHull_eq_union_convexHull_finite_subsets
{R : Type u_1}
{E : Type u_3}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
(s : Set E)
:
↑(convexHull R) s = ⋃ t, ⋃ (_ : ↑t ⊆ s), ↑(convexHull R) ↑t
A weak version of Carathéodory's theorem.
theorem
mk_mem_convexHull_prod
{R : Type u_1}
{E : Type u_3}
{F : Type u_4}
[LinearOrderedField R]
[AddCommGroup E]
[AddCommGroup F]
[Module R E]
[Module R F]
{s : Set E}
{t : Set F}
{x : E}
{y : F}
(hx : x ∈ ↑(convexHull R) s)
(hy : y ∈ ↑(convexHull R) t)
:
(x, y) ∈ ↑(convexHull R) (s ×ˢ t)
@[simp]
theorem
convexHull_prod
{R : Type u_1}
{E : Type u_3}
{F : Type u_4}
[LinearOrderedField R]
[AddCommGroup E]
[AddCommGroup F]
[Module R E]
[Module R F]
(s : Set E)
(t : Set F)
:
↑(convexHull R) (s ×ˢ t) = ↑(convexHull R) s ×ˢ ↑(convexHull R) t
theorem
convexHull_add
{R : Type u_1}
{E : Type u_3}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
(s : Set E)
(t : Set E)
:
↑(convexHull R) (s + t) = ↑(convexHull R) s + ↑(convexHull R) t
@[simp]
theorem
convexHullAddMonoidHom_apply
(R : Type u_1)
(E : Type u_3)
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
(a : Set E)
:
↑(convexHullAddMonoidHom R E) a = ↑(convexHull R) a
noncomputable def
convexHullAddMonoidHom
(R : Type u_1)
(E : Type u_3)
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
:
convexHull is an additive monoid morphism under pointwise addition.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
convexHull_sub
{R : Type u_1}
{E : Type u_3}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
(s : Set E)
(t : Set E)
:
↑(convexHull R) (s - t) = ↑(convexHull R) s - ↑(convexHull R) t
theorem
convexHull_list_sum
{R : Type u_1}
{E : Type u_3}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
(l : List (Set E))
:
↑(convexHull R) (List.sum l) = List.sum (List.map (↑(convexHull R)) l)
theorem
convexHull_multiset_sum
{R : Type u_1}
{E : Type u_3}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
(s : Multiset (Set E))
:
↑(convexHull R) (Multiset.sum s) = Multiset.sum (Multiset.map (↑(convexHull R)) s)
theorem
convexHull_sum
{R : Type u_1}
{E : Type u_3}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
{ι : Type u_8}
(s : Finset ι)
(t : ι → Set E)
:
↑(convexHull R) (Finset.sum s fun i => t i) = Finset.sum s fun i => ↑(convexHull R) (t i)
theorem
convexHull_basis_eq_stdSimplex
{R : Type u_1}
(ι : Type u_5)
[LinearOrderedField R]
[Fintype ι]
:
↑(convexHull R) (Set.range fun i j => if i = j then 1 else 0) = stdSimplex R ι
stdSimplex 𝕜 ι is the convex hull of the canonical basis in ι → 𝕜.
theorem
Set.Finite.convexHull_eq_image
{R : Type u_1}
{E : Type u_3}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
{s : Set E}
(hs : Set.Finite s)
:
↑(convexHull R) s = ↑(Finset.sum Finset.univ fun x => LinearMap.smulRight (LinearMap.proj x) ↑x) '' stdSimplex 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_stdSimplex
{R : Type u_1}
{ι : Type u_5}
[LinearOrderedField R]
[Fintype ι]
{f : ι → R}
(hf : f ∈ stdSimplex R ι)
(x : ι)
:
All values of a function f ∈ stdSimplex 𝕜 ι belong to [0, 1].
theorem
AffineBasis.convexHull_eq_nonneg_coord
{R : Type u_1}
{E : Type u_3}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
{ι : Type u_8}
(b : AffineBasis ι R E)
:
↑(convexHull R) (Set.range ↑b) = {x | ∀ (i : ι), 0 ≤ ↑(AffineBasis.coord b i) x}
The convex hull of an affine basis is the intersection of the half-spaces defined by the corresponding barycentric coordinates.