leanprover-community/mathlib4

The Shapley-Folkman lemma

Aberta

#14.427 aberto em 4 de jul. de 2024

Ver no GitHubGuia do colaborador
 (11 comentários) (2 reações) (1 responsável)Lean (1.597 forks)github user discovery
good first issuet-analysis

Métricas do repositório

Stars
 (3.877 estrelas)
Métricas de merge de PR
 (Nenhuma PRs mesclada em 30d)

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.

Guia do colaborador

Direção de pesquisa
Estude as provas dos teoremas de Carathéodory e Radon, depois adapte a abordagem usando análise convexa para formalizar o lema de Shapley Folkman.
Pilha de tecnologia
None
Domain
None
Tipo Issue
Funcionalidade
DifficultyDificuldade de implementação estimada para um novo contribuidor, de 1 para alterações muito pequenas a 5 para trabalho de nível especializado.
3
Tempo estimadoUm intervalo de tempo aproximado para um colaborador experiente investigar, implementar, testar e preparar um pull request.
1-3 horas
Status da atividadeQuão disponível o issue aparece agora: novo, ativo, obsoleto, bloqueado ou aguardando entrada do mantenedor.
Ativo
ClarityCom que clareza o issue explica a mudança esperada, os critérios de aceitação e a próxima etapa.
Claro
Prerequisites
Lean
Simpatia para novatosUma pontuação de 1 a 100 que estima o quão acessível este issue é para colaboradores iniciantes.
70