English
The convex hull of the range of an affine basis is the set of all points whose barycentric coordinates with respect to the basis are nonnegative.
Русский
Выпуклая оболочка диапазона аффинной базы состоит из всех точек с неотрицательными барицентрическими координатами относительно этой базы.
LaTeX
$$$\operatorname{conv}(R, \operatorname{range}(b)) = \{x : E \mid \forall i, 0 \le b.coord\, i\, x\}$$$
Lean4
/-- The convex hull of an affine basis is the intersection of the half-spaces defined by the
corresponding barycentric coordinates. -/
theorem convexHull_eq_nonneg_coord {ι : Type*} (b : AffineBasis ι R E) :
convexHull R (range b) = {x | ∀ i, 0 ≤ b.coord i x} :=
by
rw [convexHull_range_eq_exists_affineCombination]
ext x
refine ⟨?_, fun hx => ?_⟩
· rintro ⟨s, w, hw₀, hw₁, rfl⟩ i
by_cases hi : i ∈ s
· rw [b.coord_apply_combination_of_mem hi hw₁]
exact hw₀ i hi
· rw [b.coord_apply_combination_of_notMem hi hw₁]
· have hx' : x ∈ affineSpan R (range b) := by
rw [b.tot]
exact AffineSubspace.mem_top R E x
obtain ⟨s, w, hw₁, rfl⟩ := (mem_affineSpan_iff_eq_affineCombination R E).mp hx'
refine ⟨s, w, ?_, hw₁, rfl⟩
intro i hi
specialize hx i
rw [b.coord_apply_combination_of_mem hi hw₁] at hx
exact hx
