rockafellar

RockafellarWets es un proyecto dedicado a la formalización de los resultados matemáticos presentados en el libro de texto "Variational Analysis" de Rockafellar y Wets utilizando el probador de teoremas Lean 4. En lugar de proporcionar enunciados de teoremas aislados, el repositorio tiene como objetivo construir un desarrollo reutilizable de análisis convexo y análisis variacional, integrándose con las APIs de Mathlib. El proyecto está organizado capítulo por capítulo y actualmente cubre partes significativas de lo siguiente: - Capítulo 1 (Max and Min): Semicontinuidad y envolventes de Moreau. - Capítulo 2 (Convexity): Conjuntos convexos, funciones, separación e interior relativo. - Capítulo 3 (Cones and Cosmic Closure): Construcciones de horizonte, coercitividad y capas poliédricas. - Capítulo 4 (Set Convergence): Límites internos, externos, de horizonte y cósmicos, y métricas de hiperespacio. - Capítulo 5 (Set-Valued Mappings): Semicontinuidad, convergencia gráfica y el teorema de selección de Michael. - Capítulo 6 (Variational Geometry): Conos tangentes y normales, optimalidad de primer orden y el lema de Farkas. El repositorio incluye libros de registro de cobertura detallados para los Capítulos 3 al 6, documentando qué resultados son adaptaciones exactas y cuáles requirieron modificaciones para la corrección matemática dentro del entorno Lean. La hoja de ruta incluye formalizaciones futuras de límites epigráficos, subderivadas, propiedades Lipschitzianas, cálculo subdiferencial, dualización, mapeos monótonos, teoría de segundo orden y medibilidad.