[isabelle-dev] More HOL-Analysis

[Lawrence Paulson]

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 <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.