Lebesgue Induction and Tonelli's Theorem in Coq

TL;DR

This paper formalizes Lebesgue integration and Tonelli's theorem within Coq, enabling rigorous proof development in measure theory and integration, with a focus on product spaces and iterated integrals.

Contribution

It introduces a formalization of product measures, sigma-algebras, and the Tonelli theorem in Coq, along with a Lebesgue induction principle for nonnegative measurable functions.

Findings

Formal definitions of product sigma-algebras and measures in Coq

Proof of Tonelli's theorem for nonnegative measurable functions

Development of a Lebesgue induction principle for nonnegative functions

Abstract

Lebesgue integration is a well-known mathematical tool, used for instance in probability theory, real analysis, and numerical mathematics. Thus its formalization in a proof assistant is to be designed to fit different goals and projects. Once Lebesgue integral is formally defined and the first lemmas are proved, the question of the convenience of the formalization naturally arises. To check it, a useful extension is the Tonelli theorem, stating that the (double) integral of a nonnegative measurable function of two variables can be computed by iterated integrals, and allowing to switch the order of integration. Therefore, we need to define and prove results on product spaces, hoping that they can easily derive from the existing ones on a single space. This article describes the formal definition and proof in Coq of product $\sigma$-algebras, product measures and their uniqueness, the construction of iterated integrals, up to the Tonelli theorem. We also advertise the \emph{Lebesgue induction principle} provided by an inductive type for {\nonnegative} measurable functions.