mathlib3

86fccaab - feat(measure_theory/strongly_measurable): define strongly measurable functions (#8623)

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. Co-authored-by: RemyDegenne <remydegenne@gmail.com>