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

DOI10.1007/978-3-031-27481-7_4MaRDI QIDQ6174524zbMATH OpenOpenAlexFDO

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

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

Coqformal proofLebesgue integrationmeasure theoryTonelli'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)

Recommendations

• A Coq formalization of Lebesgue integration of nonnegative functions
• On the formalization of the Lebesgue integration theory in HOL
• A constructive and formal proof of Lebesgue's dominated convergence theorem in the interactive theorem prover Matita
• Three chapters of measure theory in Isabelle/HOL
• Theorem Proving in Higher Order Logics

Cites work

• A Coq formalization of Lebesgue integration of nonnegative functions
• Coquelicot: a user-friendly library of real analysis for Coq
• Formalization of real analysis: a survey of proof assistants and libraries
• Formalized Haar Measure
• Fubini's theorem
• scientific article; zbMATH DE number 5841426 (Why is no real title available?)
• scientific article; zbMATH DE number 6146040 (Why is no real title available?)
• scientific article; zbMATH DE number 3240665 (Why is no real title available?)
• Measure theory
• The HOL Light theory of Euclidean space
• Three chapters of measure theory in Isabelle/HOL
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program

Cited in

(6)

• Mac Lane's comparison theorem for the Kleisli construction formalized in Coq
• A Coq formalization of Lebesgue integration of nonnegative functions
• Proving tight bounds on univariate expressions with elementary functions in Coq
• Coinductive formulas and a many-sorted interpolation theorem
• Integrals within integrals: a formalization of the Gagliardo-Nirenberg-Sobolev inequality
• An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6174524)