leanprover-community/mathlib4

The Shapley-Folkman lemma

Ouverte

#14 427 ouverte le 4 juil. 2024

Voir sur GitHubGuide contributeur
 (12 commentaires) (2 réactions) (1 personne assignée)Lean (1 601 forks)github user discovery
good first issuet-analysis

Métriques du dépôt

Stars
 (3 885 étoiles)
Métriques de merge PR
 (Aucune PR mergée en 30 j)

Description

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

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

This issue existed in mathlib3 as https://github.com/leanprover-community/mathlib/issues/18135.

Guide contributeur

Direction de recherche
Étudiez les preuves des théorèmes de Carathéodory et Radon, puis adaptez l'approche en utilisant l'analyse convexe pour formaliser le lemme de Shapley Folkman.
Stack technique
Aucun
Domaine
Aucun
Type d'issue
Fonctionnalité
DifficultéDifficulté estimée pour un nouveau contributeur, de 1 pour un très petit changement à 5 pour un travail expert.
3
Temps estiméFourchette de temps approximative pour investiguer, implémenter, tester et préparer une pull request.
1-3 heures
Statut d'activitéDisponibilité apparente de l'issue : fraîche, active, ancienne, bloquée ou en attente d'un mainteneur.
Active
ClartéClarté avec laquelle l'issue explique le changement attendu, les critères d'acceptation et la prochaine étape.
Claire
Prérequis
Lean
Accessibilité débutantScore de 1 à 100 estimant l'accessibilité de cette issue pour un premier contributeur.
70