Sacerdoti Coen, C., and E. Tassi. “A Constructive and Formal Proof of Lebesgue’s Dominated Convergence Theorem in the Interactive Theorem Prover Matita”. Journal of Formalized Reasoning, vol. 1, no. 1, Jan. 2008, pp. 51-89, doi:10.6092/issn.1972-5787/1334.