Mathlib.Analysis.Convex.Combination

Finset.centerMass definition

(t : Finset ι) (w : ι → R) (z : ι → E) : E

Full source

/-- Center of mass of a finite collection of points with prescribed weights.
Note that we require neither `0 ≤ w i` nor `∑ w = 1`. -/
def Finset.centerMass (t : Finset ι) (w : ι → R) (z : ι → E) : E :=
  (∑ i ∈ t, w i)⁻¹ • ∑ i ∈ t, w i • z i

Center of mass of a finite set of points

Informal description

Given a finite set of indices $t$, a weight function $w : \iota \to R$, and a function $z : \iota \to E$ assigning a point in a vector space $E$ to each index, the center of mass is defined as the weighted average: \[ \left(\sum_{i \in t} w_i\right)^{-1} \cdot \sum_{i \in t} w_i z_i \] Note that neither non-negativity of weights nor the condition $\sum w_i = 1$ is required in this definition.

Finset.centerMass_empty theorem

: (∅ : Finset ι).centerMass w z = 0

Full source

theorem Finset.centerMass_empty : (∅ : Finset ι).centerMass w z = 0 := by
  simp only [centerMass, sum_empty, smul_zero]

Center of Mass of Empty Set is Zero

Informal description

The center of mass of an empty finite set of points is the zero vector, i.e., for any weight function $w$ and any point assignment function $z$, we have $\text{centerMass}(\emptyset, w, z) = 0$.

Finset.centerMass_pair theorem

 [DecidableEq ι] (hne : i ≠ j) :
  ({ i, j } : Finset ι).centerMass w z = (w i / (w i + w j)) • z i + (w j / (w i + w j)) • z j

Full source

theorem Finset.centerMass_pair [DecidableEq ι] (hne : i ≠ j) :
    ({i, j} : Finset ι).centerMass w z = (w i / (w i + w j)) • z i + (w j / (w i + w j)) • z j := by
  simp only [centerMass, sum_pair hne]
  module

Center of Mass Formula for Two Distinct Points

Informal description

Let $i$ and $j$ be distinct indices in a type $\iota$ with decidable equality, and let $w : \iota \to R$ be a weight function and $z : \iota \to E$ be a function assigning points in a vector space $E$. The center of mass of the two-point set $\{i, j\}$ is given by: \[ \text{centerMass}(\{i, j\}, w, z) = \left(\frac{w_i}{w_i + w_j}\right) \cdot z_i + \left(\frac{w_j}{w_i + w_j}\right) \cdot z_j. \]

Finset.centerMass_insert theorem

 [DecidableEq ι] (ha : i ∉ t) (hw : ∑ j ∈ t, w j ≠ 0) :
  (insert i t).centerMass w z =
    (w i / (w i + ∑ j ∈ t, w j)) • z i + ((∑ j ∈ t, w j) / (w i + ∑ j ∈ t, w j)) • t.centerMass w z

Full source

theorem Finset.centerMass_insert [DecidableEq ι] (ha : i ∉ t) (hw : ∑ j ∈ t, w j∑ j ∈ t, w j ≠ 0) :
    (insert i t).centerMass w z =
      (w i / (w i + ∑ j ∈ t, w j)) • z i +
        ((∑ j ∈ t, w j) / (w i + ∑ j ∈ t, w j)) • t.centerMass w z := by
  simp only [centerMass, sum_insert ha, smul_add, (mul_smul _ _ _).symm, ← div_eq_inv_mul]
  congr 2
  rw [div_mul_eq_mul_div, mul_inv_cancel₀ hw, one_div]

Insertion Formula for Center of Mass in Finite Sets

Informal description

Let $t$ be a finite set of indices, $w : \iota \to R$ a weight function, and $z : \iota \to E$ a function assigning points in a vector space $E$. For an index $i \notin t$ and assuming $\sum_{j \in t} w_j \neq 0$, the center of mass of the set $\text{insert}(i, t)$ is given by: \[ \text{centerMass}(\text{insert}(i, t), w, z) = \left(\frac{w_i}{w_i + \sum_{j \in t} w_j}\right) \cdot z_i + \left(\frac{\sum_{j \in t} w_j}{w_i + \sum_{j \in t} w_j}\right) \cdot \text{centerMass}(t, w, z). \]

Finset.centerMass_singleton theorem

(hw : w i ≠ 0) : ({ i } : Finset ι).centerMass w z = z i

Full source

theorem Finset.centerMass_singleton (hw : w i ≠ 0) : ({i} : Finset ι).centerMass w z = z i := by
  rw [centerMass, sum_singleton, sum_singleton]
  match_scalars
  field_simp

Center of Mass of Singleton Set Equals Its Point

Informal description

For any weight function $w : \iota \to R$ and function $z : \iota \to E$ assigning points in a vector space $E$, if the weight $w_i$ at index $i$ is nonzero, then the center of mass of the singleton set $\{i\}$ is equal to $z_i$, i.e., \[ \text{centerMass}(\{i\}, w, z) = z_i. \]

Finset.centerMass_neg_left theorem

: t.centerMass (-w) z = t.centerMass w z

Full source

@[simp] lemma Finset.centerMass_neg_left : t.centerMass (-w) z = t.centerMass w z := by
  simp [centerMass, inv_neg]

Negation Invariance of Center of Mass

Informal description

For any finite set of indices $t$, weight function $w : \iota \to R$, and function $z : \iota \to E$ assigning points in a vector space $E$, the center of mass computed with weights $-w$ equals the center of mass computed with weights $w$, i.e., \[ \text{centerMass}_t(-w, z) = \text{centerMass}_t(w, z). \]

