leanprover-community/mathlib4

The Shapley-Folkman lemma

Aperta

#14.427 aperta il 4 lug 2024

Vedi su GitHubGuida contributor
 (11 commenti) (2 reazioni) (1 assegnatario)Lean (1592 fork)github user discovery
good first issuet-analysis

Metriche repository

Star
 (3869 stelle)
Metriche merge PR
 (Nessuna PR mergiata in 30 g)

Descrizione

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.

Guida contributor

Direzione di ricerca
Studia le dimostrazioni dei teoremi di Carathéodory e Radon, quindi adatta l'approccio usando l'analisi convessa per formalizzare il lemma di Shapley Folkman.
Tech stack
Nessuno
Dominio
Nessuno
Tipo issue
Funzionalità
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
3
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
1-3 ore
Stato attivitàQuanto è probabile che la issue sia ancora attiva e reviewable.
Attiva
ChiarezzaQuanto chiaramente la issue descrive problema, scope e risultato atteso.
Chiara
Prerequisiti
Lean
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
70