Finitely strongly measurable functions in Lp #
Functions in Lp for 0 < p < ∞ are finitely strongly measurable.
Main statements #
MemLp.aefinStronglyMeasurable: ifMemLp f p μwith0 < p < ∞, thenAEFinStronglyMeasurable f μ.Lp.finStronglyMeasurable: for0 < p < ∞,Lpfunctions are finitely strongly measurable.
References #
- [Hytönen, Tuomas, Jan Van Neerven, Mark Veraar, and Lutz Weis. Analysis in Banach spaces. Springer, 2016.][Hytönen_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 ≠ ⊤)
:
@[deprecated MeasureTheory.MemLp.finStronglyMeasurable_of_stronglyMeasurable (since := "2025-02-21")]
theorem
MeasureTheory.Memℒp.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 ≠ ⊤)
:
Alias of MeasureTheory.MemLp.finStronglyMeasurable_of_stronglyMeasurable.
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 ≠ ⊤)
:
@[deprecated MeasureTheory.MemLp.aefinStronglyMeasurable (since := "2025-02-21")]
theorem
MeasureTheory.Memℒp.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 ≠ ⊤)
:
theorem
MeasureTheory.Integrable.aefinStronglyMeasurable
{α : Type u_1}
{G : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup G]
{f : α → G}
(hf : Integrable 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) μ