rockafellar

RockafellarWets est un projet dédié à la formalisation des résultats mathématiques présentés dans le manuel "Variational Analysis" de Rockafellar et Wets à l'aide du prouveur de théorèmes Lean 4. Plutôt que de fournir des énoncés de théorèmes isolés, le dépôt vise à construire un développement réutilisable de l'analyse convexe et de l'analyse variationnelle, en s'intégrant aux API de Mathlib. Le projet est organisé chapitre par chapitre et couvre actuellement des parties significatives des éléments suivants : - Chapitre 1 (Max et Min) : Semicontinuité et enveloppes de Moreau. - Chapitre 2 (Convexité) : Ensembles convexes, fonctions, séparation et intérieur relatif. - Chapitre 3 (Cônes et fermeture cosmique) : Constructions d'horizon, coercivité et couches polyédriques. - Chapitre 4 (Convergence d'ensembles) : Limites intérieures, extérieures, d'horizon et cosmiques, et métriques d'hyperspace. - Chapitre 5 (Applications multi-valuées) : Semicontinuité, convergence graphique et théorème de sélection de Michael. - Chapitre 6 (Géométrie variationnelle) : Cônes tangents et normaux, optimalité du premier ordre et lemme de Farkas. Le dépôt comprend des registres de couverture détaillés pour les chapitres 3 à 6, documentant quels résultats sont des adaptations exactes et lesquels ont nécessité des modifications pour la correction mathématique au sein de l'environnement Lean. La feuille de route prévoit des formalisations futures des limites épigraphiques, des sous-dérivées, des propriétés lipschitziennes, du calcul sous-différentiel, de la dualisation, des applications monotones, de la théorie du second ordre et de la mesurabilité.