Lebesgue integration. Detailed proofs to be formalized in Coq

TL;DR

This paper provides detailed, formalized proofs of Lebesgue integration and measure theory concepts to support the verification of numerical methods like the finite element method in Coq.

Contribution

It offers comprehensive, formal proofs of Lebesgue integration and measure theory results to aid formal verification in proof assistants.

Findings

Formal proofs of Lebesgue integration established

Enhanced confidence in numerical simulation correctness

Supports formal verification of finite element methods

Abstract

To obtain the highest confidence on the correction of numerical simulation programs implementing the finite element method, one has to formalize the mathematical notions and results that allow to establish the soundness of the method. Sobolev spaces are the mathematical framework in which most weak formulations of partial derivative equations are stated, and where solutions are sought. These functional spaces are built on integration and measure theory. Hence, this chapter in functional analysis is a mandatory theoretical cornerstone for the definition of the finite element method. The purpose of this document is to provide the formal proof community with very detailed pen-and-paper proofs of the main results from integration and measure theory.