mathlib documentation

measure_theory.function.strongly_measurable_lp

Finitely strongly measurable functions in Lp #

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

Main statements #

References #

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_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_group G] {f : α → G} (hf : measure_theory.mem_ℒp f p μ) (hp_ne_zero : p 0) (hp_ne_top : p ) :
theorem measure_theory.Lp.fin_strongly_measurable {α : Type u_1} {G : Type u_2} {p : ennreal} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group G] (f : (measure_theory.Lp G p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) :