A constructive and formal proof of Lebesgue’s Dominated Convergence Theorem in the interactive theorem prover Matita
AbstractWe present a formalisation of a constructive proof of Lebesgue’s Dominated Convergence Theorem given by the Sacerdoti Coen and Zoli in [CSCZ]. The proof is done in the abstract setting of ordered uniformities, also introduced by the two authors as a simplification of Weber’s lattice uniformities given in [Web91, Web93]. The proof is fully constructive, in the sense that it is done in Bishop’s style and, under certain assumptions, it is also fully predicative. The formalisation is done in the Calculus of (Co)Inductive Constructions using the interactive theorem prover Matita [ASTZ07]. It exploits some peculiar features of Matita and an advanced technique to represent algebraic hierarchies previously introduced by the authors in [ST07]. Moreover, we introduce a new technique to cope with duality to halve the formalisation effort.
How to Cite
Sacerdoti Coen, C., & Tassi, E. (2008). A constructive and formal proof of Lebesgue’s Dominated Convergence Theorem in the interactive theorem prover Matita. Journal of Formalized Reasoning, 1(1), 51–89. https://doi.org/10.6092/issn.1972-5787/1334
Copyright (c) 2008 Claudio Sacerdoti Coen, Enrico Tassi
Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.