Measure Construction by Extension in Dependent Type Theory with Application to Integration

TL;DR

This paper formalizes measure and integration theory in Coq, constructing Lebesgue measure via extension of measures over semirings, and extends existing tools to support infinite sums and extended real numbers.

Contribution

It introduces a formalization of Lebesgue measure by extension in dependent type theory, integrating with Mathematical Components and applying Hierarchy-Builder for hierarchy formalization.

Findings

Formalization of Lebesgue measure in Coq using extension over semirings

Extension of Mathematical Components to support infinite sums and extended reals

Development of a compatible formalization of Lebesgue integration

Abstract

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.