[isabelle-dev] More HOL-Analysis
lp15 at cam.ac.uk
Sun Sep 25 15:57:29 CEST 2016
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?
> On 23 Sep 2016, at 19:08, Johannes Hölzl <hoelzl at 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.
More information about the isabelle-dev