Finitely strongly measurable functions in Lp

Functions in Lp for 0 < p < ∞ are finitely strongly measurable.

Main statements

• MemLp.aefinStronglyMeasurable: if MemLp f p μ with 0 < p < ∞, then AEFinStronglyMeasurable f μ.
• Lp.finStronglyMeasurable: 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.][Hytonen_VanNeerven_Veraar_Wies_2016]

theorem MeasureTheory.MemLp.finStronglyMeasurable_of_stronglyMeasurable {α : Type u_1} {G : Type u_2} {p : ENNReal} {m0 : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup G] {f : α → G} (hf : MemLp f p μ) (hf_meas : StronglyMeasurable f) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) : FinStronglyMeasurable f μ

theorem MeasureTheory.MemLp.aefinStronglyMeasurable {α : Type u_1} {G : Type u_2} {p : ENNReal} {m0 : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup G] {f : α → G} (hf : MemLp f p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) : AEFinStronglyMeasurable f μ

theorem MeasureTheory.Integrable.aefinStronglyMeasurable {α : Type u_1} {G : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup G] {f : α → G} (hf : Integrable f μ) : AEFinStronglyMeasurable f μ

theorem MeasureTheory.Lp.finStronglyMeasurable {α : Type u_1} {G : Type u_2} {p : ENNReal} {m0 : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup G] (f : ↥(Lp G p μ)) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) : FinStronglyMeasurable (↑↑f) μ