Many thanks! I’m sure a lot of tiresome work was involved.
The file I sent you began with a number of basic lemmas that belong in various
other places. Did you move them into such places, or would you like me to do
> On 23 Sep 2016, at 19:08, Johannes Hölzl <hoe...@in.tum.de> wrote:
> I just pushed the foundations to merge your measure theory port. Now
> the absolutely integrable functions are an abbreviation for Lebesgue
> integrable functions.
> Absolute integrability was only used to prove that bounded variance
> implies them (I kept this proof) and for dominated convergence. Now the
> last one is proved by using the relation with the Lebesgue (i.e.
> Bochner) integral. For this I finally proved that all HK-integrable
> functions are Lebesgue-measurable.
isabelle-dev mailing list