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).
leanprover-community · Sep 22, 2020 · b4641ef · b4641ef
1 parent 2ae199f
commit b4641ef
Show file tree

Hide file tree

Showing 6 changed files with 684 additions and 611 deletions.
diff --git a/src/measure_theory/bochner_integration.lean b/src/measure_theory/bochner_integration.lean
diff --git a/src/measure_theory/borel_space.lean b/src/measure_theory/borel_space.lean
@@ -741,7 +741,7 @@ namespace continuous_linear_map
 
 variables [measurable_space α]
 variables {𝕜 : Type*} [normed_field 𝕜]
-variables {E : Type*} [normed_group E] [normed_space 𝕜 E] [measurable_space E] [borel_space E]
+variables {E : Type*} [normed_group E] [normed_space 𝕜 E] [measurable_space E] [opens_measurable_space E]
 variables {F : Type*} [normed_group F] [normed_space 𝕜 F] [measurable_space F] [borel_space F]
 
 protected lemma measurable (L : E →L[𝕜] F) : measurable L :=

diff --git a/src/measure_theory/interval_integral.lean b/src/measure_theory/interval_integral.lean