A Coq Formalization of the Bochner integral ; Une formalisation en Coq de l'intégrale de Bochner
In: https://inria.hal.science/hal-03516749 ; [Research Report] RR-9456, Inria Saclay - Île de France; Inria de Paris. 2022, 2022
Online
report
Zugriff:
The Bochner integral is a generalization of the Lebesgue integral, for functions taking their values in a Banach space. Therefore, both its mathematical definition and its formalization in the Coq proof assistant are more challenging as we cannot rely on the properties of real numbers. Our contributions include an original formalization of simple functions, Bochner integrability defined by a dependent type, and the construction of the proof of the integrability of measurable functions under mild hypotheses (weak separability). Then, we define the Bochner integral and prove several theorems, including dominated convergence and the equivalence with an existing formalization of Lebesgue integral for nonnegative functions. ; L'intégrale de Bochner est une généralisation de l'intégrale de Lebesgue pour des fonctions à valeurs dans un espace de Banach. Sa définition mathématique et sa formalisation dans l'assistant de preuve Coq en sont donc plus difficiles puisque l'on ne peut pas s'appuyer sur les propriétés des nombres réels. Nos contributions incluent une formalisation originale des fonctions simples, l'intégrabilité de Bochner définie par un type dépendant, et la construction de la preuve de l'intégrabilité de fonctions mesurables sous une hypothèse de séparabilité faible. Puis, nous définissons l'intégrale de Bochner et prouvons plusieurs théorèmes, dont la convergence dominée et l'équivalence avec une formalisation préexistante de l'intégrale de Lebesgue pour les fonctions mesurables positives.
Titel: |
A Coq Formalization of the Bochner integral ; Une formalisation en Coq de l'intégrale de Bochner
|
---|---|
Autor/in / Beteiligte Person: | Boldo, Sylvie ; Clément, François ; Leclerc, Louise ; 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) ; Département de Mathématiques et Applications - ENS Paris (DMA) ; École normale supérieure - Paris (ENS-PSL) ; Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Centre National de la Recherche Scientifique (CNRS) ; Inria Saclay - Île de France |
Link: | |
Zeitschrift: | https://inria.hal.science/hal-03516749 ; [Research Report] RR-9456, Inria Saclay - Île de France; Inria de Paris. 2022, 2022 |
Veröffentlichung: | HAL CCSD, 2022 |
Medientyp: | report |
Schlagwort: |
|
Sonstiges: |
|