English
If x lies in the convex hull of s, there exist a finite index set with points z_i ∈ s, positive weights w_i summing to 1, such that x is the affine combination ∑ w_i z_i with z_i affinely independent.
Русский
Если x лежит в выпуклой оболочке s, то существует конечное перечисление точек z_i ∈ s и положительные веса w_i, сумма которых равна 1, так что x = ∑ w_i z_i и {z_i} аффинно независимы.
LaTeX
$$$\\exists \\iota, (z_i)_{i∈\\iota}, (w_i)_{i∈\\iota} :\\text{finitemulti},\\ 0< w_i\\ \\forall i,\\ \\sum_i w_i = 1\\text{ and }\\sum_i w_i z_i = x\\text{ with }\\{z_i\\}\\text{ affinely independent and }\\operatorname{range}z\\subseteq s$$$
Lean4
/-- A more explicit version of `convexHull_eq_union`. -/
theorem eq_pos_convex_span_of_mem_convexHull {x : E} (hx : x ∈ convexHull 𝕜 s) :
∃ (ι : Sort (u + 1)) (_ : Fintype ι),
∃ (z : ι → E) (w : ι → 𝕜),
Set.range z ⊆ s ∧ AffineIndependent 𝕜 z ∧ (∀ i, 0 < w i) ∧ ∑ i, w i = 1 ∧ ∑ i, w i • z i = x :=
by
rw [convexHull_eq_union] at hx
simp only [exists_prop, Set.mem_iUnion] at hx
obtain ⟨t, ht₁, ht₂, ht₃⟩ := hx
simp only [t.convexHull_eq, Set.mem_setOf_eq] at ht₃
obtain ⟨w, hw₁, hw₂, hw₃⟩ := ht₃
let t' := {i ∈ t | w i ≠ 0}
refine ⟨t', t'.fintypeCoeSort, ((↑) : t' → E), w ∘ ((↑) : t' → E), ?_, ?_, ?_, ?_, ?_⟩
· rw [Subtype.range_coe_subtype]
exact Subset.trans (Finset.filter_subset _ t) ht₁
· exact ht₂.comp_embedding ⟨_, inclusion_injective (Finset.filter_subset (fun i => w i ≠ 0) t)⟩
· exact fun i => (hw₁ _ (Finset.mem_filter.mp i.2).1).lt_of_ne (Finset.mem_filter.mp i.property).2.symm
· simp only [univ_eq_attach, Function.comp_apply]
rw [Finset.sum_attach, Finset.sum_filter_ne_zero, hw₂]
· change (∑ i ∈ t'.attach, (fun e => w e • e) ↑i) = x
rw [Finset.sum_attach (f := fun e => w e • e), Finset.sum_filter_of_ne]
· rw [t.centerMass_eq_of_sum_1 id hw₂] at hw₃
exact hw₃
· intro e _ hwe contra
apply hwe
rw [contra, zero_smul]
