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} [Field 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

• t.centerMass w z = (∑ i ∈ t, w i)⁻¹ • ∑ i ∈ t, w i • z i

theorem Finset.centerMass_empty {R : Type u_1} {E : Type u_3} {ι : Type u_5} [Field R] [AddCommGroup E] [Module R E] (w : ι → R) (z : ι → E) : ∅.centerMass w z = 0

theorem Finset.centerMass_pair {R : Type u_1} {E : Type u_3} {ι : Type u_5} [Field R] [AddCommGroup E] [Module R E] (i j : ι) (w : ι → R) (z : ι → E) [DecidableEq ι] (hne : i ≠ j) : {i, j}.centerMass w z = (w i / (w i + w j)) • z i + (w j / (w i + w j)) • z j

theorem Finset.centerMass_insert {R : Type u_1} {E : Type u_3} {ι : Type u_5} [Field R] [AddCommGroup E] [Module R E] (i : ι) (t : Finset ι) {w : ι → R} (z : ι → E) [DecidableEq ι] (ha : i ∉ t) (hw : ∑ j ∈ t, w j ≠ 0) : (insert i t).centerMass w z = (w i / (w i + ∑ j ∈ t, w j)) • z i + ((∑ j ∈ t, w j) / (w i + ∑ j ∈ t, w j)) • t.centerMass w z

theorem Finset.centerMass_singleton {R : Type u_1} {E : Type u_3} {ι : Type u_5} [Field R] [AddCommGroup E] [Module R E] (i : ι) {w : ι → R} (z : ι → E) (hw : w i ≠ 0) : {i}.centerMass w z = z i

@[simp]

theorem Finset.centerMass_neg_left {R : Type u_1} {E : Type u_3} {ι : Type u_5} [Field R] [AddCommGroup E] [Module R E] (t : Finset ι) {w : ι → R} (z : ι → E) : t.centerMass (-w) z = t.centerMass w z

theorem Finset.centerMass_smul_left {R : Type u_1} {R' : Type u_2} {E : Type u_3} {ι : Type u_5} [Field R] [Field 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) : t.centerMass (c • w) z = t.centerMass w z

theorem Finset.centerMass_eq_of_sum_1 {R : Type u_1} {E : Type u_3} {ι : Type u_5} [Field R] [AddCommGroup E] [Module R E] (t : Finset ι) {w : ι → R} (z : ι → E) (hw : ∑ i ∈ t, w i = 1) : t.centerMass w z = ∑ i ∈ t, w i • z i

theorem Finset.centerMass_smul {R : Type u_1} {E : Type u_3} {ι : Type u_5} [Field R] [AddCommGroup E] [Module R E] (c : R) (t : Finset ι) {w : ι → R} (z : ι → E) : (t.centerMass w fun (i : ι) => c • z i) = c • t.centerMass w z

theorem Finset.centerMass_segment' {R : Type u_1} {E : Type u_3} {ι : Type u_5} {ι' : Type u_6} [Field R] [AddCommGroup E] [Module R E] (s : Finset ι) (t : Finset ι') (ws : ι → R) (zs : ι → E) (wt : ι' → R) (zt : ι' → E) (hws : ∑ i ∈ s, ws i = 1) (hwt : ∑ i ∈ t, wt i = 1) (a b : R) (hab : a + b = 1) : a • s.centerMass ws zs + b • t.centerMass wt zt = (s.disjSum t).centerMass (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} [Field R] [AddCommGroup E] [Module R E] (s : Finset ι) (w₁ w₂ : ι → R) (z : ι → E) (hw₁ : ∑ i ∈ s, w₁ i = 1) (hw₂ : ∑ i ∈ s, w₂ i = 1) (a b : R) (hab : a + b = 1) : a • s.centerMass w₁ z + b • s.centerMass w₂ z = s.centerMass (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} [Field R] [AddCommGroup E] [Module R E] (i : ι) (t : Finset ι) (z : ι → E) [DecidableEq ι] (hi : i ∈ t) : t.centerMass (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} [Field 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) : t.centerMass w z = t'.centerMass w z

theorem Finset.centerMass_filter_ne_zero {R : Type u_1} {E : Type u_3} {ι : Type u_5} [Field R] [AddCommGroup E] [Module R E] {t : Finset ι} {w : ι → R} (z : ι → E) [(i : ι) → Decidable (w i ≠ 0)] : {i ∈ t | w i ≠ 0}.centerMass w z = t.centerMass w z

theorem Finset.centerMass_le_sup {R : Type u_1} {ι : Type u_5} {α : Type u_7} [Field R] [AddCommGroup α] [LinearOrder α] [Module R α] [LinearOrder R] [IsStrictOrderedRing R] [IsOrderedAddMonoid α] [PosSMulMono R α] {s : Finset ι} {f : ι → α} {w : ι → R} (hw₀ : ∀ i ∈ s, 0 ≤ w i) (hw₁ : 0 < ∑ i ∈ s, w i) : s.centerMass w f ≤ s.sup' ⋯ f

theorem Finset.inf_le_centerMass {R : Type u_1} {ι : Type u_5} {α : Type u_7} [Field R] [AddCommGroup α] [LinearOrder α] [Module R α] [LinearOrder R] [IsStrictOrderedRing R] [IsOrderedAddMonoid α] [PosSMulMono R α] {s : Finset ι} {f : ι → α} {w : ι → R} (hw₀ : ∀ i ∈ s, 0 ≤ w i) (hw₁ : 0 < ∑ i ∈ s, w i) : s.inf' ⋯ f ≤ s.centerMass w f

theorem Finset.centerMass_of_sum_add_sum_eq_zero {R : Type u_1} {E : Type u_3} {ι : Type u_5} [Field R] [AddCommGroup E] [Module R E] {w : ι → R} {z : ι → E} {s t : Finset ι} (hw : ∑ i ∈ s, w i + ∑ i ∈ t, w i = 0) (hz : ∑ i ∈ s, w i • z i + ∑ i ∈ t, w i • z i = 0) : s.centerMass w z = t.centerMass w z

theorem Convex.centerMass_mem {R : Type u_1} {E : Type u_3} {ι : Type u_5} [Field R] [AddCommGroup E] [Module R E] {s : Set E} {t : Finset ι} {w : ι → R} {z : ι → E} [LinearOrder R] [IsStrictOrderedRing R] (hs : Convex R s) : (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, z i ∈ s) → t.centerMass 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} [Field R] [AddCommGroup E] [Module R E] {s : Set E} {t : Finset ι} {w : ι → R} {z : ι → E} [LinearOrder R] [IsStrictOrderedRing R] (hs : Convex R s) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i ∈ t, w i = 1) (hz : ∀ i ∈ t, z i ∈ s) : ∑ i ∈ t, w i • z i ∈ s

