Часткова формалізація в Lean книги Аналіз I

Файли в цьому каталозі містять формалізацію вибраних частин мого (пр.перекл. тут і далі це Терренс Тао) тексту Аналіз I у Lean. Формалізація має на меті максимально точно перефразувати оригінальний текст, а також продемонструвати особливості та синтаксис Lean. Зокрема, формалізація не оптимізована під ефективність, а в деяких випадках може відхилятися від ідіоматичного використання Lean.

Частини тексту, залишені як вправи для читача, у цьому перекладі передаються як тактика sorry. Читачі можуть створити форк репозиторію, щоб спробувати свої сили у виконанні цих вправ, але я не маю наміру розміщувати рішення безпосередньо в цьому репозиторії.

Хоча розташування визначень, теорем і доказів тут є близьким перефразуванням підручника, я утримуюся від прямого цитування матеріалу з підручника, натомість наводжу посилання на оригінальний текст, де це доречно. Таким чином, цю формалізацію слід розглядати як анотоване доповнення до основного тексту, а не як його заміну.

Значна частина матеріалу в цьому тексті продубльована у стандартній математичній бібліотеці Lean Mathlib, хоча й з дещо іншими визначеннями. Щоб усунути ці розбіжності, ця формалізація поступово переходитиме від визначень, наданих підручником, до визначень, наданих Mathlib, у міру просування в тексті, жертвуючи таким чином самодостатністю формалізації на користь сумісності з Mathlib. Наприклад, у розділі 2 розвивається теорія натуральних чисел незалежно від Mathlib, але в усіх наступних розділах замість неї використовуватимуть натуральні числа Mathlib. (Епілог до розділу 2 надається, щоб показати, що два поняття натуральних чисел ізоморфні.) Таким чином, цю формалізація також може бути використана як вступ до різних частин Mathlib.

Для узгодження формалізації з домовленостями Mathlib, до деяких визначень було внесено невелику кількість технічних змін порівняно з версією підручника. Найбільш помітні:

• Послідовності індексуються з нуля, а не з одиниці, оскільки Mathlib має набагато більше підтримки для натуральних чисел ℕ з нульовою нумерацією, ніж для натуральних чисел з одиничною нумерацією.

• Багатьом операціям, які залишилися невизначеними в тексті, таким як ділення на нуль або отримання формальної границі не-Коші послідовності, замість цього присвоюється "сміттєве" значення (наприклад, 0), щоб зробити операцію повністю визначеною. Це пояснюється тим, що Lean має кращу підтримку повних функцій (пр.перекл. total functions), ніж часткових функцій (пр.перекл. partial functions) (нерозбірливе використання останніх може призвести до "пекла залежних типів", в якому навіть дуже прості маніпуляції вимагають досить тонких і делікатних доказів). Дивіться, наприклад, цю публікацію в блозі Кевіна Баззарда для отримання додаткової інформації.

Поточні формалізовані розділи:

• Глава 2.1: Аксіоми Пеано

• Глава 2.2: Додавання

• Глава 2.3: Множення

• Розділ 2, Епілог: Ізоморфізм із натуральними числами Mathlib

• Глава 3.1: Основи теорії множин

• Глава 3.2: Парадок Рассела

• Глава 3.3: Функції

• Глава 3.4: Образи та прообрази

• Глава 3.5: Декартов добуток

• Глава 3.6: Cardinality of sets

• Глава 4.1: The integers

• Глава 4.2: The rationals

• Глава 4.3: Absolute value and exponentiation

• Глава 4.4: Gaps in the rational numbers

• Глава 5.1: Cauchy sequences of rationals

• Глава 5.2: Equivalent Cauchy sequences

• Глава 5.3: Construction of the real numbers

• Глава 5.4: Ordering the reals

• Глава 5.5: The least upper bound property

• Chapter 5 epilogue: Isomorphism with the Mathlib reals

• Глава 6.1: Convergence and limit laws

• Глава 6.2: The extended real number system

• Глава 6.3: Suprema and Infima of sequences

• Глава 6.4: Lim inf, lim sup, and limit points

• Глава 6.5: Some standard limits

• Глава 6.6: Subsequences

• Глава 6 epilogue: Connections with Mathlib limits

• Глава 7.1: Finite series

• Глава 7.2: Infinite series

• Глава 7.3: Sums of non-negative numbers

• Глава 7.4: Rearrangement of series

• Глава 7.5: The root and ratio tests

• Глава 9.1: Subsets of the real line

• Глава 9.2: The algebra of real-valued functions

• Глава 9.3: Limiting values of functions

• Глава 9.4: Continuous functions

• Глава 9.5: Left and right limits

• Глава 9.6: The maximum principle

• Глава 9.7: The intermediate value theorem

• Глава 9.8: Monotone functions

• Глава 9.9: Uniform continuity

• Глава 9.10: Limits at infinity

• Глава 10.1: Basic definitions

• Глава 10.2: Local extrema and derivatives

• Глава 10.3: Monotone functions and derivatives

• Глава 10.4: The inverse function theorem

• Глава 10.5: L'Hôpital's rule

• Глава 11.1: Partitions

• Глава 11.2: Piecewise constant functions

• Глава 11.3: Upper and lower Riemann integrals

• Додаток A.1: Математичні твердження

• Додаток A.2: Висновки

• Додаток A.3: Структура доказів

• Додаток A.4: Змінні та квантіфікатори

• Додаток A.5: Вкладені квантифікатори

• Додаток A.6: Деякі приклади доведень та квантифікаторів

• Додаток A.7: Рівність