eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-09-02
5:1
5:19
10.4230/LIPIcs.ITP.2024.5
article
A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq
Affeldt, Reynald
1
https://orcid.org/0000-0002-2327-953X
Stone, Zachary
2
National Institute of Advanced Industrial Science and Technology (AIST), Tokyo, Japan
The MathComp-Analysis development team, Boston, MA, USA
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol309-itp2024/LIPIcs.ITP.2024.5/LIPIcs.ITP.2024.5.pdf
Coq proof assistant
Mathematical Components library
Lebesgue integral
fundamental theorem of calculus