[Merged by Bors] - feat(measure_theory/strongly_measurable): define strongly measurable functions

[RemyDegenne]

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.

---

[sgouezel]

The notion I had heard of as "strong measurability" is not exactly this one, https://en.wikipedia.org/wiki/Strongly_measurable_function. Instead, it is: "almost everywhere limit of a sequence of simple functions" (without the finite measure support condition). With this definition, it is equivalent to "coincides almost everywhere with a function whose range is second-countable" (this works even when the target space is not second-countable). I had a plan to refactor integration theory in mathlib with this notion, to extend our definition of integral to functions with target space which is not second-countable (this is important to define spectral projections of operators in Banach spaces, as they are defined as contour integrals of operators -- the space of operators is not second-countable, but along a contour integral by compactness everything happens in a second-countable subspace). (But I never found the time to do it yet).

Anyway, this is not to stop you from working with the definition you're using in the PR, it's just that I would like to make sure we have a terminology that does not block this forthcoming refactor.

[RemyDegenne]

Actually I think that even my source for strongly_measurable uses it a bit differently than I do. It defines strongly measurable as limit of simple functions (without the finite measure condition), then defines strongly µ-measurable to mean almost everywhere limit of simple functions with support with finite µ-measure.
What I defined here is the close to the second one, strongly µ-measurable (but not quite the same, since I did not use an almost everywhere limit).

I should change the name. Any suggestion?

[RemyDegenne]

I see four possible related notions for those limits of simple functions, depending on two things:
A: limit 1) everywhere, or 2) almost everywhere
B: simple functions 1) without restriction, or 2) with finite measure support.

The book "analysis in Banach spaces" uses A1B1 (which does not depend on a measure) and A2B2. What I defined is A1B2. What you describe looks like A2B1.

I can add a few definitions to the PR. Which ones do we really want, and how do we name them? I am happy with either A1B2 or A2B2.

[sgouezel]

I'd say that A1B1 is strongly_measurable in the "analysis in Banach sapces" sense and A2B1 is ae_strongly_measurable in the wikipedia sense and A2B2 is ae_strongly_measurable in the "analysis in Banach spaces" sense (where the difference between the two is only relevant when the space is not sigma-finite, so shouldn't be relevant in interesting situations).

Since I'm far from an expert in this business, my best bet would probably be to trust the "analysis in Banach spaces" authors that their notions are the most interesting ones. So, what about using A2B2 under the name ae_strongly_measurable?

[RemyDegenne]

I introduced three of the four possible definitions:

• strongly_measurable for limit of simple functions,
• fin_strongly_measurable, which I call finitely strongly measurable, for limit of simple functions with support with finite measure,
• ae_fin_strongly_measurable, for functions a.e. equal to a fin_strongly_measurable function.

The file imports simple_func_dense: it is placed before the definition of the Bochner integral but not that early either. simple_func_dense is needed to have approx_on, which basically states that measurable functions are strongly measurable in spaces with second countable topology. If you later need the definition of strongly_measurable earlier in the import hierarchy, the file can be split into two at that time.

[sgouezel]

LGTM, thanks!

[sgouezel]

LGTM
bors d+
Thanks!

[sgouezel]

couldn't this even be an instance?

[RemyDegenne]

I made it an instance, but I don't really understand what it brings. Since there is an explicit argument, that instance cannot be found without explicitly calling that lemma? How is it then different from a lemma?

[sgouezel]

The conclusion of the instance is sigma_finite (μ.restrict hf.sigma_finite_set). Since it mentions hf, this means that hf is available when trying to apply the instance, so everything should work fine with this instance.

[bors]

✌️ RemyDegenne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[RemyDegenne]

bors r+

[bors]

This PR was included in a batch that successfully built, but then failed to merge into master (it was a non-fast-forward update). It will be automatically retried.

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests