Arrêt de service programmé du vendredi 10 juin 16h jusqu’au lundi 13 juin 9h. Pour en savoir plus
Accéder directement au contenu Accéder directement à la navigation
Rapport

A Coq Formalization of Lebesgue Integration of Nonnegative Functions

Résumé : 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.
Liste complète des métadonnées

https://hal.inria.fr/hal-03194113
Contributeur : Francois Clement Connectez-vous pour contacter le contributeur
Soumis le : mercredi 8 décembre 2021 - 16:20:07
Dernière modification le : mardi 17 mai 2022 - 03:51:30

Fichiers

RR-9401.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-03194113, version 2
  • ARXIV : 2104.05256

Relations

Citation

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.38. ⟨hal-03194113v2⟩

Partager

Métriques

Consultations de la notice

344

Téléchargements de fichiers

405