feat(Geometry/Convex): convex sets in a ConvexSpace (leanprover-community#38905)

Define convex sets in a convex space.

To allow full generality on the coefficients, for `s` to be convex we require that all finitary
convex combinations of points of `s` lie in `s`, instead of merely binary ones as is customary.

Since its body is an implementation detail, the predicate `IsConvexSet` is unexposed.

`Convex` will be deprecated to `IsConvexSet` in a later PR.

[Zulip](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/Convexity.20refactor/with/593967042)

Author: YaelDillies

Mathlib.lean

@@ -4522,6 +4522,7 @@ public import Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
 public import Mathlib.Geometry.Convex.ConvexSpace.Defs
 public import Mathlib.Geometry.Convex.ConvexSpace.Module
 public import Mathlib.Geometry.Convex.ConvexSpace.Prod
+public import Mathlib.Geometry.Convex.Set
 public import Mathlib.Geometry.Diffeology.Basic
 public import Mathlib.Geometry.Euclidean.Altitude
 public import Mathlib.Geometry.Euclidean.Angle.Bisector

Mathlib/Algebra/BigOperators/Finsupp/Basic.lean

@@ -78,6 +78,11 @@ theorem prod_mapRange_index {f : M → M'} {hf : f 0 = 0} {g : α →₀ M} {h :
     (h0 : ∀ a, h a 0 = 1) : (mapRange f hf g).prod h = g.prod fun a b => h a (f b) :=
   Finset.prod_subset support_mapRange fun _ _ H => by rw [notMem_support_iff.1 H, h0]
 
+@[to_additive (attr := simp)]
+lemma prod_onFinset (s : Finset α) (f : α → M) (hf) (g : α → M → N) (hg : ∀ i ∈ s, g i 0 = 1) :
+    (onFinset s f hf).prod g = ∏ a ∈ s, g a (f a) :=
+  prod_of_support_subset _ support_onFinset_subset _ hg
+
 @[to_additive (attr := simp)]
 theorem prod_zero_index {h : α → M → N} : (0 : α →₀ M).prod h = 1 :=
   rfl

Mathlib/Analysis/Convex/MetricSpace.lean

@@ -35,6 +35,8 @@ that has little to do with this definition.
 - Equip `StdSimplex` with a topology and show the analogous continuity result for n-ary
   convex combinations.
 - Tidy up the imports with `Mathlib.Geometric.Convex.ConvexSpace.AffineSpace`.
+- Define convex functions with domain a convex space, and redefine `IsConvexDist` as saying that
+  `dist : X × X → ℝ` is convex.
 -/
 
 public section
@@ -256,42 +258,6 @@ lemma continuous_convexCombPair' [BoundedSpace X]
 @[deprecated (since := "2026-05-15")]
 alias continuous_convexComboPair' := continuous_convexCombPair'
 
-variable {R E : Type*} [LinearOrder R] [Field R] [IsStrictOrderedRing R] [AddCommGroup E]
-  [Module R E] [ConvexSpace R E] [IsModuleConvexSpace R E] {S : Set E}
-
-/-- A convex subset of a vector space is a convex space. -/
--- TODO: this should generalize to arbitrary convex space once `Convex` is redefined.
-@[expose, implicit_reducible]
-noncomputable def ConvexSpace.ofConvex (H : Convex R S) : ConvexSpace R S where
-  sConvexComb f :=
-    ⟨sConvexComb (f.map (↑)), by
-    simpa [sConvexComb_eq_sum, StdSimplex.map, Finsupp.sum_mapDomain_index, add_smul] using
-      H.sum_mem (fun _ _ ↦ f.nonneg _) f.total fun i _ ↦ i.2⟩
-  assoc f := by
-    simp [sConvexComb_eq_sum, StdSimplex.map, Finsupp.sum_mapDomain_index, add_smul,
-      StdSimplex.join, Finsupp.sum_sum_index, Finsupp.sum_smul_index, mul_smul, Finsupp.smul_sum]
-  sConvexComb_single x := by simp [sConvexComb_eq_sum, ← StdSimplex.mk_single, StdSimplex.map]
-
-lemma isAffineMap_coe (S : Set E) (H : Convex R S) :
-    letI : ConvexSpace R S := .ofConvex H
-    IsAffineMap R ((↑) : S → E) :=
-  letI : ConvexSpace R S := .ofConvex H
-  ⟨fun _ ↦ rfl⟩
-
-@[simp]
-lemma ConvexSpace.ofConvex.coe_sConvexComb (S : Set E) (H : Convex R S) (f : StdSimplex R S) :
-    letI : ConvexSpace R S := .ofConvex H
-    (↑f.sConvexComb : E) = (f.map (↑)).sConvexComb :=
-  rfl
-
-@[simp]
-lemma ConvexSpace.ofConvex.coe_iConvexComb (S : Set E) (H : Convex R S) (f : StdSimplex R I)
-     (g : I → S) :
-    letI : ConvexSpace R S := .ofConvex H
-    (↑(f.iConvexComb g) : E) = f.iConvexComb fun x ↦ ↑(g x) :=
-  letI : ConvexSpace R S := .ofConvex H
-  (isAffineMap_coe S H).map_iConvexComb f g
-
 attribute [local instance] AddTorsor.toConvexSpace in
 instance (priority := low) {V P : Type*}
     [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] :
@@ -307,14 +273,17 @@ instance (priority := low) {V P : Type*}
     grw [Finsupp.sum, Finsupp.sum, norm_sum_le]
     simp [norm_smul, abs_eq_self.mpr (f.nonneg _)]
 
-instance IsConvexDist.of_convex {E : Type*} [NormedAddCommGroup E]
-    [NormedSpace ℝ E] [ConvexSpace ℝ E] [IsModuleConvexSpace ℝ E] [IsConvexDist E] {S : Set E}
-    (H : Convex ℝ S) :
-    letI : ConvexSpace ℝ S := .ofConvex H
-    IsConvexDist S := by
-  letI : ConvexSpace ℝ S := .ofConvex H
+instance IsConvexDist.subtype (s : Set X) (hs : IsConvexSet ℝ s) :
+    letI : ConvexSpace ℝ s := .subtype s hs
+    IsConvexDist s := by
+  letI : ConvexSpace ℝ s := .subtype s hs
   refine ⟨fun f ↦ ?_⟩
-  convert dist_iConvexComb_fst_snd_le (X := E) (f.map fun x ↦ (x.1, x.2)) <;>
-    simp [Subtype.dist_eq, Finsupp.sum_mapDomain_index, add_mul, add_smul]
+  convert dist_iConvexComb_fst_snd_le (X := X) (f.map fun x ↦ (x.1, x.2)) <;>
+    simp [Subtype.dist_eq, Finsupp.sum_mapDomain_index, add_mul]
+
+instance IsConvexDist.submodule {F M : Type*} [AddCommGroup M] [MetricSpace M]
+    [Module ℝ M] [ConvexSpace ℝ M] [IsModuleConvexSpace ℝ M] [IsConvexDist M]
+    [SetLike F M] [AddSubmonoidClass F M] [SMulMemClass F ℝ M] {S : F} :
+    IsConvexDist S := .subtype _ _
 
 end Convexity

Mathlib/Data/Finsupp/Basic.lean

@@ -276,10 +276,14 @@ def mapDomain (f : α → β) (v : α →₀ M) : β →₀ M :=
   · intro _
     rw [single_zero, coe_zero, Pi.zero_apply]
 
+lemma mapDomain_of_not_mem_image_support {f : α → β} {x : α →₀ M} {b : β}
+    (hb : b ∉ f '' x.support) : mapDomain f x b = 0 := by
+  rw [mapDomain, sum_apply, sum, Finset.sum_eq_zero]
+  exact fun a ha ↦ single_eq_of_ne fun eq => hb <| eq ▸ Set.mem_image_of_mem _ ha
+
 theorem mapDomain_notin_range {f : α → β} (x : α →₀ M) (a : β) (h : a ∉ Set.range f) :
-    mapDomain f x a = 0 := by
-  rw [mapDomain, sum_apply, sum]
-  exact Finset.sum_eq_zero fun a' _ => single_eq_of_ne fun eq => h <| eq ▸ Set.mem_range_self _
+    mapDomain f x a = 0 :=
+  mapDomain_of_not_mem_image_support <| by grw [Set.image_subset_range]; exact h
 
 @[simp]
 theorem mapDomain_id : mapDomain id v = v :=

Mathlib/Geometry/Convex/ConvexSpace/Defs.lean

@@ -62,6 +62,7 @@ grind_pattern StdSimplex.total => self.weights
 initialize_simps_projections StdSimplex (as_prefix weights)
 
 namespace StdSimplex
+section Semiring
 variable {R : Type u} [PartialOrder R] [Semiring R] {M N P : Type*} {w : StdSimplex R M} {x : M}
 
 @[simp] lemma weights_nonneg {w : StdSimplex R M} (i : M) : 0 ≤ w.weights i := w.nonneg i
@@ -167,6 +168,56 @@ private lemma map_join (f : StdSimplex R (StdSimplex R M)) (g : M → N) :
 @[simp] private lemma join_single (x : StdSimplex R M) : join (.single x) = x := by
   ext; simp [join, ← mk_single]
 
+end Semiring
+
+section Semifield
+variable [Semifield K] [LinearOrder K] [IsStrictOrderedRing K]
+
+private lemma restrict_nonneg_aux {w : StdSimplex K X} {p : X → Prop} [DecidablePred p] :
+    0 ≤ (filter p w.weights).sum fun _x k ↦ k :=
+  sum_nonneg <| by simp [filter_apply, apply_ite]
+
+private lemma restrict_ne_zero_aux {w : StdSimplex K X} {p : X → Prop} [DecidablePred p]
+    (hp : ∃ a, p a ∧ w.weights a ≠ 0) :
+    (filter p w.weights).sum (fun _x k ↦ k) ≠ 0 :=
+  (sum_pos (by simp +contextual [lt_iff_le_and_ne, eq_comm]) <| by simpa [ne_iff, filter_apply]).ne'
+
+/-- Project an element of the standard simplex to a lower-dimensional standard simplex,
+assuming at least one non-zero weight subsists. -/
+def restrict (w : StdSimplex K X) (s : Set X) (hs : ∃ x ∈ s, w.weights x ≠ 0) : StdSimplex K X where
+  weights := open scoped Classical in
+    ((w.weights.filter (· ∈ s)).sum fun x k ↦ k)⁻¹ • w.weights.filter (· ∈ s)
+  nonneg := by
+    classical
+    exact smul_nonneg (inv_nonneg.2 restrict_nonneg_aux) fun _ ↦ by simp [filter_apply, apply_ite]
+  total := by classical simp [sum_smul_index, ← mul_sum, restrict_ne_zero_aux hs]
+
+lemma weights_restrict (w : StdSimplex K X) (s : Set X) (hs) [DecidablePred (· ∈ s)] :
+    (w.restrict s hs).weights =
+      ((w.weights.filter (· ∈ s)).sum fun _x k ↦ k)⁻¹ • w.weights.filter (· ∈ s) := by
+  simp [restrict]; congr
+
+variable [IsDomain K]
+
+@[simp]
+lemma support_weights_restrict (w : StdSimplex K X) (s : Set X) (hs) [DecidablePred (· ∈ s)] :
+    (w.restrict s hs).weights.support = w.weights.support.filter (· ∈ s) := by
+  have : (w.weights.filter (· ∈ s)).sum (fun x k ↦ k) ≠ 0 :=
+    (sum_pos (by simp +contextual [lt_iff_le_and_ne, eq_comm]) <| by
+      simpa [ne_iff, filter_apply]).ne'
+  rw [weights_restrict, support_smul_eq (by convert inv_ne_zero this)]
+  simp
+
+@[simp] lemma restrict_singleton (w : StdSimplex K X) (x : X) (hx) :
+    w.restrict {x} hx = single x := by
+  classical
+  simp only [← support_weights_eq_singleton, support_weights_restrict, Set.mem_singleton_iff]
+  ext
+  simp only [Finset.mem_filter, mem_support_iff, ne_eq, Finset.mem_singleton, and_iff_right_iff_imp]
+  rintro rfl
+  simpa using hx
+
+end Semifield
 end StdSimplex
 
 /--
@@ -240,6 +291,19 @@ lemma map_sConvexComb (s : StdSimplex R (StdSimplex R I)) (f : I → J) :
     s.sConvexComb.map f = (s.map (map f)).sConvexComb :=
   StdSimplex.map_join s f
 
+variable [Semifield K] [LinearOrder K] [IsStrictOrderedRing K]
+
+lemma convexCombPair_restrict_restrict_compl (w : StdSimplex K I) (s : Set I) (hs hs')
+    [DecidablePred (· ∈ s)] :
+    convexCombPair
+      ((w.weights.filter (· ∈ s)).sum fun _x k ↦ k)
+      ((w.weights.filter (· ∉ s)).sum fun _x k ↦ k)
+      (by exact restrict_nonneg_aux) (by exact restrict_nonneg_aux) (by simp)
+      (w.restrict s hs) (w.restrict sᶜ hs') = w := by
+  ext : 1
+  simp only [Set.mem_compl_iff] at hs'
+  simp [weights_restrict, smul_inv_smul₀, restrict_ne_zero_aux, hs, hs']
+
 end StdSimplex
 
 lemma sConvexComb_sConvexComb (f : StdSimplex R (StdSimplex R M)) :
@@ -299,8 +363,8 @@ lemma iConvexComb_id (w : StdSimplex R M) : w.iConvexComb id = w.sConvexComb :=
     w.iConvexComb (fun x ↦ x) = w.sConvexComb := iConvexComb_id _
 
 @[simp] lemma iConvexComb_map (s : StdSimplex R I) (f : I → J) (g : J → M) :
-    (s.map f).iConvexComb g = s.iConvexComb (g ∘ f) := by
-  simp only [iConvexComb, map_comp]
+    (s.map f).iConvexComb g = s.iConvexComb (fun i ↦ g (f i)) := by
+  simp only [iConvexComb, map_map]
 
 @[congr] lemma iConvexComb_congr {w : StdSimplex R I} {f g : I → M}
     (hfg : ∀ i, w.weights i ≠ 0 → f i = g i) :

Mathlib/Geometry/Convex/ConvexSpace/Module.lean

@@ -5,7 +5,7 @@ Authors: Yaël Dillies
 -/
 module
 
-public import Mathlib.Geometry.Convex.ConvexSpace.Prod
+public import Mathlib.Geometry.Convex.Set
 public import Mathlib.LinearAlgebra.AffineSpace.Combination
 public import Mathlib.LinearAlgebra.AffineSpace.AffineMap
 
@@ -21,11 +21,12 @@ This file shows that every module over ordered coefficients is a convex space.
 * `IsModuleConvexSpace`: Predicate for a convex space and module structures to be compatible.
 -/
 
-public section
+public noncomputable section
 
 namespace Convexity
-variable {R M N I : Type*} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R]
-  [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N]
+variable {F R M N I : Type*} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R]
+  [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [SetLike F M]
+  [AddSubmonoidClass F M] [SMulMemClass F R M]
 
 /-- Any semimodule over an ordered semiring is a convex space.
 
@@ -75,6 +76,26 @@ lemma convexCombPair_eq_sum (a b : R) (ha hb hab) (x y : M) :
     convexCombPair a b ha hb hab x y = a • x + b • y := by
   classical simp [convexCombPair, sConvexComb_eq_sum, Finsupp.sum_add_index, add_smul]
 
+@[simp] lemma isConvexSet_coe (S : F) : IsConvexSet R (S : Set M) := by
+  refine .of_sConvexComb_mem fun w hw ↦ ?_
+  rw [sConvexComb_eq_sum]
+  exact AddSubmonoidClass.finsuppSum_mem _ _ _ fun m hm ↦ SMulMemClass.smul_mem _ <| hw <| by simpa
+
+instance (S : F) : ConvexSpace R S := .subtype _ <| isConvexSet_coe _
+
+@[simp]
+lemma subtypeVal_submodule_sConvexComb (S : F) (w : StdSimplex R S) :
+    (w.sConvexComb : M) = w.iConvexComb (↑) := rfl
+
+lemma subtypeVal_submodule_iConvexComb (S : F) (w : StdSimplex R I) (f : I → S) :
+    (↑(w.iConvexComb f) : M) = w.iConvexComb (fun i ↦ (f i).val) := subtypeVal_iConvexComb ..
+
+lemma subtypeVal_submodule_convexCombPair (S : F) (a b : R) (ha hb hab) (x y : S) :
+    (↑(convexCombPair a b ha hb hab x y) : M) = convexCombPair a b ha hb hab x.val y.val :=
+  subtypeVal_convexCombPair ..
+
+instance (S : F) : IsModuleConvexSpace R S where sConvexComb_eq_sum w := by ext; simp [Finsupp.sum]
+
 instance [ConvexSpace R N] [IsModuleConvexSpace R N] : IsModuleConvexSpace R (M × N) where
   sConvexComb_eq_sum w := by ext <;> simp [Finsupp.sum, Prod.fst_sum, Prod.snd_sum]
 

Mathlib/Geometry/Convex/README.md

@@ -8,4 +8,5 @@ See the `Mathlib.Analysis.Convex` folder for the results that need a norm or an
 
 The topics currently covered are:
 * Convex spaces
+* Convex sets
 * Cones