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 has not yet been formalized in type theory-based proof assistants: by extension of a measure over a semiring of sets. We achieve this formalization by leveraging on existing techniques from the Mathematics 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.

翻译：我们报告了在Coq证明辅助工具中对测度与积分理论的原创形式化工作。我们遵循一种尚未在基于类型理论的证明辅助工具中形式化的标准构造——通过集合半环上的测度扩展——构建了勒贝格测度。该形式化借助数学组件项目中的现有技术实现。我们阐述了如何扩展数学组件的迭代算子及分析数学结构，以支持无穷级数与扩展实数。我们引入了测度论的新数学结构，并顺便提供了层级构造器（一种用于数学结构层级形式化的通用工具）的具象应用实例。这一测度论形式化为与数学组件项目兼容的勒贝格积分的新形式化奠定了基础。