Finitely strongly measurable functions in Lp

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

Main statements

• Memℒp.aefinStronglyMeasurable: if Memℒp 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.

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

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

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

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