English
For a finite index set ι, a normed space E over ℝ and an affine basis b, the interior of the convex hull of range b consists of points whose barycentric coordinates with respect to b are strictly positive.
Русский
Для конечного множества индексов ι, вещественного векторного пространства E и аффинной базы b interior(convexHull) состоит из точек, у которых барицентрические коэффициенты по отношению к b строго положительны.
LaTeX
$$$$\operatorname{int}(\operatorname{convexHull}_{\mathbb{R}}(\operatorname{range}(b))) = \{ x \mid \forall i, 0 < b.coord(i)x \}. $$$$
Lean4
/-- Given a finite-dimensional normed real vector space, the interior of the convex hull of an
affine basis is the set of points whose barycentric coordinates are strictly positive with respect
to this basis.
TODO Restate this result for affine spaces (instead of vector spaces) once the definition of
convexity is generalised to this setting. -/
theorem interior_convexHull {ι E : Type*} [Finite ι] [NormedAddCommGroup E] [NormedSpace ℝ E] (b : AffineBasis ι ℝ E) :
interior (convexHull ℝ (range b)) = {x | ∀ i, 0 < b.coord i x} :=
by
cases subsingleton_or_nontrivial ι
· -- The zero-dimensional case.
have : range b = univ := AffineSubspace.eq_univ_of_subsingleton_span_eq_top (subsingleton_range _) b.tot
simp [this]
· -- The positive-dimensional case.
haveI : FiniteDimensional ℝ E := b.finiteDimensional
have : convexHull ℝ (range b) = ⋂ i, b.coord i ⁻¹' Ici 0 := by rw [b.convexHull_eq_nonneg_coord, setOf_forall]; rfl
ext
simp only [this, interior_iInter_of_finite,
←
IsOpenMap.preimage_interior_eq_interior_preimage (isOpenMap_barycentric_coord b _)
(continuous_barycentric_coord b _),
interior_Ici, mem_iInter, mem_setOf_eq, mem_Ioi, mem_preimage]
