Formalization of Measure and Lebesgue Integration over Extended Reals in HOL

Technical Report

Abstract
Measure theory and Lebesgue integration are fundamental tools in a wide range of mathematical theories such probability and information theory. Consequently, a formalization of these theories is highly required to be able to tackle numerous application using a theorem prover. This report is primarily focused towards overcoming the shortcomings of previous formalizations to raise the state-of-the-art in higher-order-logic formalization of measure and Lebesgue integration from the existing level, where they are applicable only to isolated facets, to a level allowing formal analysis of contemporary engineering and scientific problems. In this regard, we propose to develop a rigorous higher-order-logic formalization of measure, Lebesgue integration and probability theories over the extended real numbers, which are real numbers extended with positive and negative infinity. We also formalize the Radon-Nikodym derivative and prove some of its properties using the HOL theorem prover.

Files

• Technical Report: PDF File