勒贝格积分：用于在 Coq 中形式化的详细证明
计算机科学中的逻辑
2021-04-05 v2 经典分析与常微分方程
泛函分析
摘要
为了对实现有限元法的数值模拟程序的正确性获得最高置信度，必须形式化那些用以确立该方法可靠性的数学概念与结果。Sobolev 空间是大多数偏微分方程弱形式表述并求解的数学框架。这些函数空间建立在积分与测度论之上。因此，泛函分析中的这一章是定义有限元方法的必备理论基石。本文档旨在为形式化证明社区提供积分与测度论主要结果的极其详尽的笔纸证明。
引用
@article{arxiv.2101.05678,
title = {Lebesgue integration. Detailed proofs to be formalized in Coq},
author = {François Clément and Vincent Martin},
journal= {arXiv preprint arXiv:2101.05678},
year = {2021}
}