The Shapley-Folkman lemma

[YaelDillies]

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]

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]

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 leanprover-community/mathlib4#14427 instead, which is what you should be using from now on.