search

leanprover-community / mathlib3

Lean 3's obsolete mathematical components library: please use mathlib4
https://leanprover-community.github.io/lean3
Apache License 2.0
1.67k stars 299 forks source link

The Shapley-Folkman lemma #18135

Closed YaelDillies closed 2 months ago

YaelDillies commented 1 year ago

The Shapley-Folkman lemma is a convex analysis result standard in the economics literature. In contrast, it is basically unheard of in the mathematics one.

The proof is elementary, and very similar to the proof of Carathéodory's and Radon's theorems, which should serve as inspiration.

A secondary goal could be Helly's theorem, whose proof is again very similar to the previous.

ndcroos commented 2 months ago

Hi, I'd like to work on this as my first project. I've checked https://leanprover-community.github.io/lean3/undergrad.html and the pull requests list, and it seems like there has been no work done on the Shapley-Folkman lemma yet.

YaelDillies commented 2 months ago

Please do! I am not aware of anyone working on Shapley-Folkman right now, but just to be sure you should ask @vasnesterov who recently formalised the closely related Radon and Helly theorems.

Also note that mathlib is now ported to Lean 4, so you should be looking at https://leanprover-community.github.io/undergrad.html (well actually not, because Shapley-Folkman wouldn't be there anyway) and https://github.com/leanprover-community/mathlib4/pulls instead. As such, I am closing this issue. I have opened https://github.com/leanprover-community/mathlib4/issues/14427 instead, which is what you should be using from now on.