English
For a finite set s, the convex hull in R is the image of the standard simplex under the linear map sending a weight function w on s to ∑_{x ∈ s} w(x)·x.
Русский
Для конечного множества s выпуклая оболочка в R равна образу стандартного симплекса через линейное отображение, отправляющее взвешенную сумму ∑_{x∈s} w(x)·x.
LaTeX
$$$\operatorname{convexHull}_{R}(s) = (\sum_{x\in s} (\text{LinearMap.proj } x).smulRight(x))'' \mathrm{stdSimplex}_{R}(s)$$$
Lean4
/-- 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 convexHull_eq_image {E : Type*} [AddCommGroup E] [Module R E] {s : Set E} (hs : s.Finite) :
convexHull R s =
haveI := hs.fintype
(⇑(∑ x : s, (LinearMap.proj (R := 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
aesop
