rockafellar

RockafellarWetsは、RockafellarとWetsの教科書『Variational Analysis』で提示された数学的結果を、定理証明支援系Lean 4を用いて形式化することに特化したプロジェクトです。単に個別の定理を記述するのではなく、Mathlib APIと統合し、凸解析および変分解析の再利用可能な開発基盤を構築することを目指しています。 プロジェクトは章ごとに構成されており、現在は以下の主要部分をカバーしています： - 第1章 (Max and Min)：半連続性とMoreauエンベロープ。 - 第2章 (Convexity)：凸集合、凸関数、分離、および相対内部。 - 第3章 (Cones and Cosmic Closure)：ホライゾン構成、強制性、および多面体層。 - 第4章 (Set Convergence)：内部、外部、ホライゾン、およびコスミック極限、およびハイパースペース計量。 - 第5章 (Set-Valued Mappings)：半連続性、グラフ収束、およびMichaelの選択定理。 - 第6章 (Variational Geometry)：接錐と法錐、一次最適性、およびFarkasの補題。 リポジトリには第3章から第6章までの詳細なカバーレッジ台帳が含まれており、どの結果が正確な適応であるか、またLean環境内での数学的正当性のためにどの修正が必要であったかが記録されています。今後のロードマップには、エピグラフ極限、劣微分、リプシッツ特性、劣微分計算、双対化、単調写像、二次理論、および可測性の形式化が含まれています。