Formalization of "Analysis I" by Terence Tao

The goal of this project is to formalize the book "Analysis I" by Terence Tao, including the main text and the exercises. This is a work in progress. The formalization is done in Lean using the Mathlib library (currently version 4).

We acknowledge the use of AI tools to assist in the formalization process, notably GitHub Copilot.

Progress

(Updated on 2025-03-10)

Main text

• 2. Starting at the Beginning: The Natural Numbers
  • 2.1. The Peano axioms
  • 2.2. Addition
  • 2.3. Multiplication
• 3. Set Theory
  • 3.1. Fundamentals
  • 3.2. Russell's Paradox
  • 3.3. Functions
  • 3.4. Images and Inverse Images
  • 3.5. Cartesian Products
  • 3.6. Cardinality of Sets
• 4. Integers and Rationals
• 5. The Real Numbers
• 6. Limits of Sequences
• 7. Series
• 8. Infinite Sets
• 9. Continuous Functions on R
• 10. Differentiation of Functions
• 11. The Riemann Integral
• Appendix A: The Basics of Mathematical Logic
• Appendix B: The Decimal System

Solutions to exercises

• 2. Starting at the Beginning: The Natural Numbers
  • 2.2. Addition
  • 2.3. Multiplication
• 3. Set Theory
  • 3.1. Fundamentals
  • 3.2. Russell's Paradox
  • 3.3. Functions
  • 3.4. Images and Inverse Images
  • 3.5. Cartesian Products
  • 3.6. Cardinality of Sets
• 4. Integers and Rationals
• 5. The Real Numbers
• 6. Limits of Sequences
• 7. Series
• 8. Infinite Sets
• 9. Continuous Functions on R
• 10. Differentiation of Functions
• 11. The Riemann Integral
• Appendix A: The Basics of Mathematical Logic
• Appendix B: The Decimal System

License

The project is licensed under the MIT License. See LICENSE for details.