Finitely strongly measurable functions in Lp #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Functions in Lp for 0 < p < ∞ are finitely strongly measurable.
Main statements #
mem_ℒp.ae_fin_strongly_measurable: ifmem_ℒp f p μwith0 < p < ∞, thenae_fin_strongly_measurable f μ.Lp.fin_strongly_measurable: 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.
theorem
measure_theory.mem_ℒp.fin_strongly_measurable_of_strongly_measurable
{α : Type u_1}
{G : Type u_2}
{p : ennreal}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group G]
{f : α → G}
(hf : measure_theory.mem_ℒp f p μ)
(hf_meas : measure_theory.strongly_measurable f)
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤) :
theorem
measure_theory.mem_ℒp.ae_fin_strongly_measurable
{α : Type u_1}
{G : Type u_2}
{p : ennreal}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group G]
{f : α → G}
(hf : measure_theory.mem_ℒp f p μ)
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤) :
theorem
measure_theory.integrable.ae_fin_strongly_measurable
{α : Type u_1}
{G : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group G]
{f : α → G}
(hf : measure_theory.integrable f μ) :
theorem
measure_theory.Lp.fin_strongly_measurable
{α : Type u_1}
{G : Type u_2}
{p : ennreal}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group G]
(f : ↥(measure_theory.Lp G p μ))
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤) :