依赖类型理论中基于扩展的度量构建及其在积分中的应用
摘要：用Coq证明助手对测度和积分理论进行了原创形式化。我们按照一个标准构造来建立勒贝格测度，这一构造在基于依赖类型理论的证明助手中尚未形式化：通过对集合的半环的测度的扩展。我们通过利用Mathematical Components项目中的现有技术来实现这种形式化。我们解释了如何扩展Mathematical Components的迭代算子和数学结构以支持无穷和扩展实数。我们引入了测度论的新数学结构，并意外地提供了Hierarchy-Builder的一个具体应用，这是一个用于数学结构层次化形式化的通用工具。这种测度论的形式化为与Mathematical Components项目兼容的勒贝格积分的新形式化提供了基础。
作者：Reynald Affeldt and Cyril Cohen
论文ID：2209.02345
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-07