# 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} [] [Module R E] (t : ) (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 = (t.sum fun (i : ι) => w i)⁻¹ t.sum fun (i : ι) => w i z i
Instances For
theorem Finset.centerMass_empty {R : Type u_1} {E : Type u_3} {ι : Type u_5} [] [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} [] [Module R E] (i : ι) (j : ι) (w : ιR) (z : ιE) (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} [] [Module R E] (i : ι) (t : ) {w : ιR} (z : ιE) (ha : it) (hw : (t.sum fun (j : ι) => w j) 0) :
(insert i t).centerMass w z = (w i / (w i + t.sum fun (j : ι) => w j)) z i + ((t.sum fun (j : ι) => w j) / (w i + t.sum fun (j : ι) => w j)) t.centerMass w z
theorem Finset.centerMass_singleton {R : Type u_1} {E : Type u_3} {ι : Type u_5} [] [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} [] [Module R E] (t : ) {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} [] [] [Module R E] (t : ) {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} [] [Module R E] (t : ) {w : ιR} (z : ιE) (hw : (t.sum fun (i : ι) => w i) = 1) :
t.centerMass w z = t.sum fun (i : ι) => w i z i
theorem Finset.centerMass_smul {R : Type u_1} {E : Type u_3} {ι : Type u_5} [] [Module R E] (c : R) (t : ) {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} [] [Module R E] (s : ) (t : Finset ι') (ws : ιR) (zs : ιE) (wt : ι'R) (zt : ι'E) (hws : (s.sum fun (i : ι) => ws i) = 1) (hwt : (t.sum fun (i : ι') => wt i) = 1) (a : R) (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} [] [Module R E] (s : ) (w₁ : ιR) (w₂ : ιR) (z : ιE) (hw₁ : (s.sum fun (i : ι) => w₁ i) = 1) (hw₂ : (s.sum fun (i : ι) => w₂ i) = 1) (a : R) (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} [] [Module R E] (i : ι) (t : ) (z : ιE) (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} [] [Module R E] {t : } {w : ιR} (z : ιE) {t' : } (ht : t t') (h : it', itw 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} [] [Module R E] {t : } {w : ιR} (z : ιE) :
(Finset.filter (fun (i : ι) => w i 0) t).centerMass w z = t.centerMass w z
theorem Finset.centerMass_le_sup {R : Type u_1} {ι : Type u_5} {α : Type u_7} [Module R α] [] {s : } {f : ια} {w : ιR} (hw₀ : is, 0 w i) (hw₁ : 0 < s.sum fun (i : ι) => w i) :
s.centerMass w f s.sup' f
theorem Finset.inf_le_centerMass {R : Type u_1} {ι : Type u_5} {α : Type u_7} [Module R α] [] {s : } {f : ια} {w : ιR} (hw₀ : is, 0 w i) (hw₁ : 0 < s.sum fun (i : ι) => 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} [] [Module R E] {w : ιR} {z : ιE} {s : } {t : } (hw : ((s.sum fun (i : ι) => w i) + t.sum fun (i : ι) => w i) = 0) (hz : ((s.sum fun (i : ι) => w i z i) + t.sum fun (i : ι) => 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} [] [Module R E] {s : Set E} {t : } {w : ιR} {z : ιE} (hs : Convex R s) :
(it, 0 w i)(0 < t.sum fun (i : ι) => w i)(it, 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} [] [Module R E] {s : Set E} {t : } {w : ιR} {z : ιE} (hs : Convex R s) (h₀ : it, 0 w i) (h₁ : (t.sum fun (i : ι) => w i) = 1) (hz : it, z i s) :
(t.sum fun (i : ι) => w i z i) s
theorem Convex.finsum_mem {R : Type u_1} {E : Type u_3} [] [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 0z i s) :
(finsum fun (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} [] [Module R E] {s : Set E} :
Convex R s ∀ (t : ) (w : ER), (it, 0 w i)(t.sum fun (i : E) => w i) = 1(xt, x s)(t.sum fun (x : E) => w x x) s
theorem Finset.centerMass_mem_convexHull {R : Type u_1} {E : Type u_3} {ι : Type u_5} [] [Module R E] {s : Set E} (t : ) {w : ιR} (hw₀ : it, 0 w i) (hws : 0 < t.sum fun (i : ι) => w i) {z : ιE} (hz : it, z i s) :
t.centerMass w z () s
theorem Finset.centerMass_mem_convexHull_of_nonpos {R : Type u_1} {E : Type u_3} {ι : Type u_5} [] [Module R E] {s : Set E} {w : ιR} {z : ιE} (t : ) (hw₀ : it, w i 0) (hws : (t.sum fun (i : ι) => w i) < 0) (hz : it, z i s) :
t.centerMass w z () 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} [] [Module R E] (t : ) {w : ER} (hw₀ : it, 0 w i) (hws : 0 < t.sum fun (i : E) => w i) :
t.centerMass w id () 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} [] [Module R E] (t : ) {w : ER} (hw₀ : it, w i 0) (hws : (t.sum fun (i : E) => w i) < 0) :
t.centerMass w id () 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} [] [Module R E] {ι : Type u_8} {t : } {p : ιE} {w : ιR} (hw₂ : (t.sum fun (i : ι) => w i) = 1) :
() w = t.centerMass w p
theorem affineCombination_mem_convexHull {R : Type u_1} {E : Type u_3} {ι : Type u_5} [] [Module R E] {s : } {v : ιE} {w : ιR} (hw₀ : is, 0 w i) (hw₁ : s.sum w = 1) :
() w () ()
@[simp]
theorem Finset.centroid_eq_centerMass {R : Type u_1} {E : Type u_3} {ι : Type u_5} [] [Module R E] (s : ) (hs : s.Nonempty) (p : ιE) :
= s.centerMass () p

