rockafellar

RockafellarWets 是一个致力于使用 Lean 4 定理证明器，对 Rockafellar 和 Wets 的教科书《Variational Analysis》中呈现的数学结果进行形式化的项目。该仓库的目标并非提供孤立的定理陈述，而是旨在构建一个可重用的凸分析和变分分析开发体系，并与 Mathlib API 集成。 该项目按章节组织，目前涵盖了以下内容的很大一部分： - 第 1 章（最大值与最小值）：半连续性和 Moreau envelopes。 - 第 2 章（凸性）：凸集、函数、分离以及相对内部。 - 第 3 章（锥与 Cosmic Closure）：Horizon 构造、强制性（coercivity）和多面体层。 - 第 4 章（集合收敛）：内部、外部、horizon 和 cosmic 极限，以及超空间度量。 - 第 5 章（集值映射）：半连续性、图形收敛和 Michael 选择定理。 - 第 6 章（变分几何）：切锥与法锥、一阶最优性以及 Farkas 引理。 该仓库包含了第 3 章至第 6 章的详细覆盖账本，记录了哪些结果是精确适配的，以及哪些结果为了在 Lean 环境中保证数学正确性而进行了修改。路线图包括未来对 epigraphical 极限、次导数、Lipschitz 属性、次微分演算、对偶化、单调映射、二阶理论和可测性的形式化。