A Coq Formalization of Lebesgue Induction Principle and Tonelli’s Theorem
In: Formal Methods ISBN: 9783031274800 Proceedings of the 25th International Symposium on Formal Methods 25th International Symposium on Formal Methods (FM 2023) 25th International Symposium on Formal Methods (FM 2023), Mar 2023, Lübeck, Germany. pp.39--55, ⟨10.1007/978-3-031-27481-7_4⟩ FM 2023-25th International Symposium on Formal Methods FM 2023-25th International Symposium on Formal Methods, Mar 2023, Lübeck, Germany; (2023)
Online
unknown
Zugriff:
International audience 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.
| Titel: |
A Coq Formalization of Lebesgue Induction Principle and Tonelli’s Theorem
|
|---|---|
| Autor/in / Beteiligte Person: | Boldo, Sylvie ; Clément, François ; Martin, Vincent ; Mayero, Micaela ; Mouhcine, Houda ; Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA) ; Inria Saclay - Ile de France ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF) ; Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay) ; Simulation for the Environment: Reliable and Efficient Numerical Algorithms (SERENA) ; Inria de Paris ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) ; Centre d'Enseignement et de Recherche en Mathématiques et Calcul Scientifique (CERMICS) ; École des Ponts ParisTech (ENPC) ; Laboratoire Métallographie et Analyse Chimique (LMAC) ; Commissariat à l'énergie atomique et aux énergies alternatives (CEA) ; Laboratoire d'Informatique de Paris-Nord (LIPN) ; Centre National de la Recherche Scientifique (CNRS)-Université Sorbonne Paris Nord ; European Project: 810367,EMC2(2019) |
| Link: | |
| Quelle: | Formal Methods ISBN: 9783031274800 Proceedings of the 25th International Symposium on Formal Methods 25th International Symposium on Formal Methods (FM 2023) 25th International Symposium on Formal Methods (FM 2023), Mar 2023, Lübeck, Germany. pp.39--55, ⟨10.1007/978-3-031-27481-7_4⟩ FM 2023-25th International Symposium on Formal Methods FM 2023-25th International Symposium on Formal Methods, Mar 2023, Lübeck, Germany; (2023) |
| Veröffentlichung: | Springer International Publishing, 2023 |
| Medientyp: | unknown |
| ISBN: | 978-3-031-27480-0 (print) |
| DOI: | 10.1007/978-3-031-27481-7_4 |
| Schlagwort: |
|
| Sonstiges: |
|