English
Let s be a finite subset of a vector space E. Then the convex hull of s consists exactly of all barycenters of s with nonnegative weights summing to 1; equivalently, x is in conv_R(s) iff there exists a weight function w on E with w(y) ≥ 0 for y in s, sum_{y∈s} w(y) = 1, and x = sum_{y∈s} w(y) y.
Русский
Пусть s — конечное подмножество пространства E. Тогда выпуклая оболочка s состоит ровно из всех барицентров системы s с неотрицательными весами, сумма которых равна 1; эквивалентно: x принадлежит conv_R(s) тогда и только тогда, существует w: E → R с w(y) ≥ 0 для y в s, ∑_{y∈s} w(y) = 1 и x = ∑_{y∈s} w(y) y.
LaTeX
$$$x \in \operatorname{conv}(R, \uparrow s) \\iff \exists w : E \to \mathbb{R},\; (\forall y \in s, 0 \le w(y)) \; \wedge \; \sum_{y \in s} w(y) = 1 \; \wedge \; \sum_{y \in s} w(y) \; y = x$$$
Lean4
theorem 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
