Documentation

Mathlib.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.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} [LinearOrderedField 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 = (∑ it, w i)⁻¹ it, w i z i
Instances For
    theorem Finset.centerMass_empty {R : Type u_1} {E : Type u_3} {ι : Type u_5} [LinearOrderedField 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} [LinearOrderedField R] [AddCommGroup E] [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} [LinearOrderedField R] [AddCommGroup E] [Module R E] (i : ι) (t : Finset ι) {w : ιR} (z : ιE) (ha : it) (hw : jt, w j 0) :
    (insert i t).centerMass w z = (w i / (w i + jt, w j)) z i + ((∑ jt, w j) / (w i + jt, w j)) t.centerMass w z
    theorem Finset.centerMass_singleton {R : Type u_1} {E : Type u_3} {ι : Type u_5} [LinearOrderedField 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} [LinearOrderedField 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} [LinearOrderedField R] [LinearOrderedField 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} [LinearOrderedField R] [AddCommGroup E] [Module R E] (t : Finset ι) {w : ιR} (z : ιE) (hw : it, w i = 1) :
    t.centerMass w z = it, w i z i
    theorem Finset.centerMass_smul {R : Type u_1} {E : Type u_3} {ι : Type u_5} [LinearOrderedField 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} [LinearOrderedField R] [AddCommGroup E] [Module R E] (s : Finset ι) (t : Finset ι') (ws : ιR) (zs : ιE) (wt : ι'R) (zt : ι'E) (hws : is, ws i = 1) (hwt : it, 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} [LinearOrderedField R] [AddCommGroup E] [Module R E] (s : Finset ι) (w₁ : ιR) (w₂ : ιR) (z : ιE) (hw₁ : is, w₁ i = 1) (hw₂ : is, 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} [LinearOrderedField R] [AddCommGroup E] [Module R E] (i : ι) (t : Finset ι) (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} [LinearOrderedField R] [AddCommGroup E] [Module R E] {t : Finset ι} {w : ιR} (z : ιE) {t' : Finset ι} (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} [LinearOrderedField R] [AddCommGroup E] [Module R E] {t : Finset ι} {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} [LinearOrderedField R] [LinearOrderedAddCommGroup α] [Module R α] [OrderedSMul R α] {s : Finset ι} {f : ια} {w : ιR} (hw₀ : is, 0 w i) (hw₁ : 0 < is, w i) :
    s.centerMass w f s.sup' f
    theorem Finset.inf_le_centerMass {R : Type u_1} {ι : Type u_5} {α : Type u_7} [LinearOrderedField R] [LinearOrderedAddCommGroup α] [Module R α] [OrderedSMul R α] {s : Finset ι} {f : ια} {w : ιR} (hw₀ : is, 0 w i) (hw₁ : 0 < is, 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} [LinearOrderedField R] [AddCommGroup E] [Module R E] {w : ιR} {z : ιE} {s : Finset ι} {t : Finset ι} (hw : is, w i + it, w i = 0) (hz : is, w i z i + it, 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} [LinearOrderedField R] [AddCommGroup E] [Module R E] {s : Set E} {t : Finset ι} {w : ιR} {z : ιE} (hs : Convex R s) :
    (∀ it, 0 w i)0 < it, 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} [LinearOrderedField R] [AddCommGroup E] [Module R E] {s : Set E} {t : Finset ι} {w : ιR} {z : ιE} (hs : Convex R s) (h₀ : it, 0 w i) (h₁ : it, w i = 1) (hz : it, z i s) :
    it, w i z i s
    theorem Convex.finsum_mem {R : Type u_1} {E : Type u_3} [LinearOrderedField R] [AddCommGroup E] [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} [LinearOrderedField R] [AddCommGroup E] [Module R E] {s : Set E} :
    Convex R s ∀ (t : Finset E) (w : ER), (∀ it, 0 w i)it, w i = 1(∀ xt, x s)xt, w x x s
    theorem Finset.centerMass_mem_convexHull {R : Type u_1} {E : Type u_3} {ι : Type u_5} [LinearOrderedField R] [AddCommGroup E] [Module R E] {s : Set E} (t : Finset ι) {w : ιR} (hw₀ : it, 0 w i) (hws : 0 < it, w i) {z : ιE} (hz : it, 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} [LinearOrderedField R] [AddCommGroup E] [Module R E] {s : Set E} {w : ιR} {z : ιE} (t : Finset ι) (hw₀ : it, w i 0) (hws : it, w i < 0) (hz : it, 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} [LinearOrderedField R] [AddCommGroup E] [Module R E] (t : Finset E) {w : ER} (hw₀ : it, 0 w i) (hws : 0 < it, 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} [LinearOrderedField R] [AddCommGroup E] [Module R E] (t : Finset E) {w : ER} (hw₀ : it, w i 0) (hws : it, 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} [LinearOrderedField R] [AddCommGroup E] [Module R E] {ι : Type u_8} {t : Finset ι} {p : ιE} {w : ιR} (hw₂ : it, 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} [LinearOrderedField R] [AddCommGroup E] [Module R E] {s : Finset ι} {v : ιE} {w : ιR} (hw₀ : is, 0 w i) (hw₁ : s.sum w = 1) :
    @[simp]
    theorem Finset.centroid_eq_centerMass {R : Type u_1} {E : Type u_3} {ι : Type u_5} [LinearOrderedField R] [AddCommGroup E] [Module R E] (s : Finset ι) (hs : s.Nonempty) (p : ιE) :
    Finset.centroid R s p = s.centerMass (Finset.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} [LinearOrderedField R] [AddCommGroup E] [Module R E] (s : Finset E) (hs : s.Nonempty) :
    theorem convexHull_range_eq_exists_affineCombination {R : Type u_1} {E : Type u_3} {ι : Type u_5} [LinearOrderedField R] [AddCommGroup E] [Module R E] (v : ιE) :
    (convexHull R) (Set.range v) = {x : E | ∃ (s : Finset ι) (w : ιR), (∀ is, 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} [LinearOrderedField R] [AddCommGroup E] [Module R E] (s : Set E) :
    (convexHull R) s = {x : E | ∃ (ι : Type) (t : Finset ι) (w : ιR) (z : ιE), (∀ it, 0 w i) it, 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 mem_convexHull_of_exists_fintype {R : Type u_1} {E : Type u_3} {ι : Type u_5} [LinearOrderedField R] [AddCommGroup E] [Module R E] {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} [LinearOrderedField R] [AddCommGroup E] [Module R E] {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} [LinearOrderedField R] [AddCommGroup E] [Module R E] (s : Finset E) :
    (convexHull R) s = {x : E | ∃ (w : ER), (∀ ys, 0 w y) ys, w y = 1 s.centerMass w id = x}
    theorem Finset.mem_convexHull {R : Type u_1} {E : Type u_3} [LinearOrderedField R] [AddCommGroup E] [Module R E] {s : Finset E} {x : E} :
    x (convexHull R) s ∃ (w : ER), (∀ ys, 0 w y) ys, w y = 1 s.centerMass w id = x
    theorem Finset.mem_convexHull' {R : Type u_1} {E : Type u_3} [LinearOrderedField R] [AddCommGroup E] [Module R E] {s : Finset E} {x : E} :
    x (convexHull R) s ∃ (w : ER), (∀ ys, 0 w y) ys, w y = 1 ys, 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} [LinearOrderedField R] [AddCommGroup E] [Module R E] {s : Set E} (hs : s.Finite) :
    (convexHull R) s = {x : E | ∃ (w : ER), (∀ ys, 0 w y) yhs.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} [LinearOrderedField R] [AddCommGroup E] [Module R E] (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} [LinearOrderedField R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] {s : Set E} {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} [LinearOrderedField R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] (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} [LinearOrderedField R] [AddCommGroup E] [Module R E] (s : Set E) (t : Set E) :
    (convexHull R) (s + t) = (convexHull R) s + (convexHull R) t
    @[simp]
    theorem convexHullAddMonoidHom_apply (R : Type u_1) (E : Type u_3) [LinearOrderedField R] [AddCommGroup E] [Module R E] (a : Set E) :
    def convexHullAddMonoidHom (R : Type u_1) (E : Type u_3) [LinearOrderedField R] [AddCommGroup E] [Module R E] :

    convexHull is an additive monoid morphism under pointwise addition.

    Equations
    Instances For
      theorem convexHull_sub {R : Type u_1} {E : Type u_3} [LinearOrderedField R] [AddCommGroup E] [Module R E] (s : Set E) (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} [LinearOrderedField R] [AddCommGroup E] [Module R E] (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} [LinearOrderedField R] [AddCommGroup E] [Module R E] (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} [LinearOrderedField R] [AddCommGroup E] [Module R E] {ι : Type u_8} (s : Finset ι) (t : ιSet E) :
      (convexHull R) (∑ is, t i) = is, (convexHull R) (t i)

      stdSimplex #

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

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

      theorem Set.Finite.convexHull_eq_image {R : Type u_1} {E : Type u_3} [LinearOrderedField R] [AddCommGroup E] [Module R E] {s : Set E} (hs : s.Finite) :
      (convexHull R) s = (∑ x : s, (LinearMap.proj x).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 ∈ 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} [LinearOrderedField R] [Fintype ι] {f : ιR} (hf : f stdSimplex R ι) (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} [LinearOrderedField R] [AddCommGroup E] [Module R E] {ι : 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} [LinearOrderedField R] [AddCommGroup E] [Module R E] {s : Finset E} {t₁ : Finset E} {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} [LinearOrderedField R] [AddCommGroup E] [Module R E] {t₁ : Finset E} {t₂ : Finset 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 ι] [LinearOrderedField 𝕜] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] {s : Set ι} {t : (i : ι) → Set (E i)} {x : (i : ι) → E i} (h : is, 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 ι] [LinearOrderedField 𝕜] [(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)