theorem Convex.finsum_mem {R : Type u_1} {E : Type u_3} [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] {ι : 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) : ∑ᶠ (i : ι), w i • 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} [Field R] [AddCommGroup E] [Module R E] {s : Set E} [LinearOrder R] [IsStrictOrderedRing R] : Convex R s ↔ ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s

theorem Finset.centerMass_mem_convexHull {R : Type u_1} {E : Type u_3} {ι : Type u_5} [Field R] [AddCommGroup E] [Module R E] {s : Set E} [LinearOrder R] [IsStrictOrderedRing R] (t : Finset ι) {w : ι → R} (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hws : 0 < ∑ i ∈ t, w i) {z : ι → E} (hz : ∀ i ∈ t, z i ∈ s) : t.centerMass w z ∈ (convexHull R) s

theorem Finset.centerMass_mem_convexHull_of_nonpos {R : Type u_1} {E : Type u_3} {ι : Type u_5} [Field R] [AddCommGroup E] [Module R E] {s : Set E} {w : ι → R} {z : ι → E} [LinearOrder R] [IsStrictOrderedRing R] (t : Finset ι) (hw₀ : ∀ i ∈ t, w i ≤ 0) (hws : ∑ i ∈ t, w i < 0) (hz : ∀ i ∈ t, z i ∈ s) : t.centerMass 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} [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] (t : Finset E) {w : E → R} (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hws : 0 < ∑ i ∈ t, w i) : t.centerMass 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} [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] (t : Finset E) {w : E → R} (hw₀ : ∀ i ∈ t, w i ≤ 0) (hws : ∑ i ∈ t, w i < 0) : t.centerMass 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} [Field R] [AddCommGroup E] [Module R E] {ι : Type u_8} {t : Finset ι} {p : ι → E} {w : ι → R} (hw₂ : ∑ i ∈ t, w i = 1) : (Finset.affineCombination R t p) w = t.centerMass w p

theorem affineCombination_mem_convexHull {R : Type u_1} {E : Type u_3} {ι : Type u_5} [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] {s : Finset ι} {v : ι → E} {w : ι → R} (hw₀ : ∀ i ∈ s, 0 ≤ w i) (hw₁ : s.sum 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} [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] (s : Finset ι) (hs : s.Nonempty) (p : ι → E) : centroid R s p = s.centerMass (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} [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] (s : Finset E) (hs : s.Nonempty) : centroid R s id ∈ (convexHull R) ↑s

