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 <hoe...@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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev