इस प्रोजेक्ट के बारे में

RockafellarWets एक ऐसी परियोजना है जो Lean 4 theorem prover का उपयोग करके Rockafellar और Wets की पाठ्यपुस्तक "Variational Analysis" में प्रस्तुत गणितीय परिणामों के औपचारिकरण (formalization) के लिए समर्पित है। अलग-थलग प्रमेय कथनों को प्रदान करने के बजाय, इस रिपॉजिटरी का लक्ष्य convex analysis और variational analysis का एक पुन: प्रयोज्य विकास बनाना है, जो Mathlib APIs के साथ एकीकृत हो। परियोजना को अध्याय-दर-अध्याय व्यवस्थित किया गया है और वर्तमान में इसमें निम्नलिखित के महत्वपूर्ण हिस्से शामिल हैं: - अध्याय 1 (Max and Min): Semicontinuity और Moreau envelopes। - अध्याय 2 (Convexity): Convex sets, functions, separation, और relative interior। - अध्याय 3 (Cones and Cosmic Closure): Horizon constructions, coercivity, और polyhedral layers। - अध्याय 4 (Set Convergence): Inner, outer, horizon, और cosmic limits, और hyperspace metrics। - अध्याय 5 (Set-Valued Mappings): Semicontinuity, graphical convergence, और Michael's selection theorem। - अध्याय 6 (Variational Geometry): Tangent और normal cones, first-order optimality, और Farkas' lemma। रिपॉजिटरी में अध्याय 3 से 6 तक के विस्तृत कवरेज लेजर शामिल हैं, जो यह दस्तावेजीकरण करते हैं कि कौन से परिणाम सटीक अनुकूलन हैं और किन्हें Lean वातावरण के भीतर गणितीय शुद्धता के लिए संशोधनों की आवश्यकता थी। रोडमैप में epigraphical limits, subderivatives, Lipschitzian properties, subdifferential calculus, dualization, monotone mappings, second-order theory, और measurability का भविष्य का औपचारिकरण शामिल है।