mathlib documentation

analysis.convex.combination

Convex combinations #

This file defines convex combinations of points in a vector space.

Main declarations #

Implementation notes #

We divide by the sum of the weights in the definition of finset.center_mass 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.center_mass {R : Type u_1} {E : Type u_2} {ι : Type u_4} [linear_ordered_field R] [add_comm_group 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
theorem finset.center_mass_empty {R : Type u_1} {E : Type u_2} {ι : Type u_4} [linear_ordered_field R] [add_comm_group E] [module R E] (w : ι R) (z : ι E) :
theorem finset.center_mass_pair {R : Type u_1} {E : Type u_2} {ι : Type u_4} [linear_ordered_field R] [add_comm_group E] [module R E] (i j : ι) (w : ι R) (z : ι E) (hne : i j) :
{i, j}.center_mass w z = (w i / (w i + w j)) z i + (w j / (w i + w j)) z j
theorem finset.center_mass_insert {R : Type u_1} {E : Type u_2} {ι : Type u_4} [linear_ordered_field R] [add_comm_group E] [module R E] (i : ι) (t : finset ι) {w : ι R} (z : ι E) (ha : i t) (hw : t.sum (λ (j : ι), w j) 0) :
(has_insert.insert i t).center_mass w z = (w i / (w i + t.sum (λ (j : ι), w j))) z i + (t.sum (λ (j : ι), w j) / (w i + t.sum (λ (j : ι), w j))) t.center_mass w z
theorem finset.center_mass_singleton {R : Type u_1} {E : Type u_2} {ι : Type u_4} [linear_ordered_field R] [add_comm_group E] [module R E] (i : ι) {w : ι R} (z : ι E) (hw : w i 0) :
{i}.center_mass w z = z i
theorem finset.center_mass_eq_of_sum_1 {R : Type u_1} {E : Type u_2} {ι : Type u_4} [linear_ordered_field R] [add_comm_group E] [module R E] (t : finset ι) {w : ι R} (z : ι E) (hw : t.sum (λ (i : ι), w i) = 1) :
t.center_mass w z = t.sum (λ (i : ι), w i z i)
theorem finset.center_mass_smul {R : Type u_1} {E : Type u_2} {ι : Type u_4} [linear_ordered_field R] [add_comm_group E] [module R E] (c : R) (t : finset ι) {w : ι R} (z : ι E) :
t.center_mass w (λ (i : ι), c z i) = c t.center_mass w z
theorem finset.center_mass_segment' {R : Type u_1} {E : Type u_2} {ι : Type u_4} {ι' : Type u_5} [linear_ordered_field R] [add_comm_group E] [module R E] (s : finset ι) (t : finset ι') (ws : ι R) (zs : ι E) (wt : ι' R) (zt : ι' E) (hws : s.sum (λ (i : ι), ws i) = 1) (hwt : t.sum (λ (i : ι'), wt i) = 1) (a b : R) (hab : a + b = 1) :
a s.center_mass ws zs + b t.center_mass wt zt = (s.disj_sum t).center_mass (sum.elim (λ (i : ι), a * ws i) (λ (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.center_mass_segment {R : Type u_1} {E : Type u_2} {ι : Type u_4} [linear_ordered_field R] [add_comm_group E] [module R E] (s : finset ι) (w₁ w₂ : ι R) (z : ι E) (hw₁ : s.sum (λ (i : ι), w₁ i) = 1) (hw₂ : s.sum (λ (i : ι), w₂ i) = 1) (a b : R) (hab : a + b = 1) :
a s.center_mass w₁ z + b s.center_mass w₂ z = s.center_mass (λ (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.center_mass_ite_eq {R : Type u_1} {E : Type u_2} {ι : Type u_4} [linear_ordered_field R] [add_comm_group E] [module R E] (i : ι) (t : finset ι) (z : ι E) (hi : i t) :
t.center_mass (λ (j : ι), ite (i = j) 1 0) z = z i
theorem finset.center_mass_subset {R : Type u_1} {E : Type u_2} {ι : Type u_4} [linear_ordered_field R] [add_comm_group E] [module R E] {t : finset ι} {w : ι R} (z : ι E) {t' : finset ι} (ht : t t') (h : (i : ι), i t' i t w i = 0) :
theorem finset.center_mass_filter_ne_zero {R : Type u_1} {E : Type u_2} {ι : Type u_4} [linear_ordered_field R] [add_comm_group E] [module R E] {t : finset ι} {w : ι R} (z : ι E) :
(finset.filter (λ (i : ι), w i 0) t).center_mass w z = t.center_mass w z
theorem finset.center_mass_le_sup {R : Type u_1} {ι : Type u_4} {α : Type u_6} [linear_ordered_field R] [linear_ordered_add_comm_group α] [module R α] [ordered_smul R α] {s : finset ι} {f : ι α} {w : ι R} (hw₀ : (i : ι), i s 0 w i) (hw₁ : 0 < s.sum (λ (i : ι), w i)) :
s.center_mass w f s.sup' _ f
theorem finset.inf_le_center_mass {R : Type u_1} {ι : Type u_4} {α : Type u_6} [linear_ordered_field R] [linear_ordered_add_comm_group α] [module R α] [ordered_smul R α] {s : finset ι} {f : ι α} {w : ι R} (hw₀ : (i : ι), i s 0 w i) (hw₁ : 0 < s.sum (λ (i : ι), w i)) :
s.inf' _ f s.center_mass w f
theorem convex.center_mass_mem {R : Type u_1} {E : Type u_2} {ι : Type u_4} [linear_ordered_field R] [add_comm_group E] [module R E] {s : set E} {t : finset ι} {w : ι R} {z : ι E} (hs : convex R s) :
( (i : ι), i t 0 w i) 0 < t.sum (λ (i : ι), w i) ( (i : ι), i t z i s) t.center_mass 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_2} {ι : Type u_4} [linear_ordered_field R] [add_comm_group 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₁ : t.sum (λ (i : ι), w i) = 1) (hz : (i : ι), i t z i s) :
t.sum (λ (i : ι), w i z i) s
theorem convex.finsum_mem {R : Type u_1} {E : Type u_2} [linear_ordered_field R] [add_comm_group E] [module R E] {ι : Sort u_3} {w : ι R} {z : ι E} {s : set E} (hs : convex R s) (h₀ : (i : ι), 0 w i) (h₁ : finsum (λ (i : ι), w i) = 1) (hz : (i : ι), w i 0 z i s) :
finsum (λ (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 ibelongs tos. See alsopartition_of_unity.finsum_smul_mem_convex`.

theorem convex_iff_sum_mem {R : Type u_1} {E : Type u_2} [linear_ordered_field R] [add_comm_group E] [module R E] {s : set E} :
convex R s (t : finset E) (w : E R), ( (i : E), i t 0 w i) t.sum (λ (i : E), w i) = 1 ( (x : E), x t x s) t.sum (λ (x : E), w x x) s
theorem finset.center_mass_mem_convex_hull {R : Type u_1} {E : Type u_2} {ι : Type u_4} [linear_ordered_field R] [add_comm_group E] [module R E] {s : set E} (t : finset ι) {w : ι R} (hw₀ : (i : ι), i t 0 w i) (hws : 0 < t.sum (λ (i : ι), w i)) {z : ι E} (hz : (i : ι), i t z i s) :
theorem finset.center_mass_id_mem_convex_hull {R : Type u_1} {E : Type u_2} [linear_ordered_field R] [add_comm_group E] [module R E] (t : finset E) {w : E R} (hw₀ : (i : E), i t 0 w i) (hws : 0 < t.sum (λ (i : E), w i)) :

A refinement of finset.center_mass_mem_convex_hull when the indexed family is a finset of the space.

theorem affine_combination_eq_center_mass {R : Type u_1} {E : Type u_2} [linear_ordered_field R] [add_comm_group E] [module R E] {ι : Type u_3} {t : finset ι} {p : ι E} {w : ι R} (hw₂ : t.sum (λ (i : ι), w i) = 1) :
theorem affine_combination_mem_convex_hull {R : Type u_1} {E : Type u_2} {ι : Type u_4} [linear_ordered_field R] [add_comm_group E] [module R E] {s : finset ι} {v : ι E} {w : ι R} (hw₀ : (i : ι), i s 0 w i) (hw₁ : s.sum w = 1) :
@[simp]
theorem finset.centroid_eq_center_mass {R : Type u_1} {E : Type u_2} {ι : Type u_4} [linear_ordered_field R] [add_comm_group E] [module R E] (s : finset ι) (hs : s.nonempty) (p : ι E) :

The centroid can be regarded as a center of mass.

theorem convex_hull_range_eq_exists_affine_combination {R : Type u_1} {E : Type u_2} {ι : Type u_4} [linear_ordered_field R] [add_comm_group E] [module R E] (v : ι E) :
(convex_hull R) (set.range v) = {x : E | (s : finset ι) (w : ι R) (hw₀ : (i : ι), i s 0 w i) (hw₁ : s.sum w = 1), (s.affine_combination v) w = x}
theorem convex_hull_eq {R : Type u_1} {E : Type u_2} [linear_ordered_field R] [add_comm_group E] [module R E] (s : set E) :
(convex_hull R) s = {x : E | (ι : Type u') (t : finset ι) (w : ι R) (z : ι E) (hw₀ : (i : ι), i t 0 w i) (hw₁ : t.sum (λ (i : ι), w i) = 1) (hz : (i : ι), i t z i s), t.center_mass w z = x}

Convex hull of s is equal to the set of all centers of masses of finsets t, z '' t ⊆ s. This version allows finsets in any type in any universe.

theorem finset.convex_hull_eq {R : Type u_1} {E : Type u_2} [linear_ordered_field R] [add_comm_group E] [module R E] (s : finset E) :
(convex_hull R) s = {x : E | (w : E R) (hw₀ : (y : E), y s 0 w y) (hw₁ : s.sum (λ (y : E), w y) = 1), s.center_mass w id = x}
theorem finset.mem_convex_hull {R : Type u_1} {E : Type u_2} [linear_ordered_field R] [add_comm_group E] [module R E] {s : finset E} {x : E} :
x (convex_hull R) s (w : E R) (hw₀ : (y : E), y s 0 w y) (hw₁ : s.sum (λ (y : E), w y) = 1), s.center_mass w id = x
theorem set.finite.convex_hull_eq {R : Type u_1} {E : Type u_2} [linear_ordered_field R] [add_comm_group E] [module R E] {s : set E} (hs : s.finite) :
(convex_hull R) s = {x : E | (w : E R) (hw₀ : (y : E), y s 0 w y) (hw₁ : hs.to_finset.sum (λ (y : E), w y) = 1), hs.to_finset.center_mass w id = x}

A weak version of Carathéodory's theorem.

theorem mk_mem_convex_hull_prod {R : Type u_1} {E : Type u_2} {F : Type u_3} [linear_ordered_field R] [add_comm_group E] [add_comm_group F] [module R E] [module R F] {s : set E} {t : set F} {x : E} {y : F} (hx : x (convex_hull R) s) (hy : y (convex_hull R) t) :
(x, y) (convex_hull R) (s ×ˢ t)
@[simp]
theorem convex_hull_prod {R : Type u_1} {E : Type u_2} {F : Type u_3} [linear_ordered_field R] [add_comm_group E] [add_comm_group F] [module R E] [module R F] (s : set E) (t : set F) :
theorem convex_hull_add {R : Type u_1} {E : Type u_2} [linear_ordered_field R] [add_comm_group E] [module R E] (s t : set E) :
theorem convex_hull_sub {R : Type u_1} {E : Type u_2} [linear_ordered_field R] [add_comm_group E] [module R E] (s t : set E) :

std_simplex #

theorem convex_hull_basis_eq_std_simplex {R : Type u_1} (ι : Type u_4) [linear_ordered_field R] [fintype ι] :
(convex_hull R) (set.range (λ (i j : ι), ite (i = j) 1 0)) = std_simplex R ι

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

theorem set.finite.convex_hull_eq_image {R : Type u_1} {E : Type u_2} [linear_ordered_field R] [add_comm_group E] [module R E] {s : set E} (hs : s.finite) :

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_std_simplex {R : Type u_1} {ι : Type u_4} [linear_ordered_field R] [fintype ι] {f : ι R} (hf : f std_simplex R ι) (x : ι) :
f x set.Icc 0 1

All values of a function f ∈ std_simplex 𝕜 ι belong to [0, 1].

theorem convex_hull_affine_basis_eq_nonneg_barycentric {R : Type u_1} {E : Type u_2} [linear_ordered_field R] [add_comm_group E] [module R E] {ι : Type u_3} (b : affine_basis ι R E) :
(convex_hull R) (set.range b.points) = {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.