Contributors: Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA); 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)-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)-Centre Inria de l'Université Paris-Saclay; Centre Inria de Saclay; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre Inria de Saclay; Institut National de Recherche en Informatique et en Automatique (Inria); Simulation for the Environment: Reliable and Efficient Numerical Algorithms (SERENA); Centre 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 nationale des ponts et chaussées (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; This work was partly supported by the Paris Île-de-France Region (DIM RFSI MILC). This work was partly supported by Labex DigiCosme (project ANR-11-LABEX-0045-DIGICOSME) operated by ANR as part of the program “Investissement d’Avenir” Idex Paris-Saclay (ANR-11-IDEX-0003-02).This work was partly supported by the European Research Council (ERC) under the EuropeanUnion’s Horizon 2020 Research and Innovation Programme – Grant Agreement n◦810367.; Inria, France; ANR-11-LABX-0045,DIGICOSME,Mondes numériques: Données, programmes et architectures distribués(2011); ANR-11-IDEX-0003,IPS,Idex Paris-Saclay(2011); European Project: 810367,ERC-2018-SyG,ERC-2018-SyG,EMC2(2019)
نبذة مختصرة : Integration, just as much as differentiation, is a fundamental calculus tool that is widely used in many scientific domains. Formalizing the mathematical concept of integration and the associated results in a formal proof assistant helps in providing the highest confidence on the correctness of numerical programs involving the use of integration, directly or indirectly. By its capability to extend the (Riemann) integral to a wide class of irregular functions, and to functions defined on more general spaces than the real line, the Lebesgue integral is perfectly suited for use in mathematical fields such as probability theory, numerical mathematics, and real analysis. In this article, we present the Coq formalization of $\sigma$-algebras, measures, simple functions, and integration of nonnegative measurable functions, up to the full formal proofs of the Beppo Levi (monotone convergence) theorem and Fatou's lemma. More than a plain formalization of the known literature, we present several design choices made to balance the harmony between mathematical readability and usability of Coq theorems. These results are a first milestone toward the formalization of $L^p$~spaces such as Banach spaces. ; 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), ...
Processing Request
No Comments.