English
Characterizes convex hull as the set of all centers of masses of finite index families, with the original points lying in 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
/-- 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 [← 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
