প্রকল্প সম্পর্কে

RockafellarWets হলো একটি প্রজেক্ট যা Lean 4 থিওরেম প্রুভার ব্যবহার করে Rockafellar এবং Wets-এর "Variational Analysis" পাঠ্যবইয়ে উপস্থাপিত গাণিতিক ফলাফলগুলোর ফরম্যলাইজেশনের জন্য নিবেদিত। বিচ্ছিন্ন থিওরেম স্টেটমেন্ট প্রদানের পরিবর্তে, এই রিপোজিটরিটির লক্ষ্য হলো Mathlib API-এর সাথে সমন্বয় করে কনভেক্স অ্যানালাইসিস এবং ভ্যারিয়েশনাল অ্যানালাইসিসের একটি পুনঃব্যবহারযোগ্য ডেভেলপমেন্ট তৈরি করা। প্রজেক্টটি অধ্যায় অনুযায়ী সাজানো হয়েছে এবং বর্তমানে নিম্নলিখিত বিষয়গুলোর উল্লেখযোগ্য অংশ কভার করে: - অধ্যায় ১ (Max and Min): Semicontinuity এবং Moreau envelopes। - অধ্যায় ২ (Convexity): Convex sets, functions, separation, এবং relative interior। - অধ্যায় ৩ (Cones and Cosmic Closure): Horizon constructions, coercivity, এবং polyhedral layers। - অধ্যায় ৪ (Set Convergence): Inner, outer, horizon, এবং cosmic limits, এবং hyperspace metrics। - অধ্যায় ৫ (Set-Valued Mappings): Semicontinuity, graphical convergence, এবং Michael's selection theorem। - অধ্যায় ৬ (Variational Geometry): Tangent এবং normal cones, first-order optimality, এবং Farkas' lemma। রিপোজিটরিটিতে অধ্যায় ৩ থেকে ৬ পর্যন্ত বিস্তারিত কভারেজ লেজার অন্তর্ভুক্ত রয়েছে, যেখানে নথিভুক্ত করা হয়েছে যে কোন ফলাফলগুলো হুবহু অভিযোজন এবং কোনগুলোর জন্য Lean এনভায়রনমেন্টের গাণিতিক সঠিকতার প্রয়োজনে পরিবর্তনের প্রয়োজন ছিল। রোডম্যাপের মধ্যে ভবিষ্যতে epigraphical limits, subderivatives, Lipschitzian properties, subdifferential calculus, dualization, monotone mappings, second-order theory, এবং measurability-র ফরম্যলাইজেশন অন্তর্ভুক্ত রয়েছে।