Sciweavers

Share
ITP
2010

On the Formalization of the Lebesgue Integration Theory in HOL

8 years 7 months ago
On the Formalization of the Lebesgue Integration Theory in HOL
Lebesgue integration is a fundamental concept in many mathematical theories, such as real analysis, probability and information theory. Reported higher-order-logic formalizations of the Lebesgue integral either do not include, or have a limited support for the Borel algebra, which is the canonical sigma algebra used on any metric space over which the Lebesgue integral is defined. In this paper, we overcome this limitation by presenting a formalization of the Borel sigma algebra that can be used on any metric space, such as the complex numbers or the n-dimensional Euclidean space. Building on top of this framework, we have been able to prove some key Lebesgue integral properties, like its linearity and monotone convergence. Furthermore, we present the formalization of the “almost everywhere” relation and prove that the Lebesgue integral does not distinguish between functions which differ on a null set as well as other important results based on this concept. As applications, we pr...
Tarek Mhamdi, Osman Hasan, Sofiène Tahar
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2010
Where ITP
Authors Tarek Mhamdi, Osman Hasan, Sofiène Tahar
Comments (0)
books