mathlibdocumentation

measure_theory.function.strongly_measurable

Strongly measurable and finitely strongly measurable functions #

A function f is said to be strongly measurable if f is the sequential limit of simple functions. It is said to be finitely strongly measurable with respect to a measure μ if the supports of those simple functions have finite measure.

If the target space has a second countable topology, strongly measurable and measurable are equivalent.

Functions in Lp for 0 < p < ∞ are finitely strongly measurable. If the measure is sigma-finite, strongly measurable and finitely strongly measurable are equivalent.

The main property of finitely strongly measurable functions is fin_strongly_measurable.exists_set_sigma_finite: there exists a measurable set t such that the function is supported on t and μ.restrict t is sigma-finite. As a consequence, we can prove some results for those functions as if the measure was sigma-finite.

Main definitions #

• strongly_measurable f: f : α → β is the limit of a sequence fs : ℕ → simple_func α β.

• fin_strongly_measurable f μ: f : α → β is the limit of a sequence fs : ℕ → simple_func α β such that for all n ∈ ℕ, the measure of the support of fs n is finite.

• ae_fin_strongly_measurable f μ: f is almost everywhere equal to a fin_strongly_measurable function.

• ae_fin_strongly_measurable.sigma_finite_set: a measurable set t such that f =ᵐ[μ.restrict tᶜ] 0 and μ.restrict t is sigma-finite.

Main statements #

• ae_fin_strongly_measurable.exists_set_sigma_finite: there exists a measurable set t such that f =ᵐ[μ.restrict tᶜ] 0 and μ.restrict t is sigma-finite.
• mem_ℒp.ae_fin_strongly_measurable: if mem_ℒp f p μ with 0 < p < ∞, then ae_fin_strongly_measurable f μ.
• Lp.fin_strongly_measurable: for 0 < p < ∞, Lp functions are finitely strongly measurable.
• Hytönen, Tuomas, Jan Van Neerven, Mark Veraar, and Lutz Weis. Analysis in Banach spaces. Springer, 2016.