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 ∈ 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 ∈ s, 0 ≤ w i)
(hw₁ : 0 < Finset.sum s fun (i : ι) => w i)
:
Finset.centerMass s w f ≤ Finset.sup' 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 ∈ s, 0 ≤ w i)
(hw₁ : 0 < Finset.sum s fun (i : ι) => w i)
:
Finset.inf' 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 ∈ t, 0 ≤ w i) → (0 < Finset.sum t fun (i : ι) => w 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 ∈ t, 0 ≤ w i)
(h₁ : (Finset.sum t fun (i : ι) => w i) = 1)
(hz : ∀ 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₁ : (finsum fun (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}
:
Convex R s ↔ ∀ (t : Finset E) (w : E → R),
(∀ i ∈ t, 0 ≤ w i) →
(Finset.sum t fun (i : E) => w i) = 1 → (∀ x ∈ t, x ∈ s) → (Finset.sum t fun (x : E) => w x • x) ∈ s
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 ∈ t, 0 ≤ w i)
(hws : 0 < Finset.sum t fun (i : ι) => w i)
{z : ι → E}
(hz : ∀ 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 ∈ t, w i ≤ 0)
(hws : (Finset.sum t fun (i : ι) => w i) < 0)
(hz : ∀ 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 ∈ t, 0 ≤ w i)
(hws : 0 < Finset.sum t fun (i : E) => 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 ∈ t, w i ≤ 0)
(hws : (Finset.sum t fun (i : E) => 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 ∈ 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 : s.Nonempty)
(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 : s.Nonempty)
:
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 : E |
∃ (s : Finset ι) (w : ι → R), (∀ i ∈ s, 0 ≤ w i) ∧ Finset.sum s w = 1 ∧ (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 : E |
∃ (ι : Type) (t : Finset ι) (w : ι → R) (z : ι → E),
(∀ i ∈ t, 0 ≤ w i) ∧ (Finset.sum t fun (i : ι) => w i) = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ 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 : E | ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ (Finset.sum s fun (y : E) => w y) = 1 ∧ 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 : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ (Finset.sum s fun (y : E) => w y) = 1 ∧ 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 : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ (Finset.sum s fun (y : E) => w y) = 1 ∧ (Finset.sum s fun (y : E) => w y • y) = x
This is a version of Finset.mem_convexHull stated without Finset.centerMass.
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 : E |
∃ (w : E → R),
(∀ y ∈ s, 0 ≤ w y) ∧ (Finset.sum (Set.Finite.toFinset hs) fun (y : E) => w y) = 1 ∧ 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 : Finset E), ⋃ (_ : ↑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
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
- convexHullAddMonoidHom R E = { toZeroHom := { toFun := ⇑(convexHull R), map_zero' := ⋯ }, map_add' := ⋯ }
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 : ↑s) => 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 : E | ∀ (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.
theorem
AffineIndependent.convexHull_inter
{R : Type u_1}
{E : Type u_3}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
{s : Finset E}
{t₁ : Finset E}
{t₂ : Finset E}
(hs : AffineIndependent R Subtype.val)
(ht₁ : t₁ ⊆ s)
(ht₂ : t₂ ⊆ s)
:
(convexHull R) (↑t₁ ∩ ↑t₂) = (convexHull R) ↑t₁ ∩ (convexHull R) ↑t₂
Two simplices glue nicely if the union of their vertices is affine independent.
theorem
AffineIndependent.convexHull_inter'
{R : Type u_1}
{E : Type u_3}
[LinearOrderedField R]
[AddCommGroup E]
[Module R E]
{t₁ : Finset E}
{t₂ : Finset E}
(hs : AffineIndependent R Subtype.val)
:
(convexHull R) (↑t₁ ∩ ↑t₂) = (convexHull R) ↑t₁ ∩ (convexHull R) ↑t₂
Two simplices glue nicely if the union of their vertices is affine independent.
Note that AffineIndependent.convexHull_inter should be more versatile in most use cases.