[Merged by Bors] - feat(Geometry/Convex): star-convex sets in a convex space

[YaelDillies]

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.

---

[github-actions]

PR summary 65ca858de0

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.Convex.MetricSpace Mathlib.Geometry.Convex.ConvexSpace.Module	1
Mathlib.Geometry.Convex.Star (new file)	876

---

Declarations diff (regex)

+ IsAffineMap.add
+ IsAffineMap.map_smul_add_smul
+ IsAffineMap.map_sum_weights
+ IsAffineMap.neg
+ IsAffineMap.sub
+ IsConvexSet.isStarConvexSet
+ IsStarConvexSet
+ IsStarConvexSet.add
+ IsStarConvexSet.empty
+ IsStarConvexSet.iInter
+ IsStarConvexSet.iInter₂
+ IsStarConvexSet.iUnion
+ IsStarConvexSet.iUnion₂
+ IsStarConvexSet.image
+ IsStarConvexSet.inter
+ IsStarConvexSet.mem
+ IsStarConvexSet.neg
+ IsStarConvexSet.pi
+ IsStarConvexSet.preimage
+ IsStarConvexSet.prod
+ IsStarConvexSet.sInter
+ IsStarConvexSet.sUnion
+ IsStarConvexSet.singleton
+ IsStarConvexSet.sub
+ IsStarConvexSet.union
+ IsStarConvexSet.univ
+ instance : IsModuleConvexSpace R (M × N)
- instance [ConvexSpace R N] [IsModuleConvexSpace R N] : IsModuleConvexSpace R (M × N)

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 65ca858).

• +29 new declarations
• −0 removed declarations

+Convexity.IsAffineMap.add
+Convexity.IsAffineMap.fun_add
+Convexity.IsAffineMap.fun_neg
+Convexity.IsAffineMap.fun_sub
+Convexity.IsAffineMap.map_smul_add_smul
+Convexity.IsAffineMap.map_sum_weights
+Convexity.IsAffineMap.neg
+Convexity.IsAffineMap.sub
+Convexity.IsConvexSet.isStarConvexSet
+Convexity.IsStarConvexSet
+Convexity.IsStarConvexSet.add
+Convexity.IsStarConvexSet.empty
+Convexity.IsStarConvexSet.iInter
+Convexity.IsStarConvexSet.iInter₂
+Convexity.IsStarConvexSet.iUnion
+Convexity.IsStarConvexSet.iUnion₂
+Convexity.IsStarConvexSet.image
+Convexity.IsStarConvexSet.inter
+Convexity.IsStarConvexSet.mem
+Convexity.IsStarConvexSet.neg
+Convexity.IsStarConvexSet.pi
+Convexity.IsStarConvexSet.preimage
+Convexity.IsStarConvexSet.prod
+Convexity.IsStarConvexSet.sInter
+Convexity.IsStarConvexSet.sUnion
+Convexity.IsStarConvexSet.singleton
+Convexity.IsStarConvexSet.sub
+Convexity.IsStarConvexSet.union
+Convexity.IsStarConvexSet.univ

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 65ca858de0
Reference commit bb482f116b

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[b-mehta]

We already have StarConvex but I'm guessing this is in greater generality? It would be nice to

• mention this in the docstring, and explain why we have two (perhaps this is temporary)
• have some link between them

[b-mehta]

Looks generally nice!

[b-mehta]

It looks like your new changes do a bunch of things unrelated to star-convexity. And these changes aren't in the PR description.
Was this accidental?

[YaelDillies]

I have added more lemmas about star-convexity I realised I needed in order to deprecate the StarConvex API, as well as required preliminary lemmas

[b-mehta]

I have added more lemmas about star-convexity I realised I needed in order to deprecate the StarConvex API, as well as required preliminary lemmas

I'm not sure I follow. Lemmas like IsAffineMap.add aren't about StarConvex, nor is it required for any of the other things in this PR, so it seems to fit into neither of these categories. In addition, these unrelated changes aren't in your PR description, and both points of my comment above are still outstanding. So I will put this back to awaiting-author, until these three are addressed!

[YaelDillies]

IsAffineMap.add is required for the fun_prop call here to succeed:
https://github.com/leanprover-community/mathlib4/pull/40230/files#diff-1db65ad9421d04dd0844a369b7d7533626ce3e5c40c824e7d030190a3e2fde33R131

[YaelDillies]

• have some link between them

This will wait until #40235 if you don't mind.

[b-mehta]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job
• ci (staging) / Build
• ci (staging) / Lint style