On the Formalization of the Lebesgue Integration Theory in HOL
On the Formalization of the Lebesgue Integration Theory in HOL
复制标题
DOI：
10.1007/978-3-642-14052-5_27
复制
发表时间：
2010-07
期刊：
影响因子：
--
通讯作者：
Tarek Mhamdi;O. Hasan;S. Tahar
中科院分区：
文献类型：
--
作者：
Tarek Mhamdi;O. Hasan;S. Tahar
勒贝格积分是实分析、概率论、信息论等许多数学理论中的一个基本概念。已知的Lebesgue积分的高阶逻辑形式化要么不包括Borel代数，要么对Borel代数有有限的支持，Borel代数是在定义Lebesgue积分的任何度量空间上使用的标准sigma代数。在本文中，我们通过提出一种可用于任何度量空间（如复数或n维欧几里德空间）的Borel sigma代数的形式化来克服这一限制。在这个框架的基础上，我们证明了勒贝格积分的一些关键性质，如线性和单调收敛性。进一步，我们给出了“几乎处处”关系的形式化，并证明了Lebesgue积分不区分在零集上不同的函数，以及基于这一概念的其他重要结果。作为应用，我们给出了马尔可夫不等式和切比雪夫不等式的证明以及大数弱定律定理。
Lebesgue integration is a fundamental concept in many mathematical theories, such as real analysis, probability and information theory. Reported higher-order-logic formalizations of the Lebesgue integral either do not include, or have a limited support for the Borel algebra, which is the canonical sigma algebra used on any metric space over which the Lebesgue integral is defined. In this paper, we overcome this limitation by presenting a formalization of the Borel sigma algebra that can be used on any metric space, such as the complex numbers or the n-dimensional Euclidean space. Building on top of this framework, we have been able to prove some key Lebesgue integral properties, like its linearity and monotone convergence. Furthermore, we present the formalization of the “almost everywhere” relation and prove that the Lebesgue integral does not distinguish between functions which differ on a null set as well as other important results based on this concept. As applications, we present the verification of Markov and Chebyshev inequalities and the Weak Law of Large Numbers theorem.