Measure construction by extension in dependent type theory with application to integration

DOI10.1007/s10817-023-09671-5arXiv2209.02345OpenAlexW4385986369MaRDI QIDQ6050768

Cyril Cohen, Reynald Affeldt

Publication date: 19 September 2023

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

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

zbMATH Keywords

measure theoryLebesgue integralCoqmathematical components

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The role of the Mizar mathematical library for interactive proof development in Mizar
• The HOL Light theory of Euclidean space
• Formal adventures in convex and conical spaces
• Reconstruction of the one-dimensional Lebesgue measure
• A Coq formalization of Lebesgue integration of nonnegative functions
• Three Chapters of Measure Theory in Isabelle/HOL
• Packaging Mathematical Structures
• Canonical Big Operators
• Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
• A trustful monad for axiomatic reasoning with probability and nondeterminism
• A Machine-Checked Proof of the Odd Order Theorem
• On the Formalization of the Lebesgue Integration Theory in HOL
• Probability theory. A comprehensive course
• Formalized Haar Measure