Three Chapters of Measure Theory in Isabelle/HOL
Three Chapters of Measure Theory in Isabelle/HOL
复制标题
《Isabelle/HOL》中的测度论三章
DOI：
10.1007/978-3-642-22863-6_12
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Armin Heller
中科院分区：
文献类型：
--
作者：
Johannes Hölzl;Armin Heller
目前发表的HOL形式化的测度理论集中在勒贝格积分，他们被限制到实值的措施。我们通过引入扩展的真实的数来解除这个限制。本文定义了构成拓扑空间的任意类型的Borelσ-代数。然后，我们引入了以扩张的真实的数为测度值的测度空间。在定义了Lebesgue积分并验证了它的线性性和单调收敛性之后，我们证明了Radon-Nikodirm定理（这表明了我们框架的成熟性）。此外，我们还形式化了乘积测度，证明了Fubini定理。我们使用Isabelle多元分析中的规范积分定义勒贝格测度。最后，我们将这两种积分联系起来，并将欧氏空间上的积分与迭代积分等价。这项工作涵盖了大部分的前三章鲍尔的措施理论教科书。
Currently published HOL formalizations of measure theory concentrate on the Lebesgue integral and they are restricted to real-valued measures. We lift this restriction by introducing the extended real numbers. We define the Borelσ-algebra for an arbitrary type forming a topological space. Then, we introduce measure spaces with extended real numbers as measure values. After defining the Lebesgue integral and verifying its linearity and monotone convergence property, we prove the Radon-Nikodým theorem (which shows the maturity of our framework). Moreover, we formalize product measures and prove Fubini’s theorem. We define the Lebesgue measure using the gauge integral available in Isabelle’s multivariate analysis. Finally, we relate both integrals and equate the integral on Euclidean spaces with iterated integrals. This work covers most of the first three chapters of Bauer’s measure theory textbook.
登录
查看更多内容
Isabelle/Isar 中的局域理论规范
DOI：
--
发表时间：
2009
期刊：
Types for Proofs and Programs
影响因子：
--
作者：
Florian Haftmann;M. Wenzel
通讯作者：
M. Wenzel
匿名、信息和机器辅助证明
DOI：
--
发表时间：
2010
期刊：
影响因子：
--
作者：
A. R. Coble
通讯作者：
A. R. Coble
DOI：
--
发表时间：
2003
期刊：
影响因子：
--
作者：
Joe Hurd
通讯作者：
Joe Hurd
PVS 中的拓扑：连续数学及其应用
影响因子：
--
作者：
D. Lester
通讯作者：
D. Lester
影响因子：
0.3
作者：
N. Endou;Keiko Narita;Y. Shidama
通讯作者：
Y. Shidama