[Merged by Bors] - feat(l1_space): add measurability to integrable

[fpvandoorn]

This PR defines integrable such that integrable implies measurable. The old version is called has_finite_integral.

This allows us to drop many measurability conditions from lemmas that also require integrability.
There are some lemmas that have extra measurability conditions, if it has integrable as conclusion without corresponding measurable hypothesis.
There are many results that require an additional [measurable_space E] hypothesis, and some that require [borel_space E] or [second_countable_space E] (usually when using that addition is measurable).

---

[fpvandoorn]

The predicate integrable_on currently still implies that the function is measurable everywhere. Potentially we could choose to say that the function is only measurable after restricting to the set in question.

[urkud]

The predicate integrable_on currently still implies that the function is measurable everywhere. Potentially we could choose to say that the function is only measurable after restricting to the set in question.

I think that the best approach to this is to use measurability w.r.t. null_measurable as most textbooks do.

[urkud]

I support usage of the new definition. I did not go through the whole file but I trust that @fpvandoorn did not introduce any large regressions. @sgouezel ?

[PatrickMassot]

Sébastien is happy with this change
bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests