Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq

Reynald Affeldt, Zachary Stone

TL;DR

This work presents a comprehensive formalization of the Lebesgue Differentiation Theorem in the Coq proof assistant within the MathComp-Analysis library, enabling the first Fundamental Theorem of Calculus for Lebesgue integration as a corollary. The approach decomposes the proof into modular, independently useful components—topological extensions (subspace topology, uniform convergence), measure-theoretic results (Egorov/Lusin/Tietze), and a novel proof of Urysohn's lemma—then derives the Hardy-Littlewood maximal inequality and Vitali covering lemmas to control averages. The combination of these intermediate results yields the differentiation theorem and key corollaries such as the first FTC and Lebesgue density, illustrating the practicality of large-scale formalization in Coq and advancing MathComp-Analysis with robust, reusable theory. The work also emphasizes incremental, collaborative development and documents nuances in formalizing real analysis, paving the way for future extensions like the Radon-Nikodym-based second FTC.

Abstract

Formalization of real analysis offers a chance to rebuild traditional proofs of important theorems as unambiguous theories that can be interactively explored. This paper provides a comprehensive overview of the Lebesgue Differentiation Theorem formalized in the Coq proof assistant, from which the first Fundamental Theorem of Calculus (FTC) for the Lebesgue integral is obtained as a corollary. Proving the first FTC in this way has the advantage of decomposing into loosely-coupled theories of moderate size and of independent interest that lend themselves well to incremental and collaborative development. We explain how we formalize all the topological constructs and all the standard lemmas needed to eventually relate the definitions of derivability and of Lebesgue integration of MathComp-Analysis, a formalization of analysis developed on top of the Mathematical Components library. In the course of this experiment, we substantially enrich MathComp-Analysis and even devise a new proof for Urysohn's lemma.

A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq

TL;DR

This work presents a comprehensive formalization of the Lebesgue Differentiation Theorem in the Coq proof assistant within the MathComp-Analysis library, enabling the first Fundamental Theorem of Calculus for Lebesgue integration as a corollary. The approach decomposes the proof into modular, independently useful components—topological extensions (subspace topology, uniform convergence), measure-theoretic results (Egorov/Lusin/Tietze), and a novel proof of Urysohn's lemma—then derives the Hardy-Littlewood maximal inequality and Vitali covering lemmas to control averages. The combination of these intermediate results yields the differentiation theorem and key corollaries such as the first FTC and Lebesgue density, illustrating the practicality of large-scale formalization in Coq and advancing MathComp-Analysis with robust, reusable theory. The work also emphasizes incremental, collaborative development and documents nuances in formalizing real analysis, paving the way for future extensions like the Radon-Nikodym-based second FTC.

Abstract

Formalization of real analysis offers a chance to rebuild traditional proofs of important theorems as unambiguous theories that can be interactively explored. This paper provides a comprehensive overview of the Lebesgue Differentiation Theorem formalized in the Coq proof assistant, from which the first Fundamental Theorem of Calculus (FTC) for the Lebesgue integral is obtained as a corollary. Proving the first FTC in this way has the advantage of decomposing into loosely-coupled theories of moderate size and of independent interest that lend themselves well to incremental and collaborative development. We explain how we formalize all the topological constructs and all the standard lemmas needed to eventually relate the definitions of derivability and of Lebesgue integration of MathComp-Analysis, a formalization of analysis developed on top of the Mathematical Components library. In the course of this experiment, we substantially enrich MathComp-Analysis and even devise a new proof for Urysohn's lemma.
Paper Structure (29 sections, 2 equations, 2 figures, 1 table)

This paper contains 29 sections, 2 equations, 2 figures, 1 table.

Table of Contents

  1. Introduction
  2. Background on MathComp-Analysis
  3. Statement of the Lebesgue Differentiation theorem
  4. Proof of the Lebesgue Differentiation theorem
  5. Topological constructs added to MathComp-Analysis
  6. Subspace topologies
  7. Uniform convergence
  8. More support for extended real-valued functions
  9. Egorov's theorem and regularity
  10. Egorov's theorem
  11. Regularity
  12. Outer regularity
  13. Inner regularity
  14. A new proof of Urysohn's lemma
  15. Urysohn's lemma using uniform separator
  16. ...and 14 more sections

Figures (2)

  • Figure 1: Overview of the proof of the Lebesgue Differentiation theorem and derived results (dashed arrows indicate generalizations from statements about bounded sets)
  • Figure 2: Overview of a novel proof of Urysohn's lemma and derived results (dashed nodes are derived results that are not relevant to the Lebesgue Differentiation theorem)