Re: [mizar] Formalization of the Lebesgue measure in Mizar

Hello Adam,

On Mon, May 23, 2016 at 10:06 AM, <adamn@math.uwb.edu.pl> wrote:

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

I read this paper, which details the work on MEASURE1..6 (Lebesgue theory of measure and integration), before starting my project.

Afterwards Shidama's group added MEASURE7 (outer Lebesgue measure on R), and MEASURE8 (completely-additive measures extend to measures), and Endou added MEASURE9 (pre-measures extend to measures).

This last one is in the same direction as me, and will (as I understand) allow defining the Borel measure using half-open intervals, and then the Lebesgue measure as its closure.

But I'm itching already to have volumes of sets in R^n, so I'm only interested in some very basic regularity properties of the Lebesgue measure, and in Fubini's theorem. And I hope to be able to avoid having duplicates of theorems future articles of the MEASURE series.

Amir