Commit 2021-08-19 14:31 86fccaab

feat(measure_theory/strongly_measurable): define strongly measurable functions (#8623) A function f is said to be strongly measurable with respect to a measure μ if f is the sequential limit of simple functions whose support has finite measure. Functions in Lp for 0 < p < ∞ are strongly measurable. If the measure is sigma-finite, measurable and strongly measurable are equivalent. The main property of strongly measurable functions is strongly_measurable.exists_set_sigma_finite: there exists a measurable set t such that f 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. I will use this to prove properties of the form f =ᵐ[μ] g for Lp functions.