theorem convexHull_range_eq_exists_affineCombination {R : Type u_1} {E : Type u_3} {ι : Type u_5} [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] (v : ι → E) : (convexHull R) (Set.range v) = {x : E | ∃ (s : Finset ι) (w : ι → R), (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (Finset.affineCombination R s v) w = x}

theorem convexHull_eq {R : Type u_1} {E : Type u_3} [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] (s : Set E) : (convexHull R) s = {x : E | ∃ (ι : Type) (t : Finset ι) (w : ι → R) (z : ι → E), (∀ i ∈ t, 0 ≤ w i) ∧ ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass 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 mem_convexHull_of_exists_fintype {R : Type u_1} {E : Type u_3} {ι : Type u_5} [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] {s : Set E} {x : E} [Fintype ι] (w : ι → R) (z : ι → E) (hw₀ : ∀ (i : ι), 0 ≤ w i) (hw₁ : ∑ i : ι, w i = 1) (hz : ∀ (i : ι), z i ∈ s) (hx : ∑ i : ι, w i • z i = x) : x ∈ (convexHull R) s

Universe polymorphic version of the reverse implication of mem_convexHull_iff_exists_fintype.

theorem mem_convexHull_iff_exists_fintype {R : Type u_1} {E : Type u_3} [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] {s : Set E} {x : E} : x ∈ (convexHull R) s ↔ ∃ (ι : Type) (x_1 : Fintype ι) (w : ι → R) (z : ι → E), (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i : ι, w i • z i = x

The convex hull of s is equal to the set of centers of masses of finite families of points in s.

For universe reasons, you shouldn't use this lemma to prove that a given center of mass belongs to the convex hull. Use mem_convexHull_of_exists_fintype of the convex hull instead.

theorem Finset.convexHull_eq {R : Type u_1} {E : Type u_3} [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] (s : Finset E) : (convexHull R) ↑s = {x : E | ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x}

theorem Finset.mem_convexHull {R : Type u_1} {E : Type u_3} [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] {s : Finset E} {x : E} : x ∈ (convexHull R) ↑s ↔ ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x

theorem Finset.mem_convexHull' {R : Type u_1} {E : Type u_3} [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] {s : Finset E} {x : E} : x ∈ (convexHull R) ↑s ↔ ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ ∑ y ∈ s, 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} [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] {s : Set E} (hs : s.Finite) : (convexHull R) s = {x : E | ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ hs.toFinset, w y = 1 ∧ hs.toFinset.centerMass w id = x}

theorem convexHull_eq_union_convexHull_finite_subsets {R : Type u_1} {E : Type u_3} [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] (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} [Field R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] {s : Set E} [LinearOrder R] [IsStrictOrderedRing R] {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} [Field R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [LinearOrder R] [IsStrictOrderedRing R] (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} [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] (s t : Set E) : (convexHull R) (s + t) = (convexHull R) s + (convexHull R) t

noncomputable def convexHullAddMonoidHom (R : Type u_1) (E : Type u_3) [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] : Set E →+ Set E

convexHull is an additive monoid morphism under pointwise addition.

Equations

• convexHullAddMonoidHom R E = { toFun := ⇑(convexHull R), map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem convexHullAddMonoidHom_apply (R : Type u_1) (E : Type u_3) [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] (a : Set E) : (convexHullAddMonoidHom R E) a = (convexHull R) a

theorem convexHull_sub {R : Type u_1} {E : Type u_3} [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] (s 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} [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] (l : List (Set E)) : (convexHull R) l.sum = (List.map (⇑(convexHull R)) l).sum

theorem convexHull_multiset_sum {R : Type u_1} {E : Type u_3} [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] (s : Multiset (Set E)) : (convexHull R) s.sum = (Multiset.map (⇑(convexHull R)) s).sum

theorem convexHull_sum {R : Type u_1} {E : Type u_3} [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] {ι : Type u_8} (s : Finset ι) (t : ι → Set E) : (convexHull R) (∑ i ∈ s, t i) = ∑ i ∈ s, (convexHull R) (t i)

theorem AffineBasis.convexHull_eq_nonneg_coord {R : Type u_1} {E : Type u_3} [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] {ι : Type u_8} (b : AffineBasis ι R E) : (convexHull R) (Set.range ⇑b) = {x : E | ∀ (i : ι), 0 ≤ (b.coord 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} [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] {s t₁ 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} [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] {t₁ t₂ : Finset E} [DecidableEq 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.

theorem mem_convexHull_pi {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} [Finite ι] [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] {s : Set ι} {t : (i : ι) → Set (E i)} {x : (i : ι) → E i} (h : ∀ i ∈ s, x i ∈ (convexHull 𝕜) (t i)) : x ∈ (convexHull 𝕜) (s.pi t)

@[simp]

theorem convexHull_pi {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} [Finite ι] [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] (s : Set ι) (t : (i : ι) → Set (E i)) : (convexHull 𝕜) (s.pi t) = s.pi fun (i : ι) => (convexHull 𝕜) (t i)