feat(Analysis/Convex/Intrinsic): add product theorems for affine spans and intrinsic interiors (leanprover-community#38551)

Add API for products of affine subspaces and proves product theorems for affine spans and intrinsic interiors.

Co-authored-by: Zichen Wang <imathwy@users.noreply.github.com>

Author: TTony2019

Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

@@ -536,6 +536,10 @@ theorem inter_div_union_subset_union : s₁ ∩ s₂ / (t₁ ∪ t₂) ⊆ s₁
 theorem union_div_inter_subset_union : (s₁ ∪ s₂) / (t₁ ∩ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂ :=
   image2_union_inter_subset_union
 
+@[to_additive (attr := simp) prod_sub_prod_comm]
+lemma prod_div_prod_comm [Div β] (s₁ s₂ : Set α) (t₁ t₂ : Set β) :
+    (s₁ ×ˢ t₁) / (s₂ ×ˢ t₂) = (s₁ / s₂) ×ˢ (t₁ / t₂) := by aesop (add simp mem_div)
+
 end Div
 
 -- TODO: rename `NPow` to `npow` and `ZPow` to `zpow`.

Mathlib/Algebra/Torsor/Basic.lean

@@ -33,6 +33,15 @@ namespace Set
 theorem singleton_sdiv_self (p : P) : ({p} : Set P) /ₛ {p} = {(1 : G)} := by
   rw [Set.singleton_sdiv_singleton, sdiv_self]
 
+@[to_additive (attr := simp)]
+theorem one_mem_sdiv_iff {s t : Set P} : (1 : G) ∈ s /ₛ t ↔ ¬Disjoint s t := by
+  simp [not_disjoint_iff_nonempty_inter, mem_sdiv, Set.Nonempty]
+
+@[to_additive]
+theorem Nonempty.one_mem_sdiv_self {s : Set P} (h : s.Nonempty) : (1 : G) ∈ s /ₛ s :=
+  let ⟨p, hp⟩ := h
+  ⟨p, hp, p, hp, sdiv_self _⟩
+
 end Set
 /-- If dividing two points by the same point produces equal results, those points are equal. -/
 @[to_additive /-- If the same point subtracted from two points produces equal
@@ -160,6 +169,17 @@ theorem mk_sdiv_mk (p₁ p₂ : P) (p₁' p₂' : P') :
 
 end Prod
 
+namespace Set
+
+variable {G G' P P' : Type*} [Group G] [Group G'] [Torsor G P] [Torsor G' P']
+
+@[to_additive prod_vsub_prod_comm]
+theorem prod_sdiv_prod_comm (s₁ s₂ : Set P) (t₁ t₂ : Set P') :
+    (s₁ ×ˢ t₁) /ₛ (s₂ ×ˢ t₂) = (s₁ /ₛ s₂) ×ˢ (t₁ /ₛ t₂) := by
+  aesop (add norm simp [mem_sdiv, mem_prod])
+
+end Set
+
 namespace Pi
 
 universe u v w

Mathlib/Analysis/Convex/Intrinsic.lean

@@ -217,6 +217,16 @@ theorem intrinsicClosure_eq_closure_inter_affineSpan (s : Set P) :
   rw [Subtype.range_coe]
   apply subset_affineSpan
 
+theorem intrinsicInterior_prod_eq [AddCommGroup W] [Module 𝕜 W] [TopologicalSpace Q]
+    [AddTorsor W Q] (s : Set P) (t : Set Q) :
+    intrinsicInterior 𝕜 (s ×ˢ t) = intrinsicInterior 𝕜 s ×ˢ intrinsicInterior 𝕜 t := by
+  let e : affineSpan 𝕜 (s ×ˢ t) ≃ₜ affineSpan 𝕜 s × affineSpan 𝕜 t :=
+    (Homeomorph.setCongr (by simp [affineSpan_prod_eq])).trans (Homeomorph.Set.prod _ _)
+  have : Subtype.val ∘ e.symm = fun p ↦ (p.1, p.2) := rfl
+  have h : ((↑) ⁻¹' (s ×ˢ t) : Set _) = e ⁻¹' (((↑) ⁻¹' s) ×ˢ ((↑) ⁻¹' t)) := rfl
+  simp_rw [intrinsicInterior, h, ← e.preimage_interior, interior_prod_eq, ← e.image_symm,
+    ← image_comp, prod_image_image_eq, this]
+
 section ImageOfHomeomorphAffineSpan
 
 variable [AddCommGroup W] [Module 𝕜 W] [TopologicalSpace Q] [AddTorsor W Q]

Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean

@@ -815,8 +815,77 @@ namespace AffineSubspace
 
 open AffineEquiv
 
-variable {k : Type*} {V : Type*} {P : Type*} [Ring k] [AddCommGroup V] [Module k V]
-variable [AffineSpace V P]
+variable {k V W P Q : Type*} [Ring k] [AddCommGroup V] [Module k V] [AffineSpace V P]
+  [AddCommGroup W] [Module k W] [AffineSpace W Q]
+
+/-- The product of two affine subspaces as an affine subspace. -/
+def prod (s : AffineSubspace k P) (t : AffineSubspace k Q) : AffineSubspace k (P × Q) where
+  carrier := (s : Set P) ×ˢ (t : Set Q)
+  smul_vsub_vadd_mem' c _ _ _ hp₁ hp₂ hp₃ :=
+    ⟨s.smul_vsub_vadd_mem' c hp₁.1 hp₂.1 hp₃.1, t.smul_vsub_vadd_mem' c hp₁.2 hp₂.2 hp₃.2⟩
+
+@[simp]
+theorem coe_prod (s : AffineSubspace k P) (t : AffineSubspace k Q) :
+    (s.prod t : Set (P × Q)) = (s : Set P) ×ˢ (t : Set Q) :=
+  rfl
+
+@[simp]
+theorem mem_prod (s : AffineSubspace k P) (t : AffineSubspace k Q) (x : P × Q) :
+    x ∈ s.prod t ↔ x.1 ∈ s ∧ x.2 ∈ t :=
+  Set.mem_prod
+
+@[gcongr]
+theorem prod_mono {s₁ s₂ : AffineSubspace k P} {t₁ t₂ : AffineSubspace k Q}
+    (hs : s₁ ≤ s₂) (ht : t₁ ≤ t₂) : s₁.prod t₁ ≤ s₂.prod t₂ :=
+  Set.prod_mono hs ht
+
+@[simp]
+theorem prod_top_top : (⊤ : AffineSubspace k P).prod (⊤ : AffineSubspace k Q) = ⊤ := by
+  ext; simp
+
+@[simp]
+theorem prod_bot_right (s : AffineSubspace k P) : s.prod (⊥ : AffineSubspace k Q) = ⊥ := by
+  simp [AffineSubspace.ext_iff]
+
+@[simp]
+theorem prod_bot_left (t : AffineSubspace k P) : (⊥ : AffineSubspace k Q).prod t = ⊥ := by
+  simp [AffineSubspace.ext_iff]
+
+theorem prod_inf_prod (s₁ s₂ : AffineSubspace k P) (t₁ t₂ : AffineSubspace k Q) :
+    s₁.prod t₁ ⊓ s₂.prod t₂ = (s₁ ⊓ s₂).prod (t₁ ⊓ t₂) :=
+  SetLike.coe_injective Set.prod_inter_prod
+
+theorem _root_.vectorSpan_prod_le (s : Set P) (t : Set Q) :
+    vectorSpan k (s ×ˢ t) ≤ (vectorSpan k s).prod (vectorSpan k t) := by
+  simpa [vectorSpan_def, Set.prod_vsub_prod_comm] using Submodule.span_prod_le (s -ᵥ s) (t -ᵥ t)
+
+theorem direction_prod_le (s : AffineSubspace k P) (t : AffineSubspace k Q) :
+    (s.prod t).direction ≤ s.direction.prod t.direction := by
+  simpa [direction_eq_vectorSpan, coe_prod] using vectorSpan_prod_le (s : Set P) (t : Set Q)
+
+theorem _root_.vectorSpan_prod_eq {s : Set P} {t : Set Q} (hs : s.Nonempty) (ht : t.Nonempty) :
+    vectorSpan k (s ×ˢ t) = (vectorSpan k s).prod (vectorSpan k t) := by
+  rw [vectorSpan_def, Set.prod_vsub_prod_comm]
+  exact Submodule.span_prod_eq k hs.zero_mem_vsub_self ht.zero_mem_vsub_self
+
+theorem direction_prod_eq {s : AffineSubspace k P} {t : AffineSubspace k Q}
+    (hs : s ≠ ⊥) (ht : t ≠ ⊥) :
+    (s.prod t).direction = s.direction.prod t.direction := by
+  simp [direction_eq_vectorSpan, vectorSpan_prod_eq, nonempty_iff_ne_bot, ht, hs]
+
+theorem _root_.affineSpan_prod_eq (s : Set P) (t : Set Q) :
+    affineSpan k (s ×ˢ t) = (affineSpan k s).prod (affineSpan k t) := by
+  rcases s.eq_empty_or_nonempty with rfl | hs
+  · simp
+  rcases t.eq_empty_or_nonempty with rfl | ht
+  · simp
+  apply AffineSubspace.ext_of_direction_eq
+  · simp [direction_prod_eq, Set.nonempty_iff_ne_empty.mp, hs, ht, direction_affineSpan,
+      vectorSpan_prod_eq]
+  · obtain ⟨x, hx⟩ := hs
+    obtain ⟨y, hy⟩ := ht
+    use ⟨x, y⟩
+    simp [mem_affineSpan, hx, hy]
 
 /-- Two affine subspaces are parallel if one is related to the other by adding the same vector
 to all points. -/

Mathlib/LinearAlgebra/Prod.lean

@@ -640,6 +640,13 @@ theorem prod_eq_top_iff {p₁ : Submodule R M} {p₂ : Submodule R M₂} :
     p₁.prod p₂ = ⊤ ↔ p₁ = ⊤ ∧ p₂ = ⊤ := by
   simp only [eq_top_iff, le_prod_iff, map_top, range_fst, range_snd]
 
+variable {M M₂} in
+theorem span_prod_eq {s : Set M} {t : Set M₂} (hs : 0 ∈ s) (ht : 0 ∈ t) :
+    span R (s ×ˢ t) = (span R s).prod (span R t) := by
+  refine le_antisymm (span_prod_le s t) ?_
+  simp [Submodule.prod_le_iff, map_span]
+  grind [span_mono]
+
 end Submodule
 
 namespace LinearEquiv