feat: Intersection of convex hulls is convex hull of intersection (#9203

)

when everything is affine independent. Also a related affine span lemma.

From LeanCamCombi

Mathlib/Analysis/Convex/Combination.lean

@@ -375,6 +375,14 @@ theorem Finset.mem_convexHull {s : Finset E} {x : E} : x ∈ convexHull R (s : S
   rw [Finset.convexHull_eq, Set.mem_setOf_eq]
 #align finset.mem_convex_hull Finset.mem_convexHull
 
+/-- This is a version of `Finset.mem_convexHull` stated without `Finset.centerMass`. -/
+lemma Finset.mem_convexHull' {s : Finset E} {x : E} :
+    x ∈ convexHull R (s : Set E) ↔
+      ∃ w : E → R, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y in s, w y = 1 ∧ ∑ y in s, w y • y = x := by
+  rw [mem_convexHull]
+  refine exists_congr fun w ↦ and_congr_right' $ and_congr_right fun hw ↦ ?_
+  simp_rw [centerMass_eq_of_sum_1 _ _ hw, id_eq]
+
 theorem Set.Finite.convexHull_eq {s : Set E} (hs : s.Finite) : convexHull R s =
     { x : E | ∃ w : E → R, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y in hs.toFinset, w y = 1 ∧
       hs.toFinset.centerMass w id = x } := by
@@ -549,3 +557,37 @@ theorem AffineBasis.convexHull_eq_nonneg_coord {ι : Type*} (b : AffineBasis ι
     rw [b.coord_apply_combination_of_mem hi hw₁] at hx
     exact hx
 #align affine_basis.convex_hull_eq_nonneg_coord AffineBasis.convexHull_eq_nonneg_coord
+
+variable {s t t₁ t₂ : Finset E}
+
+/-- Two simplices glue nicely if the union of their vertices is affine independent. -/
+lemma AffineIndependent.convexHull_inter (hs : AffineIndependent R ((↑) : s → E))
+    (ht₁ : t₁ ⊆ s) (ht₂ : t₂ ⊆ s) :
+    convexHull R (t₁ ∩ t₂ : Set E) = convexHull R t₁ ∩ convexHull R t₂ := by
+  refine (Set.subset_inter (convexHull_mono inf_le_left) $
+    convexHull_mono inf_le_right).antisymm ?_
+  simp_rw [Set.subset_def, mem_inter_iff, Set.inf_eq_inter, ← coe_inter, mem_convexHull']
+  rintro x ⟨⟨w₁, h₁w₁, h₂w₁, h₃w₁⟩, w₂, -, h₂w₂, h₃w₂⟩
+  let w (x : E) : R := (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
+  have h₁w : ∑ i in s, w i = 0 := by simp [Finset.inter_eq_right.2, *]
+  replace hs := hs.eq_zero_of_sum_eq_zero_subtype h₁w $ by
+    simp only [sub_smul, zero_smul, ite_smul, Finset.sum_sub_distrib, ← Finset.sum_filter, h₃w₁,
+      Finset.filter_mem_eq_inter, Finset.inter_eq_right.2 ht₁, Finset.inter_eq_right.2 ht₂, h₃w₂,
+      sub_self]
+  have ht (x) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂) : w₁ x = 0 := by
+    simpa [hx₁, hx₂] using hs _ (ht₁ hx₁)
+  refine ⟨w₁, ?_, ?_, ?_⟩
+  · simp only [and_imp, Finset.mem_inter]
+    exact fun y hy₁ _ ↦ h₁w₁ y hy₁
+  all_goals
+  · rwa [sum_subset $ inter_subset_left _ _]
+    rintro x
+    simp_intro hx₁ hx₂
+    simp [ht x hx₁ hx₂]
+
+/-- Two simplices glue nicely if the union of their vertices is affine independent.
+
+Note that `AffineIndependent.convexHull_inter` should be more versatile in most use cases. -/
+lemma AffineIndependent.convexHull_inter' (hs : AffineIndependent R ((↑) : ↑(t₁ ∪ t₂) → E)) :
+    convexHull R (t₁ ∩ t₂ : Set E) = convexHull R t₁ ∩ convexHull R t₂ :=
+  hs.convexHull_inter (subset_union_left _ _) (subset_union_right _ _)

Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean

@@ -125,6 +125,13 @@ theorem AffineIndependent.finrank_vectorSpan [Fintype ι] {p : ι → P} (hi : A
   exact hi.finrank_vectorSpan_image_finset hc
 #align affine_independent.finrank_vector_span AffineIndependent.finrank_vectorSpan
 
+/-- The `vectorSpan` of a finite affinely independent family has dimension one less than its
+cardinality. -/
+lemma AffineIndependent.finrank_vectorSpan_add_one [Fintype ι] [Nonempty ι] {p : ι → P}
+    (hi : AffineIndependent k p) : finrank k (vectorSpan k (Set.range p)) + 1 = Fintype.card ι := by
+  rw [hi.finrank_vectorSpan (tsub_add_cancel_of_le _).symm, tsub_add_cancel_of_le] <;>
+    exact Fintype.card_pos
+
 /-- The `vectorSpan` of a finite affinely independent family whose
 cardinality is one more than that of the finite-dimensional space is
 `⊤`. -/
@@ -162,6 +169,12 @@ theorem finrank_vectorSpan_range_le [Fintype ι] (p : ι → P) {n : ℕ} (hc :
   exact finrank_vectorSpan_image_finset_le _ _ _ hc
 #align finrank_vector_span_range_le finrank_vectorSpan_range_le
 
+/-- The `vectorSpan` of an indexed family of `n + 1` points has dimension at most `n`. -/
+lemma finrank_vectorSpan_range_add_one_le [Fintype ι] [Nonempty ι] (p : ι → P) :
+    finrank k (vectorSpan k (Set.range p)) + 1 ≤ Fintype.card ι :=
+  (le_tsub_iff_right $ Nat.succ_le_iff.2 Fintype.card_pos).1 $ finrank_vectorSpan_range_le _ _
+    (tsub_add_cancel_of_le $ Nat.succ_le_iff.2 Fintype.card_pos).symm
+
 /-- `n + 1` points are affinely independent if and only if their
 `vectorSpan` has dimension `n`. -/
 theorem affineIndependent_iff_finrank_vectorSpan_eq [Fintype ι] (p : ι → P) {n : ℕ}
@@ -217,6 +230,46 @@ lemma AffineIndependent.card_le_finrank_succ [Fintype ι] {p : ι → P} (hp : A
   exact (affineIndependent_iff_le_finrank_vectorSpan _ _
     (tsub_add_cancel_of_le <| Nat.one_le_iff_ne_zero.2 Fintype.card_ne_zero).symm).1 hp
 
+open Finset in
+/-- If an affine independent finset is contained in the affine span of another finset, then its
+cardinality is at most the cardinality of that finset. -/
+lemma AffineIndependent.card_le_card_of_subset_affineSpan {s t : Finset V}
+    (hs : AffineIndependent k ((↑) : s → V)) (hst : (s : Set V) ⊆ affineSpan k (t : Set V)) :
+    s.card ≤ t.card := by
+  obtain rfl | hs' := s.eq_empty_or_nonempty
+  · simp
+  obtain rfl | ht' := t.eq_empty_or_nonempty
+  · simpa [Set.subset_empty_iff] using hst
+  have := hs'.to_subtype
+  have := ht'.to_set.to_subtype
+  have direction_le := AffineSubspace.direction_le (affineSpan_mono k hst)
+  rw [AffineSubspace.affineSpan_coe, direction_affineSpan, direction_affineSpan,
+    ← @Subtype.range_coe _ (s : Set V), ← @Subtype.range_coe _ (t : Set V)] at direction_le
+  have finrank_le := add_le_add_right (Submodule.finrank_le_finrank_of_le direction_le) 1
+  -- We use `erw` to elide the difference between `↥s` and `↥(s : Set V)}`
+  erw [hs.finrank_vectorSpan_add_one] at finrank_le
+  simpa using finrank_le.trans <| finrank_vectorSpan_range_add_one_le _ _
+
+open Finset in
+/-- If the affine span of an affine independent finset is strictly contained in the affine span of
+another finset, then its cardinality is strictly less than the cardinality of that finset. -/
+lemma AffineIndependent.card_lt_card_of_affineSpan_lt_affineSpan {s t : Finset V}
+    (hs : AffineIndependent k ((↑) : s → V))
+    (hst : affineSpan k (s : Set V) < affineSpan k (t : Set V)) : s.card < t.card := by
+  obtain rfl | hs' := s.eq_empty_or_nonempty
+  · simpa [card_pos] using hst
+  obtain rfl | ht' := t.eq_empty_or_nonempty
+  · simp [Set.subset_empty_iff] at hst
+  have := hs'.to_subtype
+  have := ht'.to_set.to_subtype
+  have dir_lt := AffineSubspace.direction_lt_of_nonempty (k := k) hst $ hs'.to_set.affineSpan k
+  rw [direction_affineSpan, direction_affineSpan,
+    ← @Subtype.range_coe _ (s : Set V), ← @Subtype.range_coe _ (t : Set V)] at dir_lt
+  have finrank_lt := add_lt_add_right (Submodule.finrank_lt_finrank_of_lt dir_lt) 1
+  -- We use `erw` to elide the difference between `↥s` and `↥(s : Set V)}`
+  erw [hs.finrank_vectorSpan_add_one] at finrank_lt
+  simpa using finrank_lt.trans_le <| finrank_vectorSpan_range_add_one_le _ _
+
 /-- If the `vectorSpan` of a finite subset of an affinely independent
 family lies in a submodule with dimension one less than its
 cardinality, it equals that submodule. -/