rockafellar

RockafellarWets is a project dedicated to the formalization of the mathematical results presented in the textbook "Variational Analysis" by Rockafellar and Wets using the Lean 4 theorem prover. Rather than providing isolated theorem statements, the repository aims to build a reusable development of convex analysis and variational analysis, integrating with Mathlib APIs. The project is organized chapter-by-chapter and currently covers significant portions of the following: - Chapter 1 (Max and Min): Semicontinuity and Moreau envelopes. - Chapter 2 (Convexity): Convex sets, functions, separation, and relative interior. - Chapter 3 (Cones and Cosmic Closure): Horizon constructions, coercivity, and polyhedral layers. - Chapter 4 (Set Convergence): Inner, outer, horizon, and cosmic limits, and hyperspace metrics. - Chapter 5 (Set-Valued Mappings): Semicontinuity, graphical convergence, and Michael's selection theorem. - Chapter 6 (Variational Geometry): Tangent and normal cones, first-order optimality, and Farkas' lemma. The repository includes detailed coverage ledgers for Chapters 3 through 6, documenting which results are exact adaptations and which required modifications for mathematical correctness within the Lean environment. The roadmap includes future formalizations of epigraphical limits, subderivatives, Lipschitzian properties, subdifferential calculus, dualization, monotone mappings, second-order theory, and measurability.