A Coq Formalization of Lebesgue Integration of Nonnegative Functions - ParisTech Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2021

A Coq Formalization of Lebesgue Integration of Nonnegative Functions

Une formalisation en Coq de l'intégrale de Lebesgue des fonctions positives

Résumé

Integration, just as much as differentiation, is a fundamental calculus tool that is widely used in many scientific domains. Formalizing the mathematical concept of integration and the associated results in a formal proof assistant helps providing the highest confidence on the correction of numerical programs involving the use of integration, directly or indirectly. By its capability to extend the (Riemann) integral to a wide class of irregular functions, and to functions defined on more general spaces than the real line, the Lebesgue integral is considered as perfectly suited for use in mathematical fields such as probability theory, numerical mathematics, and real analysis. In this article, we present the Coq formalization of $\sigma$-algebras, measures, simple functions, and integration of nonnegative measurable functions, up to the full formal proofs of the Beppo Levi (monotone convergence) theorem and Fatou's lemma. More than a plain formalization of known literature, we present several design choices made to balance the harmony between mathematical readability and usability of Coq theorems. These results are a first milestone towards the formalization of $L^p$ spaces such as Banach spaces.
Le calcul intégral, tout comme le calcul différentiel, est un outil fondamental utilisé largement dans de nombreux domaines scientifiques. La formalisation de la notion mathématique d'intégrale et de ses propriétés dans un assistant de preuve aide à donner la plus grande confiance sur la correction de programmes numériques utilisant l'intégration, directement ou indirectement. De part sa capacité à étendre l'intégrale (de Riemann) à une large classe de fonctions irrégulières, et à des fonctions définies sur des espaces plus généraux que la droite réelle, l'intégrale de Lebesgue est considérée comme parfaitement adaptée aux domaines mathématiques tels que la théorie des probabilités, les mathématiques numériques et l'analyse réelle. Dans cet article, nous présentons la formalisation en Coq des tribus (ou $\sigma$-algèbres), des mesures, des fonctions étagées et de l'intégrale des fonctions mesurables positives, jusqu'aux preuves formelles complètes du théorème de convergence monotone de Beppo Levi et du lemme de Fatou. Plus qu'une simple formalisation de la littérature connue, nous présentons plusieurs choix de design menés pour équilibrer l'harmonie entre la lisibilité mathématique et l'ergonomie des théorèmes Coq. Ces résultats sont un premier jalon vers la formalisation des espaces $L^p$ comme espaces de Banach.
Fichier principal
Vignette du fichier
RR-9401.pdf (982.18 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03194113 , version 1 (09-04-2021)
hal-03194113 , version 2 (08-12-2021)

Identifiants

Citer

Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero. A Coq Formalization of Lebesgue Integration of Nonnegative Functions. [Research Report] RR-9401, Inria, France. 2021, pp.37. ⟨hal-03194113v1⟩
542 Consultations
573 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More