Finset.centerMass_smul_left theorem

 {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

Full source

lemma Finset.centerMass_smul_left {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 := by
  simp [centerMass, -smul_assoc, smul_assoc c, ← smul_sum, smul_inv₀, smul_smul_smul_comm, hc]

Scalar Multiplication Invariance of Center of Mass

Informal description

Let $R'$ be a scalar ring acting on $R$ and $E$ such that the scalar actions commute appropriately. For any nonzero scalar $c \in R'$, finite set of indices $t$, weight function $w : \iota \to R$, and function $z : \iota \to E$ assigning points in a vector space $E$, the center of mass computed with scaled weights $c \cdot w$ equals the center of mass computed with original weights: \[ \text{centerMass}_t(c \cdot w, z) = \text{centerMass}_t(w, z). \]

Finset.centerMass_eq_of_sum_1 theorem

(hw : ∑ i ∈ t, w i = 1) : t.centerMass w z = ∑ i ∈ t, w i • z i

Full source

theorem Finset.centerMass_eq_of_sum_1 (hw : ∑ i ∈ t, w i = 1) :
    t.centerMass w z = ∑ i ∈ t, w i • z i := by
  simp only [Finset.centerMass, hw, inv_one, one_smul]

Center of Mass Equals Weighted Sum When Weights Sum to One

Informal description

For a finite set of indices $t$, a weight function $w : \iota \to R$, and a function $z : \iota \to E$ assigning points in a vector space $E$, if the sum of the weights $\sum_{i \in t} w_i = 1$, then the center of mass equals the weighted sum: \[ \text{centerMass}_t(w, z) = \sum_{i \in t} w_i z_i. \]

Finset.centerMass_smul theorem

: (t.centerMass w fun i => c • z i) = c • t.centerMass w z

Full source

theorem Finset.centerMass_smul : (t.centerMass w fun i => c • z i) = c • t.centerMass w z := by
  simp only [Finset.centerMass, Finset.smul_sum, (mul_smul _ _ _).symm, mul_comm c, mul_assoc]

Scaling Commutes with Center of Mass: $\text{centerMass}_t(w, c \cdot z) = c \cdot \text{centerMass}_t(w, z)$

Informal description

For a finite set of indices $t$, a weight function $w : \iota \to R$, and a function $z : \iota \to E$ assigning points in a vector space $E$, the center of mass of the scaled points $c \cdot z_i$ equals the scaling of the center of mass: \[ \text{centerMass}_t(w, c \cdot z) = c \cdot \text{centerMass}_t(w, z). \]

Finset.centerMass_segment' theorem

 (s : Finset ι) (t : Finset ι') (ws : ι → R) (zs : ι → E) (wt : ι' → R) (zt : ι' → E) (hws : ∑ i ∈ s, ws i = 1)
  (hwt : ∑ i ∈ t, wt i = 1) (a 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)

Full source

/-- 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' (s : Finset ι) (t : Finset ι') (ws : ι → R) (zs : ι → E)
    (wt : ι' → R) (zt : ι' → E) (hws : ∑ i ∈ s, ws i = 1) (hwt : ∑ i ∈ t, wt i = 1) (a 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) := by
  rw [s.centerMass_eq_of_sum_1 _ hws, t.centerMass_eq_of_sum_1 _ hwt, smul_sum, smul_sum, ←
    Finset.sum_sumElim, Finset.centerMass_eq_of_sum_1]
  · congr with ⟨⟩ <;> simp only [Sum.elim_inl, Sum.elim_inr, mul_smul]
  · rw [sum_sumElim, ← mul_sum, ← mul_sum, hws, hwt, mul_one, mul_one, hab]

Convex Combination of Centers of Mass for Disjoint Index Sets

Informal description

Let $s$ and $t$ be finite sets of indices (possibly of different types), with weight functions $w_s : \iota \to R$ and $w_t : \iota' \to R$, and point assignments $z_s : \iota \to E$ and $z_t : \iota' \to E$ into a vector space $E$. Suppose the weights sum to one on each set, i.e., $\sum_{i \in s} w_s(i) = 1$ and $\sum_{j \in t} w_t(j) = 1$. Then for any scalars $a, b \in R$ with $a + b = 1$, the convex combination of the centers of mass equals the center of mass of the combined sets with adjusted weights: \[ a \cdot \text{centerMass}_s(w_s, z_s) + b \cdot \text{centerMass}_t(w_t, z_t) = \text{centerMass}_{s \sqcup t}\left(\lambda k. \begin{cases} a w_s(k) & \text{if } k \in s \\ b w_t(k) & \text{if } k \in t \end{cases}, \lambda k. \begin{cases} z_s(k) & \text{if } k \in s \\ z_t(k) & \text{if } k \in t \end{cases}\right) \] where $s \sqcup t$ denotes the disjoint union of the sets.

Finset.centerMass_segment theorem

 (s : Finset ι) (w₁ w₂ : ι → R) (z : ι → E) (hw₁ : ∑ i ∈ s, w₁ i = 1) (hw₂ : ∑ i ∈ s, w₂ i = 1) (a 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

Full source

/-- 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_segment (s : Finset ι) (w₁ w₂ : ι → R) (z : ι → E)
    (hw₁ : ∑ i ∈ s, w₁ i = 1) (hw₂ : ∑ i ∈ s, w₂ i = 1) (a 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 := by
  have hw : (∑ i ∈ s, (a * w₁ i + b * w₂ i)) = 1 := by
    simp only [← mul_sum, sum_add_distrib, mul_one, *]
  simp only [Finset.centerMass_eq_of_sum_1, Finset.centerMass_eq_of_sum_1 _ _ hw,
    smul_sum, sum_add_distrib, add_smul, mul_smul, *]

Convex Combination of Centers of Mass with Shared Points

Informal description

Let $s$ be a finite set of indices, $w_1, w_2 : \iota \to R$ be weight functions, and $z : \iota \to E$ be a point assignment in a vector space $E$. Suppose the weights sum to one, i.e., $\sum_{i \in s} w_1(i) = 1$ and $\sum_{i \in s} w_2(i) = 1$. Then for any scalars $a, b \in R$ with $a + b = 1$, the convex combination of the centers of mass equals the center of mass with the combined weights: \[ a \cdot \text{centerMass}_s(w_1, z) + b \cdot \text{centerMass}_s(w_2, z) = \text{centerMass}_s(\lambda i. a w_1(i) + b w_2(i), z). \]

Finset.centerMass_ite_eq theorem

[DecidableEq ι] (hi : i ∈ t) : t.centerMass (fun j => if i = j then (1 : R) else 0) z = z i

Full source

theorem Finset.centerMass_ite_eq [DecidableEq ι] (hi : i ∈ t) :
    t.centerMass (fun j => if i = j then (1 : R) else 0) z = z i := by
  rw [Finset.centerMass_eq_of_sum_1]
  · trans ∑ j ∈ t, if i = j then z i else 0
    · congr with i
      split_ifs with h
      exacts [h ▸ one_smul _ _, zero_smul _ _]
    · rw [sum_ite_eq, if_pos hi]
  · rw [sum_ite_eq, if_pos hi]

Center of Mass with Dirac Delta Weights Equals Point Value

Informal description

For a finite set of indices $t$ and a point assignment $z : \iota \to E$ in a vector space $E$, if the weight function is defined as $w(j) = 1$ when $j = i$ and $w(j) = 0$ otherwise for some $i \in t$, then the center of mass equals $z(i)$, i.e., \[ \text{centerMass}_t(w, z) = z(i). \]

Finset.centerMass_subset theorem

{t' : Finset ι} (ht : t ⊆ t') (h : ∀ i ∈ t', i ∉ t → w i = 0) : t.centerMass w z = t'.centerMass w z

Full source

theorem Finset.centerMass_subset {t' : Finset ι} (ht : t ⊆ t') (h : ∀ i ∈ t', i ∉ t → w i = 0) :
    t.centerMass w z = t'.centerMass w z := by
  rw [centerMass, sum_subset ht h, smul_sum, centerMass, smul_sum]
  apply sum_subset ht
  intro i hit' hit
  rw [h i hit' hit, zero_smul, smul_zero]

Invariance of Center of Mass under Zero-Weight Extension

Informal description

Let $t$ and $t'$ be finite sets of indices with $t \subseteq t'$, and let $w : \iota \to R$ and $z : \iota \to E$ be weight and point functions respectively. If for every $i \in t'$ not in $t$ we have $w(i) = 0$, then the center of mass of $t$ with weights $w$ and points $z$ is equal to the center of mass of $t'$ with the same weights and points.

Finset.centerMass_filter_ne_zero theorem

[∀ i, Decidable (w i ≠ 0)] : {i ∈ t | w i ≠ 0}.centerMass w z = t.centerMass w z

Full source

theorem Finset.centerMass_filter_ne_zero [∀ i, Decidable (w i ≠ 0)] :
    {i ∈ t | w i ≠ 0}.centerMass w z = t.centerMass w z :=
  Finset.centerMass_subset z (filter_subset _ _) fun i hit hit' => by
    simpa only [hit, mem_filter, true_and, Ne, Classical.not_not] using hit'

Equality of Center of Mass with and without Zero Weights

Informal description

For a finite set of indices $t$, a weight function $w : \iota \to R$, and a point assignment $z : \iota \to E$ in a vector space $E$, the center of mass computed over the subset $\{i \in t \mid w_i \neq 0\}$ is equal to the center of mass computed over the entire set $t$.

Finset.centerMass_le_sup theorem

 {s : Finset ι} {f : ι → α} {w : ι → R} (hw₀ : ∀ i ∈ s, 0 ≤ w i) (hw₁ : 0 < ∑ i ∈ s, w i) :
  s.centerMass w f ≤ s.sup' (nonempty_of_ne_empty <| by rintro rfl; simp at hw₁) f

Full source

theorem centerMass_le_sup {s : Finset ι} {f : ι → α} {w : ι → R} (hw₀ : ∀ i ∈ s, 0 ≤ w i)
    (hw₁ : 0 < ∑ i ∈ s, w i) :
    s.centerMass w f ≤ s.sup' (nonempty_of_ne_empty <| by rintro rfl; simp at hw₁) f := by
  rw [centerMass, inv_smul_le_iff_of_pos hw₁, sum_smul]
  exact sum_le_sum fun i hi => smul_le_smul_of_nonneg_left (le_sup' _ hi) <| hw₀ i hi

Center of Mass is Bounded by Supremum under Non-Negative Weights

Informal description

Let $s$ be a finite set of indices, $f : \iota \to \alpha$ a function assigning values in a linearly ordered type $\alpha$, and $w : \iota \to R$ a weight function with non-negative weights (i.e., $w_i \geq 0$ for all $i \in s$) and positive total weight (i.e., $\sum_{i \in s} w_i > 0$). Then the center of mass of $f$ with respect to $w$ is less than or equal to the supremum of $f$ over $s$: \[ \left(\sum_{i \in s} w_i\right)^{-1} \sum_{i \in s} w_i f_i \leq \sup_{i \in s} f_i. \]

Finset.inf_le_centerMass theorem

 {s : Finset ι} {f : ι → α} {w : ι → R} (hw₀ : ∀ i ∈ s, 0 ≤ w i) (hw₁ : 0 < ∑ i ∈ s, w i) :
  s.inf' (nonempty_of_ne_empty <| by rintro rfl; simp at hw₁) f ≤ s.centerMass w f

Full source

theorem inf_le_centerMass {s : Finset ι} {f : ι → α} {w : ι → R} (hw₀ : ∀ i ∈ s, 0 ≤ w i)
    (hw₁ : 0 < ∑ i ∈ s, w i) :
    s.inf' (nonempty_of_ne_empty <| by rintro rfl; simp at hw₁) f ≤ s.centerMass w f :=
  centerMass_le_sup (α := αᵒᵈ) hw₀ hw₁

Infimum is Bounded by Center of Mass under Non-Negative Weights

Informal description

Let $s$ be a finite set of indices, $f : \iota \to \alpha$ a function assigning values in a linearly ordered type $\alpha$, and $w : \iota \to R$ a weight function with non-negative weights (i.e., $w_i \geq 0$ for all $i \in s$) and positive total weight (i.e., $\sum_{i \in s} w_i > 0$). Then the infimum of $f$ over $s$ is less than or equal to the center of mass of $f$ with respect to $w$: \[ \inf_{i \in s} f_i \leq \left(\sum_{i \in s} w_i\right)^{-1} \sum_{i \in s} w_i f_i. \]

Finset.centerMass_of_sum_add_sum_eq_zero theorem

 {s t : Finset ι} (hw : ∑ i ∈ s, w i + ∑ i ∈ t, w i = 0) (hz : ∑ i ∈ s, w i • z i + ∑ i ∈ t, w i • z i = 0) :
  s.centerMass w z = t.centerMass w z

Full source

lemma Finset.centerMass_of_sum_add_sum_eq_zero {s t : Finset ι}
    (hw : ∑ i ∈ s, w i + ∑ i ∈ t, w i = 0) (hz : ∑ i ∈ s, w i • z i + ∑ i ∈ t, w i • z i = 0) :
    s.centerMass w z = t.centerMass w z := by
  simp [centerMass, eq_neg_of_add_eq_zero_right hw, eq_neg_of_add_eq_zero_left hz, ← neg_inv]

Equality of Centers of Mass under Zero Total Weight and Zero Total Moment Condition

Informal description

Let $s$ and $t$ be finite sets of indices, $w : \iota \to R$ a weight function, and $z : \iota \to E$ a function assigning points in a vector space $E$ to each index. If the sum of weights over $s$ and $t$ is zero (i.e., $\sum_{i \in s} w_i + \sum_{i \in t} w_i = 0$) and the weighted sum of points over $s$ and $t$ is zero (i.e., $\sum_{i \in s} w_i z_i + \sum_{i \in t} w_i z_i = 0$), then the centers of mass of $s$ and $t$ with respect to $w$ and $z$ are equal: \[ \text{centerMass}_s(w, z) = \text{centerMass}_t(w, z). \]

Convex.centerMass_mem theorem

 (hs : Convex R s) : (∀ i ∈ t, 0 ≤ w i) → (0 < ∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s

Full source

/-- 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.centerMass_mem (hs : Convex R s) :
    (∀ i ∈ t, 0 ≤ w i) → (0 < ∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s := by
  classical
  induction' t using Finset.induction with i t hi ht
  · simp [lt_irrefl]
  intro h₀ hpos hmem
  have zi : z i ∈ s := hmem _ (mem_insert_self _ _)
  have hs₀ : ∀ j ∈ t, 0 ≤ w j := fun j hj => h₀ j <| mem_insert_of_mem hj
  rw [sum_insert hi] at hpos
  by_cases hsum_t : ∑ j ∈ t, w j = 0
  · have ws : ∀ j ∈ t, w j = 0 := (sum_eq_zero_iff_of_nonneg hs₀).1 hsum_t
    have wz : ∑ j ∈ t, w j • z j = 0 := sum_eq_zero fun i hi => by simp [ws i hi]
    simp only [centerMass, sum_insert hi, wz, hsum_t, add_zero]
    simp only [hsum_t, add_zero] at hpos
    rw [← mul_smul, inv_mul_cancel₀ (ne_of_gt hpos), one_smul]
    exact zi
  · rw [Finset.centerMass_insert _ _ _ hi hsum_t]
    refine convex_iff_div.1 hs zi (ht hs₀ ?_ ?_) ?_ (sum_nonneg hs₀) hpos
    · exact lt_of_le_of_ne (sum_nonneg hs₀) (Ne.symm hsum_t)
    · intro j hj
      exact hmem j (mem_insert_of_mem hj)
    · exact h₀ _ (mem_insert_self _ _)

Center of Mass of Points in a Convex Set Belongs to the Set Under Non-Negative Weights and Positive Total Weight

Informal description

Let $s$ be a convex set in a vector space over an ordered scalar field $\mathbb{R}$. For any finite set of indices $t$, weight function $w : \iota \to \mathbb{R}$, and function $z : \iota \to E$ assigning points in $E$ to each index, if all weights are non-negative (i.e., $w_i \geq 0$ for all $i \in t$), the total weight is positive (i.e., $\sum_{i \in t} w_i > 0$), and all points $z_i$ lie in $s$ (i.e., $z_i \in s$ for all $i \in t$), then the center of mass of the points with respect to the weights lies in $s$.

Convex.sum_mem theorem

 (hs : Convex R s) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i ∈ t, w i = 1) (hz : ∀ i ∈ t, z i ∈ s) : (∑ i ∈ t, w i • z i) ∈ s

Full source

theorem Convex.sum_mem (hs : Convex R s) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i ∈ t, w i = 1)
    (hz : ∀ i ∈ t, z i ∈ s) : (∑ i ∈ t, w i • z i) ∈ s := by
  simpa only [h₁, centerMass, inv_one, one_smul] using
    hs.centerMass_mem h₀ (h₁.symm ▸ zero_lt_one) hz

Convex Combination of Points in a Convex Set Belongs to the Set

Informal description

Let $s$ be a convex set in a vector space over an ordered scalar field $\mathbb{R}$. For any finite set of indices $t$, weight function $w : \iota \to \mathbb{R}$, and function $z : \iota \to E$ assigning points in $E$ to each index, if all weights are non-negative (i.e., $w_i \geq 0$ for all $i \in t$), the weights sum to 1 (i.e., $\sum_{i \in t} w_i = 1$), and all points $z_i$ lie in $s$ (i.e., $z_i \in s$ for all $i \in t$), then the convex combination $\sum_{i \in t} w_i z_i$ lies in $s$.

Convex.finsum_mem theorem

 {ι : Sort*} {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 ≠ 0 → z i ∈ s) : (∑ᶠ i, w i • z i) ∈ s

Full source

/-- A version of `Convex.sum_mem` for `finsum`s. 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.finsum_mem {ι : Sort*} {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 ≠ 0 → z i ∈ s) :
    (∑ᶠ i, w i • z i) ∈ s := by
  have hfin_w : (support (w ∘ PLift.down)).Finite := by
    by_contra H
    rw [finsum, dif_neg H] at h₁
    exact zero_ne_one h₁
  have hsub : supportsupport ((fun i => w i • z i) ∘ PLift.down) ⊆ hfin_w.toFinset :=
    (support_smul_subset_left _ _).trans hfin_w.coe_toFinset.ge
  rw [finsum_eq_sum_plift_of_support_subset hsub]
  refine hs.sum_mem (fun _ _ => h₀ _) ?_ fun i hi => hz _ ?_
  · rwa [finsum, dif_pos hfin_w] at h₁
  · rwa [hfin_w.mem_toFinset] at hi

Infinite Convex Combination of Points in a Convex Set Belongs to the Set

Informal description

Let $s$ be a convex set in a vector space over an ordered scalar field $\mathbb{R}$. Given a family of nonnegative weights $w : \iota \to \mathbb{R}$ with $\sum_{i} w_i = 1$ and a family of points $z : \iota \to E$ such that $z_i \in s$ whenever $w_i \neq 0$, the infinite convex combination $\sum_{i} w_i z_i$ belongs to $s$.

convex_iff_sum_mem theorem

 :
  Convex R s ↔
    ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → (∑ x ∈ t, w x • x) ∈ s

Full source

theorem convex_iff_sum_mem : ConvexConvex R s ↔ ∀ (t : Finset E) (w : E → R),
    (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → (∑ x ∈ t, w x • x) ∈ s := by
  classical
  refine ⟨fun hs t w hw₀ hw₁ hts => hs.sum_mem hw₀ hw₁ hts, ?_⟩
  intro h x hx y hy a b ha hb hab
  by_cases h_cases : x = y
  · rw [h_cases, ← add_smul, hab, one_smul]
    exact hy
  · convert h {x, y} (fun z => if z = y then b else a) _ _ _
    · simp only [sum_pair h_cases, if_neg h_cases, if_pos trivial]
    · intro i _
      simp only
      split_ifs <;> assumption
    · simp only [sum_pair h_cases, if_neg h_cases, if_pos trivial, hab]
    · intro i hi
      simp only [Finset.mem_singleton, Finset.mem_insert] at hi
      cases hi <;> subst i <;> assumption

Characterization of Convex Sets via Finite Convex Combinations

Informal description

A set $s$ in a vector space over an ordered scalar field $\mathbb{R}$ is convex if and only if for every finite subset $t \subseteq E$ and weight function $w : E \to \mathbb{R}$ such that all weights are non-negative ($w_i \geq 0$ for all $i \in t$), the weights sum to 1 ($\sum_{i \in t} w_i = 1$), and all points in $t$ belong to $s$ ($x \in s$ for all $x \in t$), the convex combination $\sum_{x \in t} w_x \cdot x$ belongs to $s$.

Finset.centerMass_mem_convexHull theorem

 (t : Finset ι) {w : ι → R} (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hws : 0 < ∑ i ∈ t, w i) {z : ι → E} (hz : ∀ i ∈ t, z i ∈ s) :
  t.centerMass w z ∈ convexHull R s

Full source

theorem Finset.centerMass_mem_convexHull (t : Finset ι) {w : ι → R} (hw₀ : ∀ i ∈ t, 0 ≤ w i)
    (hws : 0 < ∑ i ∈ t, w i) {z : ι → E} (hz : ∀ i ∈ t, z i ∈ s) :
    t.centerMass w z ∈ convexHull R s :=
  (convex_convexHull R s).centerMass_mem hw₀ hws fun i hi => subset_convexHull R s <| hz i hi

Center of Mass of Points in a Set Lies in its Convex Hull Under Non-Negative Weights and Positive Total Weight

Informal description

Let $t$ be a finite set of indices, $w \colon \iota \to \mathbb{R}$ a weight function, and $z \colon \iota \to E$ a function assigning points in a vector space $E$ to each index. If all weights are non-negative (i.e., $w_i \geq 0$ for all $i \in t$), the total weight is positive (i.e., $\sum_{i \in t} w_i > 0$), and all points $z_i$ lie in a set $s$ (i.e., $z_i \in s$ for all $i \in t$), then the center of mass of the points with respect to the weights lies in the convex hull of $s$ over the scalar ring $R$.

Finset.centerMass_mem_convexHull_of_nonpos theorem

 (t : Finset ι) (hw₀ : ∀ i ∈ t, w i ≤ 0) (hws : ∑ i ∈ t, w i < 0) (hz : ∀ i ∈ t, z i ∈ s) :
  t.centerMass w z ∈ convexHull R s

Full source

/-- A version of `Finset.centerMass_mem_convexHull` for when the weights are nonpositive. -/
lemma Finset.centerMass_mem_convexHull_of_nonpos (t : Finset ι) (hw₀ : ∀ i ∈ t, w i ≤ 0)
    (hws : ∑ i ∈ t, w i < 0) (hz : ∀ i ∈ t, z i ∈ s) : t.centerMass w z ∈ convexHull R s := by
  rw [← centerMass_neg_left]
  exact Finset.centerMass_mem_convexHull _ (fun _i hi ↦ neg_nonneg.2 <| hw₀ _ hi) (by simpa) hz

Center of Mass of Points in a Set Lies in its Convex Hull Under Non-Positive Weights and Negative Total Weight

Informal description

Let $t$ be a finite set of indices, $w \colon \iota \to \mathbb{R}$ a weight function, and $z \colon \iota \to E$ a function assigning points in a vector space $E$ to each index. If all weights are non-positive (i.e., $w_i \leq 0$ for all $i \in t$), the total weight is negative (i.e., $\sum_{i \in t} w_i < 0$), and all points $z_i$ lie in a set $s$ (i.e., $z_i \in s$ for all $i \in t$), then the center of mass of the points with respect to the weights lies in the convex hull of $s$ over the scalar ring $R$.

Finset.centerMass_id_mem_convexHull theorem

 (t : Finset E) {w : E → R} (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hws : 0 < ∑ i ∈ t, w i) :
  t.centerMass w id ∈ convexHull R (t : Set E)

Full source

/-- A refinement of `Finset.centerMass_mem_convexHull` when the indexed family is a `Finset` of
the space. -/
theorem Finset.centerMass_id_mem_convexHull (t : Finset E) {w : E → R} (hw₀ : ∀ i ∈ t, 0 ≤ w i)
    (hws : 0 < ∑ i ∈ t, w i) : t.centerMass w id ∈ convexHull R (t : Set E) :=
  t.centerMass_mem_convexHull hw₀ hws fun _ => mem_coe.2

Center of Mass of Points Lies in Their Convex Hull Under Non-Negative Weights and Positive Total Weight

Informal description

For any finite set $t$ of points in a vector space $E$ and any weight function $w \colon E \to \mathbb{R}$ such that all weights are non-negative (i.e., $w_i \geq 0$ for all $i \in t$) and the total weight is positive (i.e., $\sum_{i \in t} w_i > 0$), the center of mass of the points with respect to the weights lies in the convex hull of $t$ over the scalar ring $R$.

Finset.centerMass_id_mem_convexHull_of_nonpos theorem

 (t : Finset E) {w : E → R} (hw₀ : ∀ i ∈ t, w i ≤ 0) (hws : ∑ i ∈ t, w i < 0) :
  t.centerMass w id ∈ convexHull R (t : Set E)

Full source

/-- A version of `Finset.centerMass_mem_convexHull` for when the weights are nonpositive. -/
lemma Finset.centerMass_id_mem_convexHull_of_nonpos (t : Finset E) {w : E → R}
    (hw₀ : ∀ i ∈ t, w i ≤ 0) (hws : ∑ i ∈ t, w i < 0) :
    t.centerMass w id ∈ convexHull R (t : Set E) :=
  t.centerMass_mem_convexHull_of_nonpos hw₀ hws fun _ ↦ mem_coe.2

Center of Mass of Points Lies in Their Convex Hull Under Non-Positive Weights and Negative Total Weight

Informal description

Let $t$ be a finite set of points in a vector space $E$ and let $w \colon E \to \mathbb{R}$ be a weight function such that all weights are non-positive (i.e., $w_i \leq 0$ for all $i \in t$) and the total weight is negative (i.e., $\sum_{i \in t} w_i < 0$). Then the center of mass of the points with respect to the weights lies in the convex hull of $t$ over the scalar ring $R$.

affineCombination_eq_centerMass theorem

 {ι : Type*} {t : Finset ι} {p : ι → E} {w : ι → R} (hw₂ : ∑ i ∈ t, w i = 1) :
  t.affineCombination R p w = centerMass t w p

Full source

theorem affineCombination_eq_centerMass {ι : Type*} {t : Finset ι} {p : ι → E} {w : ι → R}
    (hw₂ : ∑ i ∈ t, w i = 1) : t.affineCombination R p w = centerMass t w p := by
  rw [affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ w _ hw₂ (0 : E),
    Finset.weightedVSubOfPoint_apply, vadd_eq_add, add_zero, t.centerMass_eq_of_sum_1 _ hw₂]
  simp_rw [vsub_eq_sub, sub_zero]

Affine Combination Equals Center of Mass When Weights Sum to One

Informal description

For a finite set of indices $t$, a family of points $p : \iota \to E$ in a vector space $E$, and a weight function $w : \iota \to R$ such that $\sum_{i \in t} w_i = 1$, the affine combination of the points equals their center of mass: \[ \text{affineCombination}_t(p, w) = \text{centerMass}_t(w, p). \]

affineCombination_mem_convexHull theorem

 {s : Finset ι} {v : ι → E} {w : ι → R} (hw₀ : ∀ i ∈ s, 0 ≤ w i) (hw₁ : s.sum w = 1) :
  s.affineCombination R v w ∈ convexHull R (range v)

Full source

theorem affineCombination_mem_convexHull {s : Finset ι} {v : ι → E} {w : ι → R}
    (hw₀ : ∀ i ∈ s, 0 ≤ w i) (hw₁ : s.sum w = 1) :
    s.affineCombination R v w ∈ convexHull R (range v) := by
  rw [affineCombination_eq_centerMass hw₁]
  apply s.centerMass_mem_convexHull hw₀
  · simp [hw₁]
  · simp

Affine Combination of Points with Non-Negative Weights Summing to One Lies in Convex Hull

Informal description

For a finite set of indices $s$, a family of points $v : \iota \to E$ in a vector space $E$, and a weight function $w : \iota \to \mathbb{R}$ such that all weights are non-negative (i.e., $w_i \geq 0$ for all $i \in s$) and the weights sum to 1 (i.e., $\sum_{i \in s} w_i = 1$), the affine combination of the points lies in the convex hull of the range of $v$.

Finset.centroid_eq_centerMass theorem

(s : Finset ι) (hs : s.Nonempty) (p : ι → E) : s.centroid R p = s.centerMass (s.centroidWeights R) p

Full source

/-- The centroid can be regarded as a center of mass. -/
@[simp]
theorem Finset.centroid_eq_centerMass (s : Finset ι) (hs : s.Nonempty) (p : ι → E) :
    s.centroid R p = s.centerMass (s.centroidWeights R) p :=
  affineCombination_eq_centerMass (s.sum_centroidWeights_eq_one_of_nonempty R hs)

Centroid Equals Center of Mass with Centroid Weights

Informal description

For a nonempty finite set $s$ and a family of points $p : \iota \to E$ in a vector space $E$ over a ring $R$, the centroid of $s$ with respect to $p$ equals the center of mass of $s$ with the centroid weights: \[ \text{centroid}_s(p) = \text{centerMass}_s(\text{centroidWeights}_s, p). \]

Finset.centroid_mem_convexHull theorem

(s : Finset E) (hs : s.Nonempty) : s.centroid R id ∈ convexHull R (s : Set E)

Full source

theorem Finset.centroid_mem_convexHull (s : Finset E) (hs : s.Nonempty) :
    s.centroid R id ∈ convexHull R (s : Set E) := by
  rw [s.centroid_eq_centerMass hs]
  apply s.centerMass_id_mem_convexHull
  · simp only [inv_nonneg, imp_true_iff, Nat.cast_nonneg, Finset.centroidWeights_apply]
  · have hs_card : (#s : R) ≠ 0 := by simp [Finset.nonempty_iff_ne_empty.mp hs]
    simp only [hs_card, Finset.sum_const, nsmul_eq_mul, mul_inv_cancel₀, Ne, not_false_iff,
      Finset.centroidWeights_apply, zero_lt_one]

Centroid Lies in Convex Hull of Nonempty Finite Set

Informal description

For any nonempty finite set $s$ of points in a vector space $E$ over a scalar ring $R$, the centroid of $s$ lies in the convex hull of $s$.

convexHull_range_eq_exists_affineCombination theorem

 (v : ι → E) :
  convexHull R (range v) =
    {x | ∃ (s : Finset ι) (w : ι → R), (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ s.affineCombination R v w = x}

Full source

theorem convexHull_range_eq_exists_affineCombination (v : ι → E) : convexHull R (range v) =
    { x | ∃ (s : Finset ι) (w : ι → R), (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧
      s.affineCombination R v w = x } := by
  classical
  refine Subset.antisymm (convexHull_min ?_ ?_) ?_
  · intro x hx
    obtain ⟨i, hi⟩ := Set.mem_range.mp hx
    exact ⟨{i}, Function.const ι (1 : R), by simp, by simp, by simp [hi]⟩
  · rintro x ⟨s, w, hw₀, hw₁, rfl⟩ y ⟨s', w', hw₀', hw₁', rfl⟩ a b ha hb hab
    let W : ι → R := fun i => (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
    have hW₁ : (s ∪ s').sum W = 1 := by
      rw [sum_add_distrib, ← sum_subset subset_union_left,
        ← sum_subset subset_union_right, sum_ite_of_true,
        sum_ite_of_true, ← mul_sum, ← mul_sum, hw₁, hw₁', ← add_mul, hab,
        mul_one] <;> intros <;> simp_all
    refine ⟨s ∪ s', W, ?_, hW₁, ?_⟩
    · rintro i -
      by_cases hi : i ∈ s <;> by_cases hi' : i ∈ s' <;>
        simp [W, hi, hi', add_nonneg, mul_nonneg ha (hw₀ i _), mul_nonneg hb (hw₀' i _)]
    · simp_rw [W, affineCombination_eq_linear_combination (s ∪ s') v _ hW₁,
        affineCombination_eq_linear_combination s v w hw₁,
        affineCombination_eq_linear_combination s' v w' hw₁', add_smul, sum_add_distrib]
      rw [← sum_subset subset_union_left, ← sum_subset subset_union_right]
      · simp only [ite_smul, sum_ite_of_true fun _ hi => hi, mul_smul, ← smul_sum]
      · intro i _ hi'
        simp [hi']
      · intro i _ hi'
        simp [hi']
  · rintro x ⟨s, w, hw₀, hw₁, rfl⟩
    exact affineCombination_mem_convexHull hw₀ hw₁

Characterization of Convex Hull of Range via Affine Combinations

Informal description

For a vector space $E$ over a scalar ring $R$ and a function $v : \iota \to E$, the convex hull of the range of $v$ is equal to the set of all points $x \in E$ for which there exists a finite subset $s \subseteq \iota$ and a weight function $w : \iota \to R$ such that: 1. All weights are non-negative: $w_i \geq 0$ for all $i \in s$, 2. The weights sum to one: $\sum_{i \in s} w_i = 1$, 3. $x$ is the affine combination: $x = \sum_{i \in s} w_i v_i$.

convexHull_eq theorem

 (s : Set E) :
  convexHull R s =
    {x : E |
      ∃ (ι : Type) (t : Finset ι) (w : ι → R) (z : ι → E),
        (∀ i ∈ t, 0 ≤ w i) ∧ ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x}

Full source

/--
Convex hull of `s` is equal to the set of all centers of masses of `Finset`s `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 convexHull_eq (s : Set E) : convexHull R s =
    { x : E | ∃ (ι : Type) (t : Finset ι) (w : ι → R) (z : ι → E), (∀ i ∈ t, 0 ≤ w i) ∧
      ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x } := by
  refine Subset.antisymm (convexHull_min ?_ ?_) ?_
  · intro x hx
    use PUnit, {PUnit.unit}, fun _ => 1, fun _ => x, fun _ _ => zero_le_one, sum_singleton _ _,
      fun _ _ => hx
    simp only [Finset.centerMass, Finset.sum_singleton, inv_one, one_smul]
  · rintro x ⟨ι, sx, wx, zx, hwx₀, hwx₁, hzx, rfl⟩ y ⟨ι', sy, wy, zy, hwy₀, hwy₁, hzy, rfl⟩ a b ha
      hb hab
    rw [Finset.centerMass_segment' _ _ _ _ _ _ hwx₁ hwy₁ _ _ hab]
    refine ⟨_, _, _, _, ?_, ?_, ?_, rfl⟩
    · rintro i hi
      rw [Finset.mem_disjSum] at hi
      rcases hi with (⟨j, hj, rfl⟩ | ⟨j, hj, rfl⟩) <;> simp only [Sum.elim_inl, Sum.elim_inr] <;>
        apply_rules [mul_nonneg, hwx₀, hwy₀]
    · simp [Finset.sum_sumElim, ← mul_sum, *]
    · intro i hi
      rw [Finset.mem_disjSum] at hi
      rcases hi with (⟨j, hj, rfl⟩ | ⟨j, hj, rfl⟩) <;> apply_rules [hzx, hzy]
  · rintro _ ⟨ι, t, w, z, hw₀, hw₁, hz, rfl⟩
    exact t.centerMass_mem_convexHull hw₀ (hw₁.symm ▸ zero_lt_one) hz

Characterization of Convex Hull as Centers of Mass with Non-Negative Weights Summing to One

Informal description

For any subset $s$ of a vector space $E$ over a scalar ring $R$, the convex hull of $s$ is equal to the set of all points $x \in E$ for which there exists a finite index set $\iota$, a finite subset $t \subseteq \iota$, a weight function $w \colon \iota \to R$, and a function $z \colon \iota \to E$ such that: 1. All weights are non-negative: $w_i \geq 0$ for all $i \in t$, 2. The weights sum to one: $\sum_{i \in t} w_i = 1$, 3. All points lie in $s$: $z_i \in s$ for all $i \in t$, 4. $x$ is the center of mass: $x = \text{centerMass}_t(w, z)$.

mem_convexHull_of_exists_fintype theorem

 {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

Full source

/-- Universe polymorphic version of the reverse implication of `mem_convexHull_iff_exists_fintype`.
-/
lemma mem_convexHull_of_exists_fintype {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 := by
  rw [← hx, ← centerMass_eq_of_sum_1 _ _ hw₁]
  exact centerMass_mem_convexHull _ (by simpa using hw₀) (by simp [hw₁]) (by simpa using hz)

Convex Hull Membership via Finite Convex Combination

Informal description

Let $E$ be a vector space over a scalar ring $R$, and let $s \subseteq E$ be a subset. For any finite type $\iota$, non-negative weight function $w \colon \iota \to R$ with $\sum_i w_i = 1$, and points $z_i \in s$ for all $i \in \iota$, if $x = \sum_i w_i z_i$, then $x$ belongs to the convex hull of $s$ over $R$.

mem_convexHull_iff_exists_fintype theorem

 {s : Set E} {x : E} :
  x ∈ convexHull R s ↔
    ∃ (ι : Type) (_ : Fintype ι) (w : ι → R) (z : ι → E),
      (∀ i, 0 ≤ w i) ∧ ∑ i, w i = 1 ∧ (∀ i, z i ∈ s) ∧ ∑ i, w i • z i = x

Full source

/-- 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. -/
lemma mem_convexHull_iff_exists_fintype {s : Set E} {x : E} :
    x ∈ convexHull R sx ∈ convexHull R s ↔ ∃ (ι : Type) (_ : Fintype ι) (w : ι → R) (z : ι → E), (∀ i, 0 ≤ w i) ∧
      ∑ i, w i = 1 ∧ (∀ i, z i ∈ s) ∧ ∑ i, w i • z i = x := by
  constructor
  · simp only [convexHull_eq, mem_setOf_eq]
    rintro ⟨ι, t, w, z, h⟩
    refine ⟨t, inferInstance, w ∘ (↑), z ∘ (↑), ?_⟩
    simpa [← sum_attach t, centerMass_eq_of_sum_1 _ _ h.2.1] using h
  · rintro ⟨ι, _, w, z, hw₀, hw₁, hz, hx⟩
    exact mem_convexHull_of_exists_fintype w z hw₀ hw₁ hz hx

Characterization of Convex Hull Membership via Finite Convex Combinations

Informal description

For any subset $s$ of a vector space $E$ over a scalar ring $R$, a point $x \in E$ belongs to the convex hull of $s$ if and only if there exists a finite index type $\iota$, a non-negative weight function $w \colon \iota \to R$ with $\sum_i w_i = 1$, and points $z_i \in s$ for all $i \in \iota$ such that $x = \sum_i w_i z_i$.

Finset.convexHull_eq theorem

 (s : Finset E) : convexHull R ↑s = {x : E | ∃ w : E → R, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x}

Full source

theorem Finset.convexHull_eq (s : Finset E) : convexHull R ↑s =
    { x : E | ∃ w : E → R, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x } := by
  classical
  refine Set.Subset.antisymm (convexHull_min ?_ ?_) ?_
  · intro x hx
    rw [Finset.mem_coe] at hx
    refine ⟨_, ?_, ?_, Finset.centerMass_ite_eq _ _ _ hx⟩
    · intros
      split_ifs
      exacts [zero_le_one, le_refl 0]
    · rw [Finset.sum_ite_eq, if_pos hx]
  · rintro x ⟨wx, hwx₀, hwx₁, rfl⟩ y ⟨wy, hwy₀, hwy₁, rfl⟩ a b ha hb hab
    rw [Finset.centerMass_segment _ _ _ _ hwx₁ hwy₁ _ _ hab]
    refine ⟨_, ?_, ?_, rfl⟩
    · rintro i hi
      apply_rules [add_nonneg, mul_nonneg, hwx₀, hwy₀]
    · simp only [Finset.sum_add_distrib, ← mul_sum, mul_one, *]
  · rintro _ ⟨w, hw₀, hw₁, rfl⟩
    exact
      s.centerMass_mem_convexHull (fun x hx => hw₀ _ hx) (hw₁.symm ▸ zero_lt_one) fun x hx => hx

Characterization of Convex Hull via Center of Mass for Finite Sets

Informal description

For any finite set $s$ in a vector space $E$ over a scalar ring $R$, the convex hull of $s$ is equal to the set of all points $x \in E$ for which there exists a weight function $w \colon E \to R$ such that: 1. $w(y) \geq 0$ for all $y \in s$, 2. $\sum_{y \in s} w(y) = 1$, and 3. $x$ is the center of mass of $s$ with respect to $w$ and the identity function. In other words, the convex hull consists precisely of all convex combinations of points in $s$.

Finset.mem_convexHull theorem

 {s : Finset E} {x : E} :
  x ∈ convexHull R (s : Set E) ↔ ∃ w : E → R, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x

Full source

theorem Finset.mem_convexHull {s : Finset E} {x : E} : x ∈ convexHull R (s : Set E)x ∈ convexHull R (s : Set E) ↔
    ∃ w : E → R, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x := by
  rw [Finset.convexHull_eq, Set.mem_setOf_eq]

Characterization of Convex Hull Membership via Convex Combinations for Finite Sets

Informal description

For any finite set $s$ in a vector space $E$ over a scalar ring $R$, a point $x \in E$ belongs to the convex hull of $s$ if and only if there exists a weight function $w \colon E \to R$ such that: 1. $w(y) \geq 0$ for all $y \in s$, 2. $\sum_{y \in s} w(y) = 1$, and 3. $x$ is the center of mass of $s$ with respect to $w$ and the identity function. In other words, $x$ is in the convex hull of $s$ precisely when it can be expressed as a convex combination of points in $s$.

Finset.mem_convexHull' theorem

 {s : Finset E} {x : E} :
  x ∈ convexHull R (s : Set E) ↔ ∃ w : E → R, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ ∑ y ∈ s, w y • y = x

Full source

/-- This is a version of `Finset.mem_convexHull` stated without `Finset.centerMass`. -/
lemma Finset.mem_convexHull' {s : Finset E} {x : E} :
    x ∈ convexHull R (s : Set E)x ∈ convexHull R (s : Set E) ↔
      ∃ w : E → R, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ ∑ y ∈ s, w y • y = x := by
  rw [mem_convexHull]
  refine exists_congr fun w ↦ and_congr_right' <| and_congr_right fun hw ↦ ?_
  simp_rw [centerMass_eq_of_sum_1 _ _ hw, id_eq]

Characterization of Convex Hull Membership via Weighted Sums for Finite Sets

Informal description

For any finite set $s$ in a vector space $E$ over a scalar ring $R$, a point $x \in E$ belongs to the convex hull of $s$ if and only if there exists a weight function $w \colon E \to R$ such that: 1. $w(y) \geq 0$ for all $y \in s$, 2. $\sum_{y \in s} w(y) = 1$, and 3. $x$ is the weighted sum $\sum_{y \in s} w(y) \cdot y$. In other words, $x$ is in the convex hull of $s$ precisely when it can be expressed as a convex combination of points in $s$.

Set.Finite.convexHull_eq theorem

 {s : Set E} (hs : s.Finite) :
  convexHull R s =
    {x : E | ∃ w : E → R, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ hs.toFinset, w y = 1 ∧ hs.toFinset.centerMass w id = x}

Full source

theorem Set.Finite.convexHull_eq {s : Set E} (hs : s.Finite) : convexHull R s =
    { x : E | ∃ w : E → R, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ hs.toFinset, w y = 1 ∧
      hs.toFinset.centerMass w id = x } := by
  simpa only [Set.Finite.coe_toFinset, Set.Finite.mem_toFinset, exists_prop] using
    hs.toFinset.convexHull_eq

Characterization of Convex Hull via Convex Combinations for Finite Sets

Informal description

For any finite set $s$ in a vector space $E$ over a scalar ring $R$, the convex hull of $s$ is equal to the set of all points $x \in E$ for which there exists a weight function $w \colon E \to R$ such that: 1. $w(y) \geq 0$ for all $y \in s$, 2. $\sum_{y \in s} w(y) = 1$, and 3. $x$ is the center of mass of $s$ with respect to $w$ and the identity function. In other words, the convex hull consists precisely of all convex combinations of points in $s$.

convexHull_eq_union_convexHull_finite_subsets theorem

(s : Set E) : convexHull R s = ⋃ (t : Finset E) (_ : ↑t ⊆ s), convexHull R ↑t

Full source

/-- A weak version of Carathéodory's theorem. -/
theorem convexHull_eq_union_convexHull_finite_subsets (s : Set E) :
    convexHull R s = ⋃ (t : Finset E) (_ : ↑t ⊆ s), convexHull R ↑t := by
  classical
  refine Subset.antisymm ?_ ?_
  · rw [_root_.convexHull_eq]
    rintro x ⟨ι, t, w, z, hw₀, hw₁, hz, rfl⟩
    simp only [mem_iUnion]
    refine ⟨t.image z, ?_, ?_⟩
    · rw [coe_image, Set.image_subset_iff]
      exact hz
    · apply t.centerMass_mem_convexHull hw₀
      · simp only [hw₁, zero_lt_one]
      · exact fun i hi => Finset.mem_coe.2 (Finset.mem_image_of_mem _ hi)
  · exact iUnion_subset fun i => iUnion_subset convexHull_mono

Convex Hull as Union of Finite Subset Convex Hulls

Informal description

For any subset $s$ of a vector space $E$ over a scalar ring $R$, the convex hull of $s$ is equal to the union of the convex hulls of all finite subsets of $s$. In other words: \[ \text{convexHull}_R(s) = \bigcup_{\substack{t \subseteq s \\ t \text{ finite}}} \text{convexHull}_R(t) \]

mk_mem_convexHull_prod theorem

 {t : Set F} {x : E} {y : F} (hx : x ∈ convexHull R s) (hy : y ∈ convexHull R t) : (x, y) ∈ convexHull R (s ×ˢ t)

Full source

theorem mk_mem_convexHull_prod {t : Set F} {x : E} {y : F} (hx : x ∈ convexHull R s)
    (hy : y ∈ convexHull R t) : (x, y)(x, y) ∈ convexHull R (s ×ˢ t) := by
  rw [mem_convexHull_iff_exists_fintype] at hx hy ⊢
  obtain ⟨ι, _, w, f, hw₀, hw₁, hfs, hf⟩ := hx
  obtain ⟨κ, _, v, g, hv₀, hv₁, hgt, hg⟩ := hy
  have h_sum : ∑ i : ι × κ, w i.1 * v i.2 = 1 := by
    rw [Fintype.sum_prod_type, ← sum_mul_sum, hw₁, hv₁, mul_one]
  refine ⟨ι × κ, inferInstance, fun p => w p.1 * v p.2, fun p ↦ (f p.1, g p.2),
    fun p ↦ mul_nonneg (hw₀ _) (hv₀ _), h_sum, fun p ↦ ⟨hfs _, hgt _⟩, ?_⟩
  ext
  · simp_rw [Prod.fst_sum, Prod.smul_mk, Fintype.sum_prod_type, mul_comm (w _), mul_smul,
      sum_comm (γ := ι), ← Fintype.sum_smul_sum, hv₁, one_smul, hf]
  · simp_rw [Prod.snd_sum, Prod.smul_mk, Fintype.sum_prod_type, mul_smul, ← Fintype.sum_smul_sum,
      hw₁, one_smul, hg]

Pair in Convex Hull of Product Set

Informal description

For any subsets $s \subseteq E$ and $t \subseteq F$ of vector spaces over a scalar ring $R$, if $x$ belongs to the convex hull of $s$ and $y$ belongs to the convex hull of $t$, then the pair $(x, y)$ belongs to the convex hull of the Cartesian product $s \times t$.

convexHull_prod theorem

(s : Set E) (t : Set F) : convexHull R (s ×ˢ t) = convexHull R s ×ˢ convexHull R t

Full source

@[simp]
theorem convexHull_prod (s : Set E) (t : Set F) :
    convexHull R (s ×ˢ t) = convexHull R s ×ˢ convexHull R t :=
  Subset.antisymm
      (convexHull_min (prod_mono (subset_convexHull _ _) <| subset_convexHull _ _) <|
        (convex_convexHull _ _).prod <| convex_convexHull _ _) <|
    prod_subset_iff.2 fun _ hx _ => mk_mem_convexHull_prod hx

Convex Hull of Cartesian Product Equals Product of Convex Hulls

Informal description

For any subsets $s \subseteq E$ and $t \subseteq F$ of vector spaces over a scalar ring $R$, the convex hull of their Cartesian product $s \times t$ is equal to the Cartesian product of their convex hulls, i.e., \[ \text{convexHull}_R(s \times t) = \text{convexHull}_R(s) \times \text{convexHull}_R(t). \]

convexHull_add theorem

(s t : Set E) : convexHull R (s + t) = convexHull R s + convexHull R t

Full source

theorem convexHull_add (s t : Set E) : convexHull R (s + t) = convexHull R s + convexHull R t := by
  simp_rw [← add_image_prod, ← IsLinearMap.isLinearMap_add.image_convexHull, convexHull_prod]

Convex Hull of Minkowski Sum Equals Minkowski Sum of Convex Hulls

Informal description

For any subsets $s$ and $t$ of a vector space $E$ over a scalar ring $R$, the convex hull of their Minkowski sum $s + t$ is equal to the Minkowski sum of their convex hulls, i.e., \[ \text{convexHull}_R(s + t) = \text{convexHull}_R(s) + \text{convexHull}_R(t). \]

convexHullAddMonoidHom definition

: Set E →+ Set E

Full source

/-- `convexHull` is an additive monoid morphism under pointwise addition. -/
@[simps]
def convexHullAddMonoidHom : SetSet E →+ Set E where
  toFun := convexHull R
  map_add' := convexHull_add
  map_zero' := convexHull_zero

Convex Hull as an Additive Monoid Homomorphism

Informal description

The function that maps a subset $s$ of a vector space $E$ over a scalar ring $R$ to its convex hull $\text{convexHull}_R(s)$ is an additive monoid homomorphism under pointwise addition of sets. That is, it satisfies: 1. $\text{convexHull}_R(s + t) = \text{convexHull}_R(s) + \text{convexHull}_R(t)$ for any subsets $s, t \subseteq E$ 2. $\text{convexHull}_R(\emptyset) = \emptyset$

convexHull_sub theorem

(s t : Set E) : convexHull R (s - t) = convexHull R s - convexHull R t

Full source

theorem convexHull_sub (s t : Set E) : convexHull R (s - t) = convexHull R s - convexHull R t := by
  simp_rw [sub_eq_add_neg, convexHull_add, ← convexHull_neg]

Convex Hull of Set Difference Equals Set Difference of Convex Hulls

Informal description

For any subsets $s$ and $t$ of a vector space $E$ over a scalar ring $R$, the convex hull of their set difference $s - t$ is equal to the set difference of their convex hulls, i.e., \[ \text{convexHull}_R(s - t) = \text{convexHull}_R(s) - \text{convexHull}_R(t). \]

convexHull_list_sum theorem

(l : List (Set E)) : convexHull R l.sum = (l.map <| convexHull R).sum

Full source

theorem convexHull_list_sum (l : List (Set E)) : convexHull R l.sum = (l.map <| convexHull R).sum :=
  map_list_sum (convexHullAddMonoidHom R E) l

Convex Hull of Minkowski Sum of List of Sets Equals Minkowski Sum of Convex Hulls

Informal description

For any list $l$ of subsets of a vector space $E$ over a scalar ring $R$, the convex hull of the Minkowski sum of the sets in $l$ is equal to the Minkowski sum of the convex hulls of each set in $l$. That is, \[ \text{convexHull}_R\left(\sum_{s \in l} s\right) = \sum_{s \in l} \text{convexHull}_R(s). \]

convexHull_multiset_sum theorem

(s : Multiset (Set E)) : convexHull R s.sum = (s.map <| convexHull R).sum

Full source

theorem convexHull_multiset_sum (s : Multiset (Set E)) :
    convexHull R s.sum = (s.map <| convexHull R).sum :=
  map_multiset_sum (convexHullAddMonoidHom R E) s

Convex Hull of Multiset Sum Equals Sum of Convex Hulls

Informal description

For any multiset $s$ of subsets of a vector space $E$ over a scalar ring $R$, the convex hull of the sum of the subsets in $s$ is equal to the sum of the convex hulls of each subset in $s$. That is, \[ \text{convexHull}_R \left( \sum_{A \in s} A \right) = \sum_{A \in s} \text{convexHull}_R(A). \]

convexHull_sum theorem

{ι} (s : Finset ι) (t : ι → Set E) : convexHull R (∑ i ∈ s, t i) = ∑ i ∈ s, convexHull R (t i)

Full source

theorem convexHull_sum {ι} (s : Finset ι) (t : ι → Set E) :
    convexHull R (∑ i ∈ s, t i) = ∑ i ∈ s, convexHull R (t i) :=
  map_sum (convexHullAddMonoidHom R E) _ _

Convex Hull Commutes with Finite Minkowski Sums

Informal description

For any finite index set $s \subseteq \iota$ and any family of sets $t_i \subseteq E$ indexed by $i \in \iota$, the convex hull of the Minkowski sum $\sum_{i \in s} t_i$ is equal to the Minkowski sum of the convex hulls $\sum_{i \in s} \text{convexHull}_R(t_i)$. In other words, the convex hull operator commutes with finite Minkowski sums: \[ \text{convexHull}_R\left(\sum_{i \in s} t_i\right) = \sum_{i \in s} \text{convexHull}_R(t_i). \]

convexHull_basis_eq_stdSimplex theorem

[DecidableEq ι] : convexHull R (range fun i j : ι => if i = j then (1 : R) else 0) = stdSimplex R ι

Full source

/-- `stdSimplex 𝕜 ι` is the convex hull of the canonical basis in `ι → 𝕜`. -/
theorem convexHull_basis_eq_stdSimplex [DecidableEq ι] :
    convexHull R (range fun i j : ι => if i = j then (1 : R) else 0) = stdSimplex R ι := by
  refine Subset.antisymm (convexHull_min ?_ (convex_stdSimplex R ι)) ?_
  · rintro _ ⟨i, rfl⟩
    exact ite_eq_mem_stdSimplex R i
  · rintro w ⟨hw₀, hw₁⟩
    rw [pi_eq_sum_univ w, ← Finset.univ.centerMass_eq_of_sum_1 _ hw₁]
    exact Finset.univ.centerMass_mem_convexHull (fun i _ => hw₀ i) (hw₁.symm ▸ zero_lt_one)
      fun i _ => mem_range_self i

Convex Hull of Indicator Functions Equals Standard Simplex

Informal description

For a type $\iota$ with decidable equality and a scalar ring $R$, the convex hull of the set of indicator functions $\{\mathbf{1}_i \mid i \in \iota\}$ (where $\mathbf{1}_i(j) = 1$ if $i = j$ and $0$ otherwise) is equal to the standard simplex in the function space $\iota \to R$. That is, \[ \text{convexHull}_R \left( \{\mathbf{1}_i \mid i \in \iota\} \right) = \text{stdSimplex}_R \iota. \]

Set.Finite.convexHull_eq_image theorem

 {s : Set E} (hs : s.Finite) :
  convexHull R s =
    haveI := hs.fintype
    (⇑(∑ x : s, (@LinearMap.proj R s _ (fun _ => R) _ _ x).smulRight x.1)) '' stdSimplex R s

Full source

/-- 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 Set.Finite.convexHull_eq_image {s : Set E} (hs : s.Finite) : convexHull R s =
    haveI := hs.fintype
    (⇑(∑ x : s, (@LinearMap.proj R s _ (fun _ => R) _ _ x).smulRight x.1)) '' stdSimplex R s := by
  classical
  letI := hs.fintype
  rw [← convexHull_basis_eq_stdSimplex, LinearMap.image_convexHull, ← Set.range_comp]
  apply congr_arg
  simp_rw [Function.comp_def]
  convert Subtype.range_coe.symm
  simp [LinearMap.sum_apply, ite_smul, Finset.filter_eq, Finset.mem_univ]

Convex Hull of Finite Set as Linear Image of Standard Simplex

Informal description

For any finite subset $s$ of a vector space $E$ over a scalar ring $R$, the convex hull of $s$ is equal to the image of the standard simplex in the function space $s \to R$ under the linear map that sends each function $w$ to the weighted sum $\sum_{x \in s} w(x) \cdot x$.

mem_Icc_of_mem_stdSimplex theorem

(hf : f ∈ stdSimplex R ι) (x) : f x ∈ Icc (0 : R) 1

Full source

/-- All values of a function `f ∈ stdSimplex 𝕜 ι` belong to `[0, 1]`. -/
theorem mem_Icc_of_mem_stdSimplex (hf : f ∈ stdSimplex R ι) (x) : f x ∈ Icc (0 : R) 1 :=
  ⟨hf.1 x, hf.2 ▸ Finset.single_le_sum (fun y _ => hf.1 y) (Finset.mem_univ x)⟩

Values of Standard Simplex Functions Lie in $[0,1]$

Informal description

For any function $f$ in the standard simplex $\text{stdSimplex}(R, \iota)$ and any element $x \in \iota$, the value $f(x)$ lies in the closed interval $[0, 1]$.

AffineBasis.convexHull_eq_nonneg_coord theorem

{ι : Type*} (b : AffineBasis ι R E) : convexHull R (range b) = {x | ∀ i, 0 ≤ b.coord i x}

Full source

/-- The convex hull of an affine basis is the intersection of the half-spaces defined by the
corresponding barycentric coordinates. -/
theorem AffineBasis.convexHull_eq_nonneg_coord {ι : Type*} (b : AffineBasis ι R E) :
    convexHull R (range b) = { x | ∀ i, 0 ≤ b.coord i x } := by
  rw [convexHull_range_eq_exists_affineCombination]
  ext x
  refine ⟨?_, fun hx => ?_⟩
  · rintro ⟨s, w, hw₀, hw₁, rfl⟩ i
    by_cases hi : i ∈ s
    · rw [b.coord_apply_combination_of_mem hi hw₁]
      exact hw₀ i hi
    · rw [b.coord_apply_combination_of_not_mem hi hw₁]
  · have hx' : x ∈ affineSpan R (range b) := by
      rw [b.tot]
      exact AffineSubspace.mem_top R E x
    obtain ⟨s, w, hw₁, rfl⟩ := (mem_affineSpan_iff_eq_affineCombination R E).mp hx'
    refine ⟨s, w, ?_, hw₁, rfl⟩
    intro i hi
    specialize hx i
    rw [b.coord_apply_combination_of_mem hi hw₁] at hx
    exact hx

Convex Hull of Affine Basis via Nonnegative Coordinates

Informal description

Let $E$ be a vector space over a scalar ring $R$ and let $b \colon \iota \to E$ be an affine basis. The convex hull of the range of $b$ is equal to the set of all points $x \in E$ such that for every coordinate function $b.\mathrm{coord}_i$ associated with the basis, the coordinate value satisfies $b.\mathrm{coord}_i(x) \geq 0$.

AffineIndependent.convexHull_inter theorem

 (hs : AffineIndependent R ((↑) : s → E)) (ht₁ : t₁ ⊆ s) (ht₂ : t₂ ⊆ s) :
  convexHull R (t₁ ∩ t₂ : Set E) = convexHull R t₁ ∩ convexHull R t₂

Full source

/-- Two simplices glue nicely if the union of their vertices is affine independent. -/
lemma AffineIndependent.convexHull_inter (hs : AffineIndependent R ((↑) : s → E))
    (ht₁ : t₁ ⊆ s) (ht₂ : t₂ ⊆ s) :
    convexHull R (t₁ ∩ t₂ : Set E) = convexHullconvexHull R t₁ ∩ convexHull R t₂ := by
  classical
  refine (Set.subset_inter (convexHull_mono inf_le_left) <|
    convexHull_mono inf_le_right).antisymm ?_
  simp_rw [Set.subset_def, mem_inter_iff, Set.inf_eq_inter, ← coe_inter, mem_convexHull']
  rintro x ⟨⟨w₁, h₁w₁, h₂w₁, h₃w₁⟩, w₂, -, h₂w₂, h₃w₂⟩
  let w (x : E) : R := (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
  have h₁w : ∑ i ∈ s, w i = 0 := by simp [w, Finset.inter_eq_right.2, *]
  replace hs := hs.eq_zero_of_sum_eq_zero_subtype h₁w <| by
    simp only [w, sub_smul, zero_smul, ite_smul, Finset.sum_sub_distrib, ← Finset.sum_filter, h₃w₁,
      Finset.filter_mem_eq_inter, Finset.inter_eq_right.2 ht₁, Finset.inter_eq_right.2 ht₂, h₃w₂,
      sub_self]
  have ht (x) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂) : w₁ x = 0 := by
    simpa [w, hx₁, hx₂] using hs _ (ht₁ hx₁)
  refine ⟨w₁, ?_, ?_, ?_⟩
  · simp only [and_imp, Finset.mem_inter]
    exact fun y hy₁ _ ↦ h₁w₁ y hy₁
  all_goals
  · rwa [sum_subset inter_subset_left]
    rintro x
    simp_intro hx₁ hx₂
    simp [ht x hx₁ hx₂]

Convex Hull of Intersection Equals Intersection of Convex Hulls for Affine Independent Sets

Informal description

Let $E$ be a vector space over a scalar ring $R$, and let $s$ be a subset of $E$ that is affine independent. For any subsets $t_1, t_2 \subseteq s$, the convex hull of their intersection equals the intersection of their convex hulls, i.e., \[ \text{convexHull}_R(t_1 \cap t_2) = \text{convexHull}_R(t_1) \cap \text{convexHull}_R(t_2). \]

AffineIndependent.convexHull_inter' theorem

 [DecidableEq E] (hs : AffineIndependent R ((↑) : ↑(t₁ ∪ t₂) → E)) :
  convexHull R (t₁ ∩ t₂ : Set E) = convexHull R t₁ ∩ convexHull R t₂

Full source

/-- 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. -/
lemma AffineIndependent.convexHull_inter' [DecidableEq E]
    (hs : AffineIndependent R ((↑) : ↑(t₁ ∪ t₂) → E)) :
    convexHull R (t₁ ∩ t₂ : Set E) = convexHullconvexHull R t₁ ∩ convexHull R t₂ :=
  hs.convexHull_inter subset_union_left subset_union_right

Convex Hull of Intersection Equals Intersection of Convex Hulls for Affine Independent Union

Informal description

Let $E$ be a vector space over a scalar ring $R$, and let $t_1, t_2$ be subsets of $E$ such that the union $t_1 \cup t_2$ is affine independent. Then the convex hull of the intersection $t_1 \cap t_2$ equals the intersection of the convex hulls of $t_1$ and $t_2$, i.e., \[ \text{convexHull}_R(t_1 \cap t_2) = \text{convexHull}_R(t_1) \cap \text{convexHull}_R(t_2). \]

mem_convexHull_pi theorem

(h : ∀ i ∈ s, x i ∈ convexHull 𝕜 (t i)) : x ∈ convexHull 𝕜 (s.pi t)

Full source

lemma mem_convexHull_pi (h : ∀ i ∈ s, x i ∈ convexHull 𝕜 (t i)) : x ∈ convexHull 𝕜 (s.pi t) := by
  classical
  cases nonempty_fintype ι
  wlog hs : s = Set.univ generalizing s t
  · rw [← pi_univ_ite]
    refine this (fun i _ ↦ ?_) rfl
    split_ifs with hi
    · exact h i hi
    · simp
  subst hs
  simp only [Set.mem_univ, mem_convexHull_iff_exists_fintype, true_implies, Set.mem_pi] at h
  choose κ _ w f hw₀ hw₁ hft hf using h
  refine mem_convexHull_of_exists_fintype (fun k : Π i, κ i ↦ ∏ i, w i (k i)) (fun g i ↦ f _ (g i))
    (fun g ↦ prod_nonneg fun _ _ ↦ hw₀ _ _) ?_ (fun _ _ _ ↦ hft _ _) ?_
  · rw [← Fintype.prod_sum]
    exact prod_eq_one fun _ _ ↦ hw₁ _
  ext i
  calc
    _ = ∑ g : ∀ i, κ i, (∏ i, w i (g i)) • f i (g i) := by
      simp only [Finset.sum_apply, Pi.smul_apply]
    _ = ∑ j : κ i, ∑ g : {g : ∀ k, κ k // g i = j},
          (∏ k, w k (g.1 k)) • f i ((g : ∀ i, κ i) i) := by
      rw [← Fintype.sum_fiberwise fun g : ∀ k, κ k ↦ g i]
    _ = ∑ j : κ i, (∑ g : {g : ∀ k, κ k // g i = j}, ∏ k, w k (g.1 k)) • f i j := by
      simp_rw [sum_smul]
      congr! with j _ g _
      exact g.2
    _ = ∑ j : κ i, w i j • f i j := ?_
    _ = x i := hf _
  congr! with j _
  calc
    ∑ g : {g : ∀ k, κ k // g i = j}, ∏ k, w k (g.1 k)
      = ∑ g ∈ piFinset fun k ↦ if hk : k = i then hk ▸ {j} else univ, ∏ k, w k (g k) :=
      Finset.sum_bij' (fun g _ ↦ g) (fun g hg ↦ ⟨g, by simpa using mem_piFinset.1 hg i⟩)
        (by aesop) (by simp) (by simp) (by simp) (by simp)
    _ = w i j := by
      rw [← prod_univ_sum, ← prod_mul_prod_compl, Finset.prod_singleton, Finset.sum_eq_single,
        Finset.prod_eq_one, mul_one] <;> simp +contextual [hw₁]

Convex Hull Membership in Product Spaces

Informal description

Let $\mathbb{K}$ be a scalar ring, $E$ a vector space over $\mathbb{K}$, and $s$ a set of indices. For each $i \in s$, let $t_i$ be a subset of $E_i$. If for every $i \in s$ the element $x_i$ belongs to the convex hull of $t_i$, then the tuple $x = (x_i)_{i \in s}$ belongs to the convex hull of the product set $\prod_{i \in s} t_i$.

convexHull_pi theorem

(s : Set ι) (t : Π i, Set (E i)) : convexHull 𝕜 (s.pi t) = s.pi (fun i ↦ convexHull 𝕜 (t i))

Full source

@[simp] lemma convexHull_pi (s : Set ι) (t : Π i, Set (E i)) :
    convexHull 𝕜 (s.pi t) = s.pi (fun i ↦ convexHull 𝕜 (t i)) :=
  Set.Subset.antisymm (convexHull_min (Set.pi_mono fun _ _ ↦ subset_convexHull _ _) <| convex_pi <|
    fun _ _ ↦ convex_convexHull _ _) fun _ ↦ mem_convexHull_pi

Convex Hull of Product Set Equals Product of Convex Hulls

Informal description

For any set of indices $s$ and any family of sets $t_i \subseteq E_i$ for $i \in s$, the convex hull of the product set $\prod_{i \in s} t_i$ is equal to the product of the convex hulls of each $t_i$, i.e., \[ \text{convexHull}_{\mathbb{K}}\left(\prod_{i \in s} t_i\right) = \prod_{i \in s} \text{convexHull}_{\mathbb{K}}(t_i). \]

Mathlib.Analysis.Convex.Combination

Main declarations

Implementation notes