rockafellar

RockafellarWets — это проект, посвященный формализации математических результатов, представленных в учебнике «Variational Analysis» авторов Rockafellar и Wets, с помощью системы доказательства теорем Lean 4. Вместо предоставления изолированных формулировок теорем, репозиторий стремится создать многократно используемую базу выпуклого и вариационного анализа, интегрированную с API Mathlib. Проект организован по главам и на данный момент охватывает значительные части следующих разделов: - Глава 1 (Max and Min): Полунепрерывность и огибающие Moreau. - Глава 2 (Convexity): Выпуклые множества, функции, разделение и относительная внутренность. - Глава 3 (Cones and Cosmic Closure): Горизонтные конструкции, коэрцитивность и полиэдральные слои. - Глава 4 (Set Convergence): Внутренние, внешние, горизонтные и космические пределы, а также метрики гиперпространств. - Глава 5 (Set-Valued Mappings): Полунепрерывность, графическая сходимость и теорема о выборе Майкла. - Глава 6 (Variational Geometry): Касательные и нормальные конусы, оптимальность первого порядка и лемма Фаркаса. Репозиторий включает подробные реестры охвата для глав с 3 по 6, в которых задокументировано, какие результаты являются точными адаптациями, а какие потребовали модификаций для обеспечения математической корректности в среде Lean. Дорожная карта включает будущую формализацию эпиграфических пределов, субдифференциалов, липшицевых свойств, исчисления субдифференциалов, дуализации, монотонных отображений, теории второго порядка и измеримости.