A Coq formalization of Lebesgue induction principle and Tonelli's theorem

DOI10.1007/978-3-031-27481-7_4zbMath1529.68315OpenAlexW4310894270MaRDI QIDQ6174524

Vincent Martin, Houda Mouhcine, François Clément, Sylvie Boldo, Micaela Mayero

Publication date: 17 August 2023

Published in: Formal Methods (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-031-27481-7_4

zbMATH Keywords

measure theoryformal proofCoqLebesgue integrationTonelli's theorem

Mathematics Subject Classification ID

Integrals of Riemann, Stieltjes and Lebesgue type (26A42) Integration of real functions of several variables: length, area, volume (26B15) Measures and integrals in product spaces (28A35) Formalization of mathematics in connection with theorem provers (68V20)

Cites Work

• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• The HOL Light theory of Euclidean space
• Coquelicot: a user-friendly library of real analysis for Coq
• Fubini's theorem
• A Coq formalization of Lebesgue integration of nonnegative functions
• Formalization of real analysis: a survey of proof assistants and libraries
• Three Chapters of Measure Theory in Isabelle/HOL
• Measure Theory
• Formalized Haar Measure
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A Coq formalization of Lebesgue induction principle and Tonelli's theorem