非负函数勒贝格积分的 Coq 形式化
计算机科学中的逻辑
2021-12-10 v2 泛函分析
摘要
积分与微分一样，是被广泛运用于诸多科学领域的基本微积分工具。在形式化证明助手中形式化积分的数学概念及相关结果，有助于为涉及直接或间接使用积分的数值程序的正确性提供最高程度的信心。勒贝格积分因其能将（黎曼）积分扩展到广泛的一类不规则函数以及定义于比实直线更一般空间上的函数，非常适用于概率论、数值数学与实分析等数学领域。本文给出 -代数、测度、简单函数以及非负可测函数积分的 Coq 形式化，直至贝波·列维（单调收敛）定理与法图引理的完整形式化证明。相较于既有文献的平铺式形式化，我们给出了若干在数可读性与其 Coq 定理可用性之间取得平衡的设计选择。这些结果是朝向 空间（如巴拿赫空间）形式化的第一个里程碑。
引用
@article{arxiv.2104.05256,
title = {A Coq Formalization of Lebesgue Integration of Nonnegative Functions},
author = {Sylvie Boldo and François Clément and Florian Faissole and Vincent Martin and Micaela Mayero},
journal= {arXiv preprint arXiv:2104.05256},
year = {2021}
}