DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2024.5

A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq

Authors: Reynald Affeldt and Zachary Stone

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

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.

Cite as

Reynald Affeldt and Zachary Stone. A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{affeldt_et_al:LIPIcs.ITP.2024.5,
  author =	{Affeldt, Reynald and Stone, Zachary},
  title =	{{A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{5:1--5:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.5},
  URN =		{urn:nbn:de:0030-drops-207330},
  doi =		{10.4230/LIPIcs.ITP.2024.5},
  annote =	{Keywords: Coq proof assistant, Mathematical Components library, Lebesgue integral, fundamental theorem of calculus}
}

Search Results

Documents authored by Stone, Zachary

A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq

Abstract

Cite as

Thanks for your feedback!

Could not send message