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库，甚至为乌雷松引理设计了一种新证明。