[isabelle-dev] More HOL-Analysis

[Johannes Hölzl]

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.

 - Johannes

changeset:   63941:f353674c2528
tag:         tip
user:        hoelzl
date:        Fri Sep 23 18:34:34 2016 +0200
summary:     move absolutely_integrable_on to Equivalence_Lebesgue_Henstock_Integration, now based on the Lebesgue integral

changeset:   63940:0d82c4c94014
user:        hoelzl
date:        Fri Sep 23 10:26:04 2016 +0200
summary:     prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions



Am Mittwoch, den 21.09.2016, 15:29 +0100 schrieb Lawrence Paulson:
> Convex_Euclidean_Space is the largest file in Analysis, more than
> half a megabyte, so rather than combining the files it would be good
> to split them up even more.
> 
> I admit, I have been putting in a lot of new material and trying to
> put things in sensible places, but with no global overview of the
> development.
> 
> Larry
> 
> > 
> > On 16 Sep 2016, at 16:20, Johannes Hölzl <hoelzl at in.tum.de> wrote:
> > 
> > Also Brian's theories are still in HOL-Library (i.e. Inner_Product
> > and
> > Product_Vector). I would also move Convex back. It was split of
> > Convex_Euclidean_Space to be usable in Probability. Which is not
> > necessary anymore as Probability is based on Analysis.
> > 
> > I will move these files.