Lebesgue Induction and Tonelli's Theorem in Coq - Université Sorbonne Paris Nord Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2023

Lebesgue Induction and Tonelli's Theorem in Coq

Induction de Lebesgue et théorème de Tonelli en Coq

Résumé

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 the 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 Tonelli's 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. 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 Tonelli's theorem. We also advertise the Lebesgue induction principle provided by an inductive type for nonnegative measurable functions.
L'intégrale de Lebesgue est un outil mathématique bien connu, utilisé par exemple en théorie des probabilités, en analyse réelle et pour les mathématiques appliquées. Sa formalisation dans un assistant de preuve doit donc être conçue pour s'adapter à des buts et des projets différents. Une fois que l'intégrale de Lebesgue est définie formellement et que les premiers lemmes sont prouvés, il se pose naturellement la question de la commodité d'usage de la formalisation. Pour la contrôler, le théorème de Tonelli est une extension utile. Ce dernier établi que l'intégrale (double) d'une fonction mesurable positive de deux variables peut être calculée par des intégrales itérées et que l'on peut intervertir l'ordre d'intégration. Cet article décrit la définition formelle et la preuve en Coq des tribus produits, de l'existence et l'unicité des mesures produits, de la construction des intégrales itérées, jusqu'au théorème de Tonelli. Nous mettons également en avant le principe d'induction de Lebesgue, obtenu à partir d'un type inductif pour les fonctions mesurables positives.
Fichier principal
Vignette du fichier
RR-9457.pdf (754.61 Ko) Télécharger le fichier
pagei.pdf (78.34 Ko) Télécharger le fichier
rrpage1.pdf (178.3 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03564379 , version 1 (10-02-2022)
hal-03564379 , version 2 (16-01-2023)

Identifiants

Citer

Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine. Lebesgue Induction and Tonelli's Theorem in Coq. [Research Report] RR-9457, Institut National de Recherche en Informatique et en Automatique (INRIA). 2023, pp.17. ⟨hal-03564379v2⟩

Relations

468 Consultations
216 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More