English
For a real affine space with a finite basis b, the interior of convex hull of range b equals the positivity set of barycentric coordinates.
Русский
Для нормированного вещественного пространства с конечной базой b interior(convexHull( range b)) совпадает с множеством точек, для которых барицентрические координаты положительны.
LaTeX
$$$$\operatorname{Interior}(\operatorname{convexHull}_{\mathbb{R}}(\operatorname{range}(b))) = \{x \ | \ \forall i, 0 < b.coord(i)x\}.$$$$
Lean4
/-- Given a set `s` of affine-independent points belonging to an open set `u`, we may extend `s` to
an affine basis, all of whose elements belong to `u`. -/
theorem exists_between_affineIndependent_span_eq_top {s u : Set P} (hu : IsOpen u) (hsu : s ⊆ u) (hne : s.Nonempty)
(h : AffineIndependent ℝ ((↑) : s → P)) :
∃ t : Set P, s ⊆ t ∧ t ⊆ u ∧ AffineIndependent ℝ ((↑) : t → P) ∧ affineSpan ℝ t = ⊤ :=
by
obtain ⟨q, hq⟩ := hne
obtain ⟨ε, ε0, hεu⟩ := Metric.nhds_basis_closedBall.mem_iff.1 (hu.mem_nhds <| hsu hq)
obtain ⟨t, ht₁, ht₂, ht₃⟩ := exists_subset_affineIndependent_affineSpan_eq_top h
let f : P → P := fun y => lineMap q y (ε / dist y q)
have hf : ∀ y, f y ∈ u := by
refine fun y => hεu ?_
simp only [f]
rw [Metric.mem_closedBall, lineMap_apply, dist_vadd_left, norm_smul, Real.norm_eq_abs, dist_eq_norm_vsub V y q,
abs_div, abs_of_pos ε0, abs_of_nonneg (norm_nonneg _), div_mul_comm]
exact mul_le_of_le_one_left ε0.le (div_self_le_one _)
have hεyq : ∀ y ∉ s, ε / dist y q ≠ 0 := fun y hy =>
div_ne_zero ε0.ne' (dist_ne_zero.2 (ne_of_mem_of_not_mem hq hy).symm)
classical
let w : t → ℝˣ := fun p => if hp : (p : P) ∈ s then 1 else Units.mk0 _ (hεyq (↑p) hp)
refine ⟨Set.range fun p : t => lineMap q p (w p : ℝ), ?_, ?_, ?_, ?_⟩
· intro p hp; use ⟨p, ht₁ hp⟩; simp [w, hp]
· rintro y ⟨⟨p, hp⟩, rfl⟩
by_cases hps : p ∈ s <;>
simp only [w, hps, lineMap_apply_one, Units.val_mk0, dif_neg, dif_pos, not_false_iff, Units.val_one] <;>
[exact hsu hps; exact hf p]
· exact (ht₂.units_lineMap ⟨q, ht₁ hq⟩ w).range
· rw [affineSpan_eq_affineSpan_lineMap_units (ht₁ hq) w, ht₃]
