عن المشروع

مشروع RockafellarWets هو مشروع مخصص للصياغة الرسمية للنتائج الرياضية الواردة في كتاب "Variational Analysis" من تأليف Rockafellar و Wets باستخدام مثبت النظريات Lean 4. وبدلاً من تقديم بيانات نظريات معزولة، يهدف المستودع إلى بناء تطوير قابل لإعادة الاستخدام للتحليل المحدب والتحليل التبايني، مع التكامل مع واجهات برمجة تطبيقات Mathlib. تم تنظيم المشروع فصلاً بفصل، وهو يغطي حالياً أجزاءً كبيرة مما يلي: - الفصل 1 (الحد الأقصى والأدنى): شبه الاستمرارية وأغلفة Moreau. - الفصل 2 (التحدب): المجموعات المحدبة، والدوال، والفصل، والداخل النسبي. - الفصل 3 (المخاريط والإغلاق الكوني): إنشاءات الأفق، والقسرية، والطبقات متعددة السطوح. - الفصل 4 (تقارب المجموعات): الحدود الداخلية والخارجية وحدود الأفق والحدود الكونية، ومقاييس الفضاء الفائق. - الفصل 5 (التطبيقات ذات القيم المجموعية): شبه الاستمرارية، والتقارب الرسومي، ونظرية اختيار Michael. - الفصل 6 (الهندسة التباينية): المخاريط المماسية والعمودية، والأمثلية من الدرجة الأولى، ولمة Farkas. يتضمن المستودع سجلات تغطية مفصلة للفصول من 3 إلى 6، توثق النتائج التي تعد تكييفات دقيقة وتلك التي تطلبت تعديلات لتحقيق الصحة الرياضية ضمن بيئة Lean. وتتضمن خارطة الطريق صياغات رسمية مستقبلية للحدود الإبيغرافية، والمشتقات الفرعية، وخصائص Lipschitzian، وحساب التفاضل الفرعي، والمزدوجة، والتطبيقات الرتيبة، ونظرية الدرجة الثانية، والقابلية للقياس.