Lebesgue Induction and Tonelli's Theorem in Coq
| Autor: | Boldo, Sylvie, Clément, François, Martin, Vincent, Mayero, Micaela, Mouhcine, Houda |
|---|---|
| Přispěvatelé: | 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 de Mathématiques Appliquées de Compiègne (LMAC), Université de Technologie de Compiègne (UTC), Laboratoire d'Informatique de Paris-Nord (LIPN), Centre National de la Recherche Scientifique (CNRS)-Université Sorbonne Paris Nord, Institut National de Recherche en Informatique et en Automatique (INRIA), European Project: 810367,EMC2(2019) |
| Jazyk: | angličtina |
| Rok vydání: | 2023 |
| Předmět: |
Tonelli theorem
Théorie de la mesure Lebesgue integration Preuve formelle Intégrale de Lebesgue Formal proof Coq Measure theory [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] [MATH.MATH-CA]Mathematics [math]/Classical Analysis and ODEs [math.CA] [MATH.MATH-FA]Mathematics [math]/Functional Analysis [math.FA] Théorème de Tonelli |
| Zdroj: | [Research Report] RR-9457, Institut National de Recherche en Informatique et en Automatique (INRIA). 2023, pp.17 [Research Report] RR-9457, Institut National de Recherche en Informatique et en Automatique (INRIA). 2022, pp.17 [Research Report] RR-9457, Institut National de Recherche en Informatique et en Automatique (INRIA). 2022, pp.16 |
| Popis: | 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 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 the Tonelli 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. Therefore, we need to define and prove results on product spaces, hoping that they can easily derive from the existing ones on a single space. 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 the Tonelli theorem. We also advertise the \emph{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. Nous devons donc définir et prouver des résultats sur les espaces produits, en espérant qu'ils peuvent facilement découler des résultats existants sur un espace simple. Cet article décrit la définition formelle et la preuve en Coq des tribus produits, des 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 annonçons également le \emph{principe d'induction de Lebesgue}, qui est obtenu à partir d'un type inductif pour les fonctions mesurables positives. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|