A Coq Formalization of Lebesgue Induction Principle and Tonelli's Theorem (original) (raw)

Résumé

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.

Domaines

HAL

A comme version hal-03564379 Rapport Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine. Lebesgue Induction and Tonelli's Theorem in Coq. [Research Report] RR-9457, Institut National de Recherche en Informatique et en Automatique (INRIA). 2023, pp.17. ⟨hal-03564379v2⟩

Dates et versions

hal-03889276 , version 1 (07-12-2022)

hal-03889276 , version 2 (16-12-2022)

Licence

Identifiants

Citer

Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine. A Coq Formalization of Lebesgue Induction Principle and Tonelli's Theorem. 25th International Symposium on Formal Methods (FM 2023), Mar 2023, Lübeck, Germany. pp.39--55, ⟨10.1007/978-3-031-27481-7_4⟩. ⟨hal-03889276v2⟩

1358 Consultations

952 Téléchargements

Altmetric