feat(l1_space): add measurability to integrable (#4170)
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).
