feat(Geometry/Convex): star-convex sets in a convex space (leanprover-community#40230)

Define `IsStarConvexSet`,a predicate for a set in a `ConvexSpace` to be star-convex at a point. Add a few lemmas about `IsAffineMap` as preliminaries to lemmas about star-convex sets in a module.

The existing `Module`-specific `StarConvex` predicate will be deprecated in a future PR.

Author: YaelDillies

Mathlib.lean

@@ -4550,6 +4550,7 @@ public import Mathlib.Geometry.Convex.ConvexSpace.Module
 public import Mathlib.Geometry.Convex.ConvexSpace.Prod
 public import Mathlib.Geometry.Convex.Hull
 public import Mathlib.Geometry.Convex.Set
+public import Mathlib.Geometry.Convex.Star
 public import Mathlib.Geometry.Diffeology.Basic
 public import Mathlib.Geometry.Euclidean.Altitude
 public import Mathlib.Geometry.Euclidean.Angle.Bisector

Mathlib/Analysis/Convex/Star.lean

@@ -39,13 +39,11 @@ Concretely, the empty set is star-convex at every point.
 
 ## TODO
 
-Balanced sets are star-convex.
-
 The closure of a star-convex set is star-convex.
 
-Star-convex sets are contractible.
-
 A nonempty open star-convex set in `ℝ^n` is diffeomorphic to the entire space.
+
+Replace with `Convexity.IsStarConvexSet`.
 -/
 
 @[expose] public section

Mathlib/Geometry/Convex/ConvexSpace/Module.lean

@@ -5,7 +5,8 @@ Authors: Yaël Dillies
 -/
 module
 
-public import Mathlib.Geometry.Convex.Set
+public import Mathlib.Algebra.Group.Pointwise.Set.Basic
+public import Mathlib.Geometry.Convex.Star
 public import Mathlib.LinearAlgebra.AffineSpace.Combination
 public import Mathlib.LinearAlgebra.AffineSpace.AffineMap
 
@@ -21,12 +22,16 @@ 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.
 -/
 
+open scoped Pointwise
+
 public noncomputable section
 
 namespace Convexity
 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]
+
+section AddCommMonoid
+variable [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [SetLike F M]
+  [AddSubmonoidClass F M] [SMulMemClass F R M] {f g : M → N}
 
 /-- Any semimodule over an ordered semiring is a convex space.
 
@@ -62,7 +67,8 @@ protected lemma IsModuleConvexSpace.ofModule : IsModuleConvexSpace R M where
 instance isModuleConvexSpace_self : IsModuleConvexSpace R R := .ofModule
 
 section IsModuleConvexSpace
-variable [ConvexSpace R M] [IsModuleConvexSpace R M]
+variable [ConvexSpace R M] [IsModuleConvexSpace R M] [ConvexSpace R N] [IsModuleConvexSpace R N]
+  {x y : M} {s t : Set M} {a b : R}
 
 /-- `iConvexComb` in a module can be expressed as a sum. -/
 @[simp]
@@ -76,6 +82,14 @@ 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]
 
+lemma IsAffineMap.map_sum_weights (hf : IsAffineMap R f) (w : StdSimplex R I) (g : I → M) :
+   f (w.weights.sum fun i r ↦ r • g i) = w.weights.sum fun i r ↦ r • f (g i) := by
+  simpa using hf.map_iConvexComb w g
+
+lemma IsAffineMap.map_smul_add_smul (hf : IsAffineMap R f) (ha : 0 ≤ a) (hb : 0 ≤ b)
+    (hab : a + b = 1) (x y : M) : f (a • x + b • y) = a • f x + b • f y := by
+  simpa using hf.map_convexCombPair ha hb hab x y
+
 @[simp] lemma isConvexSet_coe (S : F) : IsConvexSet R (S : Set M) := by
   refine .of_sConvexComb_mem fun w hw ↦ ?_
   rw [sConvexComb_eq_sum]
