feat(LinearAlgebra/AffineSpace/Independent): interior of a simplex (#21929)

Define the notion of the interior of a simplex
(`Affine.Simplex.interior`), and also the corresponding closed set (`Affine.Simplex.closedInterior`).

It's common in geometry to refer to a point being in the interior of a triangle, and having such a definition allows such a statement to be made without depending on the convexity refactor.  Furthermore, this is a common enough concept that I think it makes sense for it to have its own definition and API even in the presence of the convexity refactor; `intrinsicInterior k (convexHull k (Set.range s.points))` is not exactly a convenient way to refer to this common construct.  (The convexity refactor would of course allow the equivalence of the two definitions to be stated and proved, or the definitions here could be redefined in terms of the general convexity ones at that point if desired.)  There are plenty of things that could be stated and proved using this definition (e.g. conditions for triangle centers to be inside the triangle) though this PR doesn't do anything like that beyond one API lemma saying when an affine combination lies in the interior of a simplex.

The corresponding `closedInterior` is by analogy to how, for example, we have both `ball` and `closedBall` in metric spaces.  The definitions are also intended to be analogous to such definitions for (not necessarily convex) polygons once we have those defined: sometimes when considering a polygon as a set of points in a plane you want the interior as an open set, sometimes the interior together with the boundary (and this analogy with polygons that aren't necessarily convex is why a simpler name such as `Affine.Simplex.convexHull` wasn't used for `closedInterior`).

Author: jsm28

Mathlib/LinearAlgebra/AffineSpace/Independent.lean

@@ -943,3 +943,43 @@ theorem centroid_eq_of_range_eq {n : ℕ} {s₁ s₂ : Simplex k P n}
 end Simplex
 
 end Affine
+
+namespace Affine
+
+namespace Simplex
+
+variable {k V P : Type*} [OrderedRing k] [AddCommGroup V] [Module k V] [AffineSpace V P]
+
+/-- The interior of a simplex is the set of points that can be expressed as an affine combination
+of the vertices with weights strictly between 0 and 1. This is equivalent to the intrinsic
+interior of the convex hull of the vertices. -/
+protected def interior {n : ℕ} (s : Simplex k P n) : Set P :=
+  {p | ∃ w : Fin (n + 1) → k,
+    (∑ i, w i = 1) ∧ (∀ i, w i ∈ Set.Ioo 0 1) ∧ Finset.univ.affineCombination k s.points w = p}
+
+lemma affineCombination_mem_interior_iff {n : ℕ} {s : Simplex k P n} {w : Fin (n + 1) → k}
+    (hw : ∑ i, w i = 1) :
+    Finset.univ.affineCombination k s.points w ∈ s.interior ↔ ∀ i, w i ∈ Set.Ioo 0 1 := by
+  refine ⟨fun ⟨w', hw', hw'01, hww'⟩ ↦ ?_, fun h ↦ ⟨w, hw, h, rfl⟩⟩
+  simp_rw [← (affineIndependent_iff_eq_of_fintype_affineCombination_eq k s.points).1
+    s.independent w' w hw' hw hww']
+  exact hw'01
+
+/-- `s.closedInterior is the set of points that can be expressed as an affine combination
+of the vertices with weights between 0 and 1 inclusive. This is equivalent to the convex hull of
+the vertices or the closure of the interior. -/
+protected def closedInterior {n : ℕ} (s : Simplex k P n) : Set P :=
+  {p | ∃ w : Fin (n + 1) → k,
+    (∑ i, w i = 1) ∧ (∀ i, w i ∈ Set.Icc 0 1) ∧ Finset.univ.affineCombination k s.points w = p}
+
+lemma affineCombination_mem_closedInterior_iff {n : ℕ} {s : Simplex k P n} {w : Fin (n + 1) → k}
+    (hw : ∑ i, w i = 1) :
+    Finset.univ.affineCombination k s.points w ∈ s.closedInterior ↔ ∀ i, w i ∈ Set.Icc 0 1 := by
+  refine ⟨fun ⟨w', hw', hw'01, hww'⟩ ↦ ?_, fun h ↦ ⟨w, hw, h, rfl⟩⟩
+  simp_rw [← (affineIndependent_iff_eq_of_fintype_affineCombination_eq k s.points).1
+    s.independent w' w hw' hw hww']
+  exact hw'01
+
+end Simplex
+
+end Affine