A Coq formalization of Lebesgue integration of nonnegative functions

DOI10.1007/s10817-021-09612-0OpenAlexW3215924521MaRDI QIDQ2673304

Micaela Mayero, Vincent Martin, Florian Faissole, Sylvie Boldo, François Clément

Publication date: 9 June 2022

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2104.05256

zbMATH Keywords

measure theoryformal proofCoqLebesgue integration

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Measure construction by extension in dependent type theory with application to integration ⋮ A Coq formalization of Lebesgue induction principle and Tonelli's theorem

Uses Software

• Coq
• Isabelle/HOL
• PVS
• Flocq
• FEAPpv
• Coquelicot
• Lean
• mathlib

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• Isabelle/HOL. A proof assistant for higher-order logic
• Theory and practice of finite elements.
• Coquelicot: a user-friendly library of real analysis for Coq
• Trusting computations: a mechanized proof from partial differential equations to actual program
• Fubini's theorem
• An Isabelle/HOL Formalisation of Green’s Theorem
• The Flow of ODEs
• Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
• Formalization of real analysis: a survey of proof assistants and libraries
• Three Chapters of Measure Theory in Isabelle/HOL
• Generalized ordinary differential equations and continuous dependence on a parameter
• The Lean Theorem Prover (System Description)
• Functional Analysis and the Feynman Operator Calculus
• Canonical Big Operators
• Probability
• The Picard Algorithm for Ordinary Differential Equations in Coq
• Measure Theory
• Fundamentals of Nonparametric Bayesian Inference
• On the Formalization of the Lebesgue Integration Theory in HOL
• Introduction to nonparametric estimation

This page was built for publication: A Coq formalization of Lebesgue integration of nonnegative functions