Dear Amir, Quoting Amir Livne Bar-on <amir.livne.baron@gmail.com>:
My working directory is publicly available at https://github.com/amirlb/mizar-lebesgue-measure 1. Is this really not covered? AFAICT, the Lebesgue measure only appears in two definitions in the end of MEASURE7. If it is covered, or if anyone else is in the process of formalizing this, I'll pick another area.
Have you looked at the MEASFUNC series of articles developed by prof. Shidama's group? It seems that these articles use a slightly more general setting to Lebesgue integrability.
There is also a paper you might be interested to see: http://logika.uwb.edu.pl/studies/download.php?volid=23&artid=se&format=PDF Best regards, Adam