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.

翻译：实分析的形式化为重建重要定理的传统证明提供了契机，使得这些定理能以可交互探索的无歧义理论形式呈现。本文全面综述了Coq证明助手中形式化的勒贝格微分定理，并由此推导出勒贝格积分语境下第一个微积分基本定理作为推论。以这种方式证明第一个微积分基本定理的优势在于，它能将证明分解为规模适中且具有独立研究价值的松散耦合理论，这些理论非常适合增量式协作开发。我们阐释了如何形式化所有拓扑构造及标准引理，最终建立数学组件库上构建的分析形式化库MathComp-Analysis中可微性与勒贝格积分定义之间的关联。在此实验过程中，我们显著丰富了MathComp-Analysis的内容，甚至为乌雷松引理提出了全新的证明方法。