Three Chapters of Measure Theory in Isabelle/HOL

DOI10.1007/978-3-642-22863-6_12zbMath1342.68287OpenAlexW166580360MaRDI QIDQ3088003

Armin Heller, Johannes Hölzl

Publication date: 17 August 2011

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22863-6_12

Mathematics Subject Classification ID

Classical measure theory (28Axx)

Related Items

Towards Formal Fault Tree Analysis Using Theorem Proving ⋮ A learning-based fact selector for Isabelle/HOL ⋮ Program logic for higher-order probabilistic programs in Isabelle/HOL ⋮ Formalizing Ordinal Partition Relations Using Isabelle/HOL ⋮ A Coq formalization of Lebesgue integration of nonnegative functions ⋮ Measure construction by extension in dependent type theory with application to integration ⋮ A formally verified proof of the central limit theorem ⋮ A Coq formalization of Lebesgue induction principle and Tonelli's theorem ⋮ Formal probabilistic analysis of detection properties in wireless sensor networks ⋮ Markov chains and Markov decision processes in Isabelle/HOL ⋮ Formal reasoning about finite-state discrete-time Markov chains in HOL ⋮ Formalization of real analysis: a survey of proof assistants and libraries ⋮ From types to sets by local type definition in higher-order logic ⋮ A formal proof of the expressiveness of deep learning ⋮ A formal proof of the expressiveness of deep learning ⋮ Verified analysis of random binary tree structures ⋮ Fubini's theorem for non-negative or non-positive functions ⋮ Formalization of Normal Random Variables in HOL ⋮ Formal Dependability Modeling and Analysis: A Survey ⋮ Verified interactive computation of definite integrals ⋮ An Isabelle/HOL Formalisation of Green’s Theorem ⋮ From Types to Sets by Local Type Definitions in Higher-Order Logic ⋮ An Isabelle/HOL formalisation of Green's theorem ⋮ Towards the Formal Reliability Analysis of Oil and Gas Pipelines ⋮ Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation ⋮ Formalization of Shannon's theorems ⋮ On the formalization of gamma function in HOL

Uses Software

• Isabelle
• HOL

Cites Work

• Unnamed Item
• Probabilistic guarded commands mechanized in HOL
• Local Theory Specifications in Isabelle/Isar
• Theorem Proving in Higher Order Logics
• Theorem Proving in Higher Order Logics
• Measures, Integrals and Martingales
• On the Formalization of the Lebesgue Integration Theory in HOL
• Measure and integration theory. Transl. from the German by Robert B. Burckel