The files in this directory contain a formalization of my text An introduction to measure theory into Lean. The formalization is intended to be as faithful a paraphrasing as possible to the original text, while also showcasing Lean's features and syntax. In particular, the formalization is not optimized for efficiency, and in some cases may deviate from idiomatic Lean usage.

Portions of the text that were left as exercises to the reader, as well as many of the proofs in the text are rendered in this translation as sorrys. Readers who are not in my classes are also welcome to submit such proofs.

Some of the material in this text is duplicated in Lean's standard math library Mathlib, though with slightly different definitions. To reconcile these discrepancies, this formalization will gradually transition from the textbook-provided definitions to the Mathlib-provided definitions as one progresses further into the text, thus sacrificing the self-containedness of the formalization in favor of compatibility with Mathlib. For instance, Chapter 2 develops a theory of the natural numbers independent of Mathlib, but all subsequent chapters will use the Mathlib natural numbers instead. (An epilogue to Chapter 2 is provided to show that the two notions of the natural numbers are isomorphic.) As such, this formalization can also be used as an introduction to various portions of Mathlib.

• Notation section (Documentation) (Lean source)
• Chapter 1: Measure Theory
  • Section 1.1: Prologue: the problem of measure
    • Section 1.1.1: Elementary measure (Documentation) (Lean source)
    • Section 1.1.2: Jordan measure (Documentation) (Lean source)
    • Section 1.1.3: Connections with the Riemann integral (Documentation) (Lean source)
  • Section 1.2: Lebesgue measure
    • Introduction: (Documentation) (Lean source)
    • Section 1.2.1: Properties of Lebesgue outer measure (Documentation) (Lean source)
    • Section 1.2.2: Lebesgue measurability (Documentation) (Lean source)
    • Section 1.2.3: Non-measurable sets (Documentation) (Lean source)
  • Section 1.3: The Lebesgue integral
    • Section 1.3.1: Integration of simple functions (Documentation) (Lean source)
    • Section 1.3.2: Measurable functions (Documentation) (Lean source)
    • Section 1.3.3: Unsigned Lebesgue integrals (Documentation) (Lean source)
    • Section 1.3.4: Absolute integrability (Documentation) (Lean source)
    • Section 1.3.5: Littlewood's three principles (Documentation) (Lean source)
  • Section 1.4: Abstract measure spaces
    • Section 1.4.1: Boolean algebras (Documentation) (Lean source)
    • Section 1.4.2: $\sigma$-algebras and measurable spaces (Documentation) (Lean source)
    • Section 1.4.3: Countably additive measures and measure spaces (Documentation) (Lean source)
    • Section 1.4.4: Measurable functions, and integration on a measure space (Documentation) (Lean source)
    • Section 1.4.5: The convergence theorems (Documentation) (Lean source)
  • Section 1.5: Modes of convergence
    • Introduction: (Documentation) (Lean source)
    • Section 1.5.1: Uniqueness (Documentation) (Lean source)
    • Section 1.5.2: The case of a step function (Documentation) (Lean source)
    • Section 1.5.3: Finite measure spaces (Documentation) (Lean source)
    • Section 1.5.4: Domination and uniform integrability (Documentation) (Lean source)
  • Section 1.6: Differentiation theorems
    • Introduction: (Documentation) (Lean source)
    • Section 1.6.1: The Lebesgue differentiation theorem in one dimension (Documentation) (Lean source)
    • Section 1.6.2: The Lebesgue differentiation theorem in higher dimensions (Documentation) (Lean source)
    • Section 1.6.3: Almost everywhere differentiability (Documentation) (Lean source)
  • Section 1.7: Outer measure, pre-measure, and product measures
    • Introduction: (Documentation) (Lean source)
    • Section 1.7.1: Outer measures and the Carathéodory extension theorem (Documentation) (Lean source)
    • Section 1.7.2: Pre-measures (Documentation) (Lean source)
    • Section 1.7.3: Lebesgue-Stieltjes measure (Documentation) (Lean source)
    • Section 1.7.4: Product measure (Documentation) (Lean source)
  • Chapter 2: Related articles (possible future expansion)

• The Lean community
  • Lean4 web playground
  • How to run a project in Lean locally
  • The Lean community Zulip chat
  • Learning Lean4
    • The natural number game
    • Mathematics in Lean - Lean textbook by Jeremy Avigad and Patrick Massot
• Mathlib documentation
  • Mathlib help files
  • Moogle - semantic search engine for Mathlib
  • Loogle - expression matching search engine for Mathlib
  • LeanSearch - Natural language search engine for Mathlib
  • List of Mathlib tactics
    • Lean tactics cheat sheet
• Lean extensions:
  • Canonical
  • Duper
  • LeanCopilot
• Common Lean pitfalls
• Lean4 questions in Proof Stack Exchange
• The mechanics of proof - introductory Lean textbook by Heather Macbeth
• My Youtube channel has some demonstrations of various Lean formalization, using a variety of tools.
• A broader list of AI and formal mathematics resources.

More resource suggestions welcome!