The centroid can be regarded as a center of mass.

theorem Finset.centroid_mem_convexHull {R : Type u_1} {E : Type u_3} [] [Module R E] (s : ) (hs : s.Nonempty) :
Finset.centroid R s id () s
theorem convexHull_range_eq_exists_affineCombination {R : Type u_1} {E : Type u_3} {ι : Type u_5} [] [Module R E] (v : ιE) :
() () = {x : E | ∃ (s : ) (w : ιR), (is, 0 w i) s.sum w = 1 () w = x}
theorem convexHull_eq {R : Type u_1} {E : Type u_3} [] [Module R E] (s : Set E) :
() s = {x : E | ∃ (ι : Type) (t : ) (w : ιR) (z : ιE), (it, 0 w i) (t.sum fun (i : ι) => w i) = 1 (it, 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 Finset.convexHull_eq {R : Type u_1} {E : Type u_3} [] [Module R E] (s : ) :
() s = {x : E | ∃ (w : ER), (ys, 0 w y) (s.sum fun (y : E) => w y) = 1 s.centerMass w id = x}
theorem Finset.mem_convexHull {R : Type u_1} {E : Type u_3} [] [Module R E] {s : } {x : E} :
x () s ∃ (w : ER), (ys, 0 w y) (s.sum fun (y : E) => w y) = 1 s.centerMass w id = x
theorem Finset.mem_convexHull' {R : Type u_1} {E : Type u_3} [] [Module R E] {s : } {x : E} :
x () s ∃ (w : ER), (ys, 0 w y) (s.sum fun (y : E) => w y) = 1 (s.sum 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} [] [Module R E] {s : Set E} (hs : s.Finite) :
() s = {x : E | ∃ (w : ER), (ys, 0 w y) (hs.toFinset.sum fun (y : E) => w y) = 1 hs.toFinset.centerMass w id = x}
theorem convexHull_eq_union_convexHull_finite_subsets {R : Type u_1} {E : Type u_3} [] [Module R E] (s : Set E) :
() s = ⋃ (t : ), ⋃ (_ : t s), () 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} [] [] [Module R E] [Module R F] {s : Set E} {t : Set F} {x : E} {y : F} (hx : x () s) (hy : y () t) :
(x, y) () (s ×ˢ t)
@[simp]
theorem convexHull_prod {R : Type u_1} {E : Type u_3} {F : Type u_4} [] [] [Module R E] [Module R F] (s : Set E) (t : Set F) :
() (s ×ˢ t) = () s ×ˢ () t
theorem convexHull_add {R : Type u_1} {E : Type u_3} [] [Module R E] (s : Set E) (t : Set E) :
() (s + t) = () s + () t
@[simp]
theorem convexHullAddMonoidHom_apply (R : Type u_1) (E : Type u_3) [] [Module R E] (a : Set E) :
() a = () a
def convexHullAddMonoidHom (R : Type u_1) (E : Type u_3) [] [Module R E] :

convexHull is an additive monoid morphism under pointwise addition.

Equations
• = { toFun := (), map_zero' := , map_add' := }
Instances For
theorem convexHull_sub {R : Type u_1} {E : Type u_3} [] [Module R E] (s : Set E) (t : Set E) :
() (s - t) = () s - () t
theorem convexHull_list_sum {R : Type u_1} {E : Type u_3} [] [Module R E] (l : List (Set E)) :
() l.sum = (List.map (()) l).sum
theorem convexHull_multiset_sum {R : Type u_1} {E : Type u_3} [] [Module R E] (s : Multiset (Set E)) :
() s.sum = (Multiset.map (()) s).sum
theorem convexHull_sum {R : Type u_1} {E : Type u_3} [] [Module R E] {ι : Type u_8} (s : ) (t : ιSet E) :
() (s.sum fun (i : ι) => t i) = s.sum fun (i : ι) => () (t i)

### stdSimplex#

theorem convexHull_basis_eq_stdSimplex {R : Type u_1} (ι : Type u_5) [] :
() (Set.range fun (i j : ι) => if i = j then 1 else 0) =

stdSimplex 𝕜 ι is the convex hull of the canonical basis in ι → 𝕜.

theorem Set.Finite.convexHull_eq_image {R : Type u_1} {E : Type u_3} [] [Module R E] {s : Set E} (hs : s.Finite) :
() s = (Finset.univ.sum fun (x : s) => ().smulRight 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} [] {f : ιR} (hf : f ) (x : ι) :
f x Set.Icc 0 1

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} [] [Module R E] {ι : Type u_8} (b : AffineBasis ι R E) :
() () = {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} [] [Module R E] {s : } {t₁ : } {t₂ : } (hs : AffineIndependent R Subtype.val) (ht₁ : t₁ s) (ht₂ : t₂ s) :
() (t₁ t₂) = () t₁ () 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} [] [Module R E] {t₁ : } {t₂ : } (hs : AffineIndependent R Subtype.val) :
() (t₁ t₂) = () t₁ () 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.