Define Bochner integrals over subsets and measures

[urkud]

Currently we only have Bochner integral w.r.t. the "canonical" measure. It would be nice to add

• integral w.r.t. a measure, see measure.integral for an example. Probably measure.integral should be renamed to measure.lintegral for consistency, and Bochner integral should take the name measure.integral.
• integral over a subset; either use restriction of a measure to a subset, or integrate an ite. Probably we'll need a proof of the fact that these two approaches are equivalent. See also Define boole? #1472.
• as a special case, it would be nice to have real.integral f a b. It should be the integral over [a, b] or [a, b) if a ≤ b, and -real.integral f b a otherwise. This way for a functions integrable on all finite intervals, real.integral will be linear in f and additive in a and b.

[robertylewis]

@urkud , @sgouezel claims on Zulip that you've finished all this, so can the issue be closed? 😄