English
The convex hull equals the set of all centers of masses of finite index families drawn from the set.
Русский
Выпуклая оболочка равна множеству всех центров масс конечных семейств точек из множества.
LaTeX
$$convexHull R s = {x | ∃ (ι) (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}$$
Lean4
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₁
