TY - JOUR
AU - Sacerdoti Coen, Claudio
AU - Tassi, Enrico
PY - 2008/01/01
Y2 - 2023/02/08
TI - A constructive and formal proof of Lebesgue’s Dominated Convergence Theorem in the interactive theorem prover Matita
JF - Journal of Formalized Reasoning
JA - JFR
VL - 1
IS - 1
SE - Articles
DO - 10.6092/issn.1972-5787/1334
UR - https://jfr.unibo.it/article/view/1334
SP - 51-89
AB - We 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.
ER -