منصوبے کے بارے میں

RockafellarWets ایک ایسا پروجیکٹ ہے جو Lean 4 theorem prover کا استعمال کرتے ہوئے Rockafellar اور Wets کی درسی کتاب "Variational Analysis" میں پیش کردہ ریاضیاتی نتائج کی فارمیلیزیشن کے لیے وقف ہے۔ الگ تھلگ تھیورم بیانات فراہم کرنے کے بجائے، اس ریپوزٹری کا مقصد convex analysis اور variational analysis کی ایک قابلِ استعمال ڈویلپمنٹ بنانا ہے، جو Mathlib APIs کے ساتھ مربوط ہو۔ اس پروجیکٹ کو باب بہ باب ترتیب دیا گیا ہے اور فی الحال درج ذیل کے اہم حصوں کا احاطہ کرتا ہے: - باب 1 (Max and Min): Semicontinuity اور Moreau envelopes۔ - باب 2 (Convexity): Convex sets، فنکشنز، علیحدگی (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 کی فارمیلیزیشن شامل ہے۔