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 that?
Larry > 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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
