论文标题
通过扩展的依赖类型理论测量构建，并应用于集成
Measure Construction by Extension in Dependent Type Theory with Application to Integration
论文作者
论文摘要
我们在COQ证明助手中报告了对度量和整合理论的原始形式化。我们遵循尚未根据依赖类型理论在证明助理中正式化的标准结构来建立Lebesgue度量：通过将措施扩展到集合的半度性上。我们通过利用数学组件项目的现有技术来实现这种形式化。我们解释了如何扩展数学组件的迭代运算符和数学结构，以提供对无限总和和扩展实数的支持。我们介绍了量度理论的新数学结构，并偶然地提供了层次结构构建器的说明性，具体的应用，这是一种用于形式化数学结构层次结构的通用工具。衡量理论的这种形式化为与数学成分项目兼容的Lebesgue集成的新形式化提供了基础。
We report on an original formalization of measure and integration theory in the Coq proof assistant. We build the Lebesgue measure following a standard construction that had not yet been formalized in proof assistants based on dependent type theory: by extension of a measure over a semiring of sets. We achieve this formalization by leveraging on existing techniques from the Mathematical Components project. We explain how we extend Mathematical Components' iterated operators and mathematical structures for analysis to provide support for infinite sums and extended real numbers. We introduce new mathematical structures for measure theory and incidentally provide an illustrative, concrete application of Hierarchy-Builder, a generic tool for the formalization of hierarchies of mathematical structures. This formalization of measure theory provides the basis for a new formalization of the Lebesgue integration compatible with the Mathematical Components project.
