I just pushed the foundations to merge your measure theory port. Now
the absolutely integrable functions are an abbreviation for Lebesgue
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.
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
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
> > 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