feat(analysis/normed_space/add_torsor_bases): the interior of the con…

…vex hull of a finite affine basis is the set of points with strictly positive barycentric coordinates (#9583)

Formalized as part of the Sphere Eversion project.

src/analysis/convex/hull.lean

@@ -57,6 +57,9 @@ lemma convex_hull_mono (hst : s ⊆ t) : convex_hull 𝕜 s ⊆ convex_hull 𝕜
 lemma convex.convex_hull_eq {s : set E} (hs : convex 𝕜 s) : convex_hull 𝕜 s = s :=
 closure_operator.mem_mk₃_closed hs
 
+@[simp] lemma convex_hull_univ : convex_hull 𝕜 (univ : set E) = univ :=
+closure_operator.closure_top (convex_hull 𝕜)
+
 @[simp] lemma convex_hull_empty : convex_hull 𝕜 (∅ : set E) = ∅ := convex_empty.convex_hull_eq
 
 @[simp] lemma convex_hull_empty_iff : convex_hull 𝕜 s = ∅ ↔ s = ∅ :=

src/analysis/normed_space/add_torsor_bases.lean

@@ -5,6 +5,7 @@ Authors: Oliver Nash
 -/
 import analysis.normed_space.banach
 import analysis.normed_space.finite_dimension
+import analysis.convex.combination
 import linear_algebra.affine_space.barycentric_coords
 
 /-!
@@ -16,6 +17,7 @@ This file contains results about bases in normed affine spaces.
 
  * `continuous_barycentric_coord`
  * `is_open_map_barycentric_coord`
+ * `interior_convex_hull_aff_basis`
  * `exists_subset_affine_independent_affine_span_eq_top_of_open`
 -/
 
@@ -40,6 +42,39 @@ open_mapping_affine
 
 end barycentric
 
+open set
+
+/-- 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. -/
+lemma interior_convex_hull_aff_basis {ι E : Type*} [fintype ι] [normed_group E] [normed_space ℝ E]
+  {p : ι → E} (h_ind : affine_independent ℝ p) (h_tot : affine_span ℝ (range p) = ⊤) :
+  interior (convex_hull ℝ (range p)) = { x | ∀ i, 0 < barycentric_coord h_ind h_tot i x } :=
+begin
+  cases subsingleton_or_nontrivial ι with h h,
+  { -- The zero-dimensional case.
+    haveI := h,
+    suffices : range p = univ, { simp [this], },
+    refine affine_subspace.eq_univ_of_subsingleton_span_eq_top _ h_tot,
+    rw ← image_univ,
+    exact subsingleton.image subsingleton_of_subsingleton p, },
+  { -- The positive-dimensional case.
+    haveI : finite_dimensional ℝ E,
+    { classical,
+      obtain ⟨i⟩ := (infer_instance : nonempty ι),
+      have b := basis_of_aff_ind_span_eq_top h_ind h_tot i,
+      exact finite_dimensional.of_fintype_basis b, },
+    have : convex_hull ℝ (range p) = ⋂ i, (barycentric_coord h_ind h_tot i)⁻¹' Ici 0,
+    { rw convex_hull_affine_basis_eq_nonneg_barycentric h_ind h_tot, ext, simp, },
+    ext,
+    simp only [this, interior_Inter_of_fintype, ← is_open_map.preimage_interior_eq_interior_preimage
+      (continuous_barycentric_coord h_ind h_tot _) (is_open_map_barycentric_coord h_ind h_tot _),
+      interior_Ici, mem_Inter, mem_set_of_eq, mem_Ioi, mem_preimage], },
+end
+
 variables {V P : Type*} [normed_group V] [normed_space ℝ V] [metric_space P] [normed_add_torsor V P]
 include V
 

src/linear_algebra/affine_space/affine_subspace.lean

@@ -710,6 +710,15 @@ begin
   exact subsingleton_of_univ_subsingleton h₂,
 end
 
+lemma eq_univ_of_subsingleton_span_eq_top {s : set P} (h₁ : s.subsingleton)
+  (h₂ : affine_span k s = ⊤) : s = (univ : set P) :=
+begin
+  obtain ⟨p, hp⟩ := affine_subspace.nonempty_of_affine_span_eq_top k V P h₂,
+  have : s = {p}, { exact subset.antisymm (λ q hq, h₁ hq hp) (by simp [hp]), },
+  rw [this, eq_comm, ← subsingleton_iff_singleton (mem_univ p), subsingleton_univ_iff],
+  exact subsingleton_of_subsingleton_span_eq_top h₁ h₂,
+end
+
 /-- A nonempty affine subspace is `⊤` if and only if its direction is
 `⊤`. -/
 @[simp] lemma direction_eq_top_iff_of_nonempty {s : affine_subspace k P}