chore(measure_theory/function): split files strongly_measurable and s…

…imple_func_dense (#12711)

The files `strongly_measurable` and `simple_func_dense` contain general results, and results pertaining to the `L^p` space. We move the results regarding `L^p` to new files, to make sure that the main parts of the files can be imported earlier in the hierarchy. This is needed for a forthcoming integral refactor.

src/measure_theory/function/ae_eq_of_integral.lean

@@ -5,7 +5,7 @@ Authors: Rémy Degenne
 -/
 
 import analysis.normed_space.dual
-import measure_theory.function.strongly_measurable
+import measure_theory.function.strongly_measurable_lp
 import measure_theory.integral.set_integral
 
 /-! # From equality of integrals to equality of functions

src/measure_theory/function/continuous_map_dense.lean

@@ -5,7 +5,7 @@ Authors: Heather Macbeth
 -/
 
 import measure_theory.measure.regular
-import measure_theory.function.simple_func_dense
+import measure_theory.function.simple_func_dense_lp
 import topology.urysohns_lemma
 
 /-!

src/measure_theory/function/strongly_measurable.lean

@@ -16,7 +16,6 @@ of those simple functions have finite measure.
 If the target space has a second countable topology, strongly measurable and measurable are
 equivalent.
 
-Functions in `Lp` for `0 < p < ∞` are finitely strongly measurable.
 If the measure is sigma-finite, strongly measurable and finitely strongly measurable are equivalent.
 
 The main property of finitely strongly measurable functions is
@@ -39,9 +38,6 @@ results for those functions as if the measure was sigma-finite.
 
 * `ae_fin_strongly_measurable.exists_set_sigma_finite`: there exists a measurable set `t` such that
   `f =ᵐ[μ.restrict tᶜ] 0` and `μ.restrict t` is sigma-finite.
-* `mem_ℒp.ae_fin_strongly_measurable`: if `mem_ℒp f p μ` with `0 < p < ∞`, then
-  `ae_fin_strongly_measurable f μ`.
-* `Lp.fin_strongly_measurable`: for `0 < p < ∞`, `Lp` functions are finitely strongly measurable.
 
 ## References
 
@@ -565,33 +561,6 @@ lemma ae_fin_strongly_measurable_iff_ae_measurable {m0 : measurable_space α} (
   ae_fin_strongly_measurable f μ ↔ ae_measurable f μ :=
 by simp_rw [ae_fin_strongly_measurable, ae_measurable, fin_strongly_measurable_iff_measurable]
 
-lemma mem_ℒp.fin_strongly_measurable_of_measurable (hf : mem_ℒp f p μ) (hf_meas : measurable f)
-  (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) :
-  fin_strongly_measurable f μ :=
-begin
-  let fs := simple_func.approx_on f hf_meas set.univ 0 (set.mem_univ _),
-  refine ⟨fs, _, _⟩,
-  { have h_fs_Lp : ∀ n, mem_ℒp (fs n) p μ, from simple_func.mem_ℒp_approx_on_univ hf_meas hf,
-    exact λ n, (fs n).measure_support_lt_top_of_mem_ℒp (h_fs_Lp n) hp_ne_zero hp_ne_top, },
-  { exact λ x, simple_func.tendsto_approx_on hf_meas (set.mem_univ 0) (by simp), },
-end
-
-lemma mem_ℒp.ae_fin_strongly_measurable (hf : mem_ℒp f p μ) (hp_ne_zero : p ≠ 0)
-  (hp_ne_top : p ≠ ∞) :
-  ae_fin_strongly_measurable f μ :=
-⟨hf.ae_measurable.mk f,
-  ((mem_ℒp_congr_ae hf.ae_measurable.ae_eq_mk).mp hf).fin_strongly_measurable_of_measurable
-    hf.ae_measurable.measurable_mk hp_ne_zero hp_ne_top,
-  hf.ae_measurable.ae_eq_mk⟩
-
-lemma integrable.ae_fin_strongly_measurable (hf : integrable f μ) :
-  ae_fin_strongly_measurable f μ :=
-(mem_ℒp_one_iff_integrable.mpr hf).ae_fin_strongly_measurable one_ne_zero ennreal.coe_ne_top
-
-lemma Lp.fin_strongly_measurable (f : Lp G p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) :
-  fin_strongly_measurable f μ :=
-(Lp.mem_ℒp f).fin_strongly_measurable_of_measurable (Lp.measurable f) hp_ne_zero hp_ne_top
-
 end second_countable_topology
 
 lemma measurable_uncurry_of_continuous_of_measurable {α β ι : Type*} [emetric_space ι]

src/measure_theory/function/strongly_measurable_lp.lean

@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2022 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+
+import measure_theory.function.simple_func_dense_lp
+import measure_theory.function.strongly_measurable
+
+/-!
+# Finitely strongly measurable functions in `Lp`
+
+Functions in `Lp` for `0 < p < ∞` are finitely strongly measurable.
+
+## Main statements
+
+* `mem_ℒp.ae_fin_strongly_measurable`: if `mem_ℒp f p μ` with `0 < p < ∞`, then
+  `ae_fin_strongly_measurable f μ`.
+* `Lp.fin_strongly_measurable`: for `0 < p < ∞`, `Lp` functions are finitely strongly measurable.
+
+## References
+
+* Hytönen, Tuomas, Jan Van Neerven, Mark Veraar, and Lutz Weis. Analysis in Banach spaces.
+Springer, 2016.
+-/
+
+open measure_theory filter topological_space function
+open_locale ennreal topological_space measure_theory
+
+namespace measure_theory
+
+local infixr ` →ₛ `:25 := simple_func
+
+variables {α G : Type*} {p : ℝ≥0∞} {m m0 : measurable_space α} {μ : measure α}
+  [normed_group G] [measurable_space G] [borel_space G] [second_countable_topology G]
+  {f : α → G}
+
+lemma mem_ℒp.fin_strongly_measurable_of_measurable (hf : mem_ℒp f p μ) (hf_meas : measurable f)
+  (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) :
+  fin_strongly_measurable f μ :=
+begin
+  let fs := simple_func.approx_on f hf_meas set.univ 0 (set.mem_univ _),
+  refine ⟨fs, _, _⟩,
+  { have h_fs_Lp : ∀ n, mem_ℒp (fs n) p μ, from simple_func.mem_ℒp_approx_on_univ hf_meas hf,
+    exact λ n, (fs n).measure_support_lt_top_of_mem_ℒp (h_fs_Lp n) hp_ne_zero hp_ne_top, },
+  { exact λ x, simple_func.tendsto_approx_on hf_meas (set.mem_univ 0) (by simp), },
+end
+
+lemma mem_ℒp.ae_fin_strongly_measurable (hf : mem_ℒp f p μ) (hp_ne_zero : p ≠ 0)
+  (hp_ne_top : p ≠ ∞) :
+  ae_fin_strongly_measurable f μ :=
+⟨hf.ae_measurable.mk f,
+  ((mem_ℒp_congr_ae hf.ae_measurable.ae_eq_mk).mp hf).fin_strongly_measurable_of_measurable
+    hf.ae_measurable.measurable_mk hp_ne_zero hp_ne_top,
+  hf.ae_measurable.ae_eq_mk⟩
+
+lemma integrable.ae_fin_strongly_measurable (hf : integrable f μ) :
+  ae_fin_strongly_measurable f μ :=
+(mem_ℒp_one_iff_integrable.mpr hf).ae_fin_strongly_measurable one_ne_zero ennreal.coe_ne_top
+
+lemma Lp.fin_strongly_measurable (f : Lp G p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) :
+  fin_strongly_measurable f μ :=
+(Lp.mem_ℒp f).fin_strongly_measurable_of_measurable (Lp.measurable f) hp_ne_zero hp_ne_top
+
+end measure_theory

src/measure_theory/integral/set_to_l1.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Zhouhang Zhou, Yury Kudryashov, Sébastien Gouëzel, Rémy Degenne
 -/
-import measure_theory.function.simple_func_dense
+import measure_theory.function.simple_func_dense_lp
 
 /-!
 # Extension of a linear function from indicators to L1