# Documentation

Mathlib.Analysis.Convex.Combination

# 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.

Instances For
theorem Finset.centerMass_empty {R : Type u_1} {E : Type u_3} {ι : Type u_5} [] [Module R E] (w : ιR) (z : ιE) :
= 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) :
Finset.centerMass {i, j} 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 : ¬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))
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) :
Finset.centerMass {i} 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) :
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) :
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 : (Finset.sum t fun i => w i) = 1) :
= Finset.sum t 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) :
(Finset.centerMass t w fun i => c z i) = c
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 : (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 () (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₁ : (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 + b = 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} [] [Module R E] (i : ι) (t : ) (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} [] [Module R E] {t : } {w : ιR} (z : ιE) {t' : } (ht : t t') (h : ∀ (i : ι), i t'¬i tw i = 0) :
=
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.centerMass (Finset.filter (fun i => w i 0) t) w z =
theorem Finset.centerMass_le_sup {R : Type u_1} {ι : Type u_5} {α : Type u_7} [Module R α] [] {s : } {f : ια} {w : ιR} (hw₀ : ∀ (i : ι), i s0 w i) (hw₁ : 0 < Finset.sum s fun i => w i) :
Finset.sup' s (_ : ) f
theorem Finset.inf_le_centerMass {R : Type u_1} {ι : Type u_5} {α : Type u_7} [Module R α] [] {s : } {f : ια} {w : ιR} (hw₀ : ∀ (i : ι), i s0 w i) (hw₁ : 0 < Finset.sum s fun i => w i) :
Finset.inf' s (_ : ) 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 : ((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) :
=
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) :
(∀ (i : ι), i t0 w i) → (0 < Finset.sum t fun i => w i) → (∀ (i : ι), i tz i s) → 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₀ : ∀ (i : ι), i t0 w i) (h₁ : (Finset.sum t fun i => w i) = 1) (hz : ∀ (i : ι), i tz i s) :
(Finset.sum t 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₁ : ∑ᶠ (i : ι), w i = 1) (hz : ∀ (i : ι), w i 0z 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} [] [Module R E] {s : Set E} :
Convex R s ∀ (t : ) (w : ER), (∀ (i : E), i t0 w i) → (Finset.sum t fun i => w i) = 1(∀ (x : E), x tx s) → (Finset.sum t fun x => 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₀ : ∀ (i : ι), i t0 w i) (hws : 0 < Finset.sum t fun i => w i) {z : ιE} (hz : ∀ (i : ι), i tz i s) :
↑() 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₀ : ∀ (i : ι), i tw i 0) (hws : (Finset.sum t fun i => w i) < 0) (hz : ∀ (i : ι), i tz i s) :
↑() 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₀ : ∀ (i : E), i t0 w i) (hws : 0 < Finset.sum t fun i => w i) :
↑() 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₀ : ∀ (i : E), i tw i 0) (hws : (Finset.sum t fun i => w i) < 0) :
↑() 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₂ : (Finset.sum t fun i => w i) = 1) :
↑() w =
theorem affineCombination_mem_convexHull {R : Type u_1} {E : Type u_3} {ι : Type u_5} [] [Module R E] {s : } {v : ιE} {w : ιR} (hw₀ : ∀ (i : ι), i s0 w i) (hw₁ : = 1) :
↑() w ↑() ()
@[simp]
theorem Finset.centroid_eq_centerMass {R : Type u_1} {E : Type u_3} {ι : Type u_5} [] [Module R E] (s : ) (hs : ) (p : ιE) :
=

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 : ) :
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 | s w x_1 x_2, ↑() w = x}
theorem convexHull_eq {R : Type u_1} {E : Type u_3} [] [Module R E] (s : Set E) :
↑() s = {x | ι t w z x_1 x_2 x_3, = 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 | w x_1 x_2, = x}
theorem Finset.mem_convexHull {R : Type u_1} {E : Type u_3} [] [Module R E] {s : } {x : E} :
x ↑() s w x x, = x
theorem Set.Finite.convexHull_eq {R : Type u_1} {E : Type u_3} [] [Module R E] {s : Set E} (hs : ) :
↑() s = {x | w x_1 x_2, = 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
noncomputable def convexHullAddMonoidHom (R : Type u_1) (E : Type u_3) [] [Module R E] :

convexHull is an additive monoid morphism under pointwise addition.

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)) :
↑() () = List.sum (List.map (↑()) l)
theorem convexHull_multiset_sum {R : Type u_1} {E : Type u_3} [] [Module R E] (s : Multiset (Set E)) :
↑() () = Multiset.sum (Multiset.map (↑()) s)
theorem convexHull_sum {R : Type u_1} {E : Type u_3} [] [Module R E] {ι : Type u_8} (s : ) (t : ιSet E) :
↑() (Finset.sum s fun i => t i) = Finset.sum s 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 = ↑(Finset.sum Finset.univ fun 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 | ∀ (i : ι), 0 ↑() x}

The convex hull of an affine basis is the intersection of the half-spaces defined by the corresponding barycentric coordinates.