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 = (finset.map function.embedding.inl s finset.map function.embedding.inr 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 tw 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 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 t0 w i)0 < t.sum (λ (i : ι), w i)(∀ (i : ι), i tz 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 t0 w i) (h₁ : t.sum (λ (i : ι), w i) = 1) (hz : ∀ (i : ι), i tz 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 0z 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 t0 w i)t.sum (λ (i : E), w i) = 1(∀ (x : E), x tx 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 t0 w i) (hws : 0 < t.sum (λ (i : ι), w i)) {z : ι → E} (hz : ∀ (i : ι), i tz 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 t0 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 s0 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 finset.centroid_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) (hs : s.nonempty) :
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 s0 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 t0 w i) (hw₁ : t.sum (λ (i : ι), w i) = 1) (hz : ∀ (i : ι), i tz 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 s0 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 s0 w y) (hw₁ : hs.to_finset.sum (λ (y : E), w y) = 1), hs.to_finset.center_mass w id = x}
theorem convex_hull_eq_union_convex_hull_finite_subsets {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 = ⋃ (t : finset E) (w : t s), (convex_hull R) t

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.