Coq中勒贝格微分定理的全面概述

实分析的形式化为将重要定理的传统证明重建为可交互探索的无歧义理论提供了机会。本文全面概述了在Coq证明助手中形式化的勒贝格微分定理，并由此得到勒贝格积分的第一微积分基本定理（FTC）作为推论。以这种方式证明第一FTC具有优势，它将问题分解为规模适中、相互独立且本身具有研究价值的理论，这些理论适合增量式和协作式开发。我们解释了如何形式化所有拓扑构造以及所有标准引理，最终将MathComp-Analysis（一个基于数学组件库开发的分析形式化库）中可微性和勒贝格积分的定义联系起来。在此实验过程中，我们极大地丰富了MathComp-Analysis，甚至为乌雷松引理设计了一个新证明。