@@ -96,7 +110,7 @@ lemma subtypeVal_submodule_convexCombPair (S : F) (a b : R) (ha hb hab) (x y : S
 
 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
+instance : IsModuleConvexSpace R (M × N) where
   sConvexComb_eq_sum w := by ext <;> simp [Finsupp.sum, Prod.fst_sum, Prod.snd_sum]
 
 instance {ι : Type*} {M : ι → Type*} [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]
@@ -107,10 +121,42 @@ instance {ι : Type*} {M : ι → Type*} [∀ i, AddCommMonoid (M i)] [∀ i, Mo
 instance {ι : Type*} : IsModuleConvexSpace R (ι →₀ M) where
   sConvexComb_eq_sum w := by ext; simp [Finsupp.sum]
 
+@[to_fun (attr := fun_prop)]
+lemma IsAffineMap.add (hf : IsAffineMap R f) (hg : IsAffineMap R g) : IsAffineMap R (f + g) where
+  map_sConvexComb w := by
+    simp [hf.map_sum_weights, hg.map_sum_weights, Finsupp.sum_mapDomain_index, add_smul]
+
+lemma IsStarConvexSet.add (hs : IsStarConvexSet R x s) (ht : IsStarConvexSet R y t) :
+    IsStarConvexSet R (x + y) (s + t) := by
+  rw [← Set.add_image_prod]; exact (hs.prod ht).image (by fun_prop)
+
 end IsModuleConvexSpace
 
 variable (R I) in
 lemma StdSimplex.isAffineMap_weights : IsAffineMap R (weights (R := R) (M := I)) where
   map_sConvexComb s := by simp [sConvexComb_eq_sum, Finsupp.sum_mapDomain_index, add_smul]
 
+end AddCommMonoid
+
+section AddCommGroup
+variable [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
+  [ConvexSpace R M] [IsModuleConvexSpace R M] [ConvexSpace R N] [IsModuleConvexSpace R N]
+  {x y : M} {s t : Set M} {f g : M → N}
+
+@[to_fun (attr := fun_prop)]
+lemma IsAffineMap.neg (hf : IsAffineMap R f) : IsAffineMap R (-f) where
+  map_sConvexComb w := by simp [hf.map_sum_weights, Finsupp.sum_mapDomain_index, add_smul]
+
+@[to_fun (attr := fun_prop)]
+lemma IsAffineMap.sub (hf : IsAffineMap R f) (hg : IsAffineMap R g) : IsAffineMap R (f - g) := by
+  simpa [sub_eq_add_neg] using hf.add hg.neg
+
+lemma IsStarConvexSet.neg (hs : IsStarConvexSet R x s) : IsStarConvexSet R (-x) (-s) := by
+  rw [← Set.image_neg_eq_neg]; exact hs.image (by fun_prop)
+
+lemma IsStarConvexSet.sub (hs : IsStarConvexSet R x s) (ht : IsStarConvexSet R y t) :
+    IsStarConvexSet R (x - y) (s - t) := by
+  rw [← Set.sub_image_prod]; exact (hs.prod ht).image (by fun_prop)
+
+end AddCommGroup
 end Convexity

Mathlib/Geometry/Convex/Star.lean

@@ -0,0 +1,120 @@
+/-
+Copyright (c) 2026 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+module
+
+public import Mathlib.Geometry.Convex.Set
+
+/-!
+# Star-convex sets
+
+This file defines star-convex sets in a convex space.
+
+A set is star-convex at `x` if every segment from `x` to a point in the set is contained in the set.
+
+This is the prototypical example of a contractible set in homotopy theory (by scaling every point
+towards `x`), but has wider uses.
+
+Note that this has nothing to do with star rings, `Star` and co.
+
+## Implementation notes
+
+Instead of saying that a set is star-convex, we say a set is star-convex *at a point*. This has the
+advantage of allowing us to talk about convexity as being "everywhere star-convexity" and of making
+the union of star-convex sets be star-convex.
+
+Incidentally, this choice means we don't need to assume a set is nonempty for it to be star-convex.
+Concretely, the empty set is star-convex at every point.
+-/
+
+open Finsupp Set
+
+public section
+
+namespace Convexity
+variable {R X Y : Type*} {ι : Sort*} {κ : ι → Sort*}
+
+section Semiring
+variable [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] [ConvexSpace R Y]
+  {f : X → Y} {w : StdSimplex R X} {x : X} {s t : Set X} {y : X}
+
+variable (R x s) in
+/-- A set `s` is star-convex at a point `x` if every segment from `x` to a point in `s` is
+contained in `s`.
+
+TODO: Replace `StarConvex` with this predicate. -/
+@[expose]
+def IsStarConvexSet : Prop :=
+  ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : R⦄ ha hb hab, convexCombPair a b ha hb hab x y ∈ s
+
+@[simp] protected lemma IsStarConvexSet.empty : IsStarConvexSet R x ∅ := by simp [IsStarConvexSet]
+
+@[simp]
+protected lemma IsStarConvexSet.univ : IsStarConvexSet R x .univ := by simp [IsStarConvexSet]
+
+@[simp] protected lemma IsStarConvexSet.singleton : IsStarConvexSet R x {x} := by
+  simp [IsStarConvexSet]
+
+@[grind ←]
+protected lemma IsStarConvexSet.inter (hs : IsStarConvexSet R x s) (ht : IsStarConvexSet R x t) :
+    IsStarConvexSet R x (s ∩ t) := by simp +contextual [IsStarConvexSet, hs _, ht _]
+
+@[grind ←]
+protected lemma IsStarConvexSet.union (hs : IsStarConvexSet R x s) (ht : IsStarConvexSet R x t) :
+    IsStarConvexSet R x (s ∪ t) := by simp +contextual [IsStarConvexSet, hs _, ht _, or_imp]
+
+@[grind ←]
+protected lemma IsStarConvexSet.sInter {S : Set (Set X)} (hS : ∀ s ∈ S, IsStarConvexSet R x s) :
+    IsStarConvexSet R x (⋂₀ S) := by simp +contextual [IsStarConvexSet, hS _ _ _]
+
+@[grind ←]
+protected lemma IsStarConvexSet.iInter {s : ι → Set X} (hs : ∀ i, IsStarConvexSet R x (s i)) :
+    IsStarConvexSet R x (⋂ i, s i) := by simp +contextual [IsStarConvexSet, hs _ _]
+
+lemma IsStarConvexSet.iInter₂ {s : ∀ i, κ i → Set X} (h : ∀ i j, IsStarConvexSet R x (s i j)) :
+    IsStarConvexSet R x (⋂ i, ⋂ j, s i j) := .iInter fun i ↦ .iInter <| h i
+
+@[grind ←]
+protected lemma IsStarConvexSet.sUnion {S : Set (Set X)} (hS : ∀ s ∈ S, IsStarConvexSet R x s) :
+    IsStarConvexSet R x (⋃₀ S) := by
+  rintro y ⟨s, hs, hy⟩ a ha b hb hab; exact ⟨s, hs, hS _ hs hy _ ..⟩
+
+@[grind ←]
+protected lemma IsStarConvexSet.iUnion {s : ι → Set X} (hs : ∀ i, IsStarConvexSet R x (s i)) :
+    IsStarConvexSet R x (⋃ i, s i) := .sUnion <| by simpa
+
+protected lemma IsStarConvexSet.iUnion₂ {s : ∀ i, κ i → Set X}
+    (h : ∀ i j, IsStarConvexSet R x (s i j)) : IsStarConvexSet R x (⋃ i, ⋃ j, s i j) :=
+  .iUnion fun i ↦ .iUnion <| h i
+
+lemma IsConvexSet.isStarConvexSet (hs : IsConvexSet R s) (hx : x ∈ s) : IsStarConvexSet R x s :=
+  fun _y hy _a _b _ha _hb _hab ↦ hs.convexCombPair_mem hx hy ..
+
+lemma IsStarConvexSet.mem (hs : IsStarConvexSet R x s) (hs₀ : s.Nonempty) : x ∈ s := by
+  obtain ⟨y, hy⟩ := hs₀; simpa using hs hy zero_le_one le_rfl (add_zero _)
+
+@[grind ←]
+protected lemma IsStarConvexSet.preimage {s : Set Y} (hf : IsAffineMap R f)
+    (hs : IsStarConvexSet R (f x) s) : IsStarConvexSet R x (f ⁻¹' s) :=
+  fun y hy a b ha hb hab ↦ by simpa [mem_preimage, hf.map_convexCombPair] using hs hy _ ..
+
+@[grind <=]
+protected lemma IsStarConvexSet.image (hf : IsAffineMap R f) (hs : IsStarConvexSet R x s) :
+    IsStarConvexSet R (f x) (f '' s) := by
+  rintro _ ⟨y, hy, rfl⟩ a b ha hb hab; exact ⟨_, hs hy _ .., hf.map_convexCombPair ..⟩
+
+@[grind ←]
+protected lemma IsStarConvexSet.prod {t : Set Y} {y : Y} (hs : IsStarConvexSet R x s)
+    (ht : IsStarConvexSet R y t) : IsStarConvexSet R (x, y) (s ×ˢ t) := by
+  rintro ⟨w, z⟩ ⟨hw, hz⟩ a b ha hb hab; exact ⟨by simpa using hs hw _ .., by simpa using ht hz _ ..⟩
+
+@[grind ←]
+protected lemma IsStarConvexSet.pi {ι : Type*} {X : ι → Type*} [∀ i, ConvexSpace R (X i)]
+    {s : Set ι} {x : ∀ i, X i} {t : ∀ i, Set (X i)} (ht : ∀ i ∈ s, IsStarConvexSet R (x i) (t i)) :
+    IsStarConvexSet R x (s.pi t) :=
+  fun y hy a b ha hb hab i hi ↦ by simpa using ht _ hi (hy _ hi) _ ..
+
+end Semiring
+end Convexity