rockafellar

RockafellarWets é um projeto dedicado à formalização dos resultados matemáticos apresentados no livro "Variational Analysis", de Rockafellar e Wets, utilizando o provador de teoremas Lean 4. Em vez de fornecer enunciados de teoremas isolados, o repositório visa construir um desenvolvimento reutilizável de análise convexa e análise variacional, integrando-se com as APIs do Mathlib. O projeto é organizado capítulo por capítulo e atualmente cobre partes significativas do seguinte: - Capítulo 1 (Max and Min): Semicontinuidade e envelopes de Moreau. - Capítulo 2 (Convexity): Conjuntos convexos, funções, separação e interior relativo. - Capítulo 3 (Cones and Cosmic Closure): Construções de horizonte, coercitividade e camadas poliédricas. - Capítulo 4 (Set Convergence): Limites internos, externos, de horizonte e cósmicos, e métricas de hiperespaço. - Capítulo 5 (Set-Valued Mappings): Semicontinuidade, convergência gráfica e o teorema de seleção de Michael. - Capítulo 6 (Variational Geometry): Cones tangentes e normais, optimalidade de primeira ordem e o lema de Farkas. O repositório inclui livros de registro de cobertura detalhados para os Capítulos 3 a 6, documentando quais resultados são adaptações exatas e quais exigiram modificações para correção matemática dentro do ambiente Lean. O roteiro inclui formalizações futuras de limites epigráficos, subderivadas, propriedades Lipschitzianas, cálculo subdiferencial, dualização, mapeamentos monotonos, teoria de segunda ordem e mensurabilidade.