ae_measurable vs null_measurable

Stream: maths

[Yury G. Kudryashov]

@Sebastien Gouezel, it seems to me that it's easier to work with null measurable functions than with a.e. measurable functions. E.g., you can apply all theorems about measurable functions, and once we rewrite basic facts like measure_union for null measurable sets, we can prove other theorems (e.g., about integrals) for null measurable functions right away instead of the current approach (prove for measurable, use the definition of a.e. measurable).

One difficulty I failed to overcome with a.e. measurable functions (disclaimer: it's 1:35 a.m. here, so possibly in fact it's not a hard issue) is to prove (or disprove) a version of docs#ae_measurable.add_measure for a countable sum of measures. UPD: I can do it but it'll be much uglier than for null_measurable.

AFAIR, the main argument pro a.e. measurable functions (besides the fact that we use them now) is that this way we can easily ensure that the coercion of an ae_eq_fun to a function is measurable. I suggest that we use the following trick: (a) ensure that it is measurable whenever possible (if h : ∃ f (hf : measurable f), mk f hf.null_measurable = g then h.some else ...) then prove measurable_coe whenever we're ready (probably in simple_func_dense). What do you think?

[Yury G. Kudryashov]

Another argument pro null measurable functions: most textbooks about measure theory (at least those I've read) use them (and quite often call them just "measurable").

[Sebastien Gouezel]

The main point, I think, is in view of the upcoming refactor sketched in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/naming.20contest/near/260590829: the right formulation of the most general measurability condition to be able to define an integral is: there exists a function g, almost everywhere equal to f and taking values in a second-countable subspace. This is where we should be heading, and I don't see how this can be expressed through a null_measurable version.

[Sebastien Gouezel]

In fact, it can be expressed through a null_measurable version: it is equivalent to the facts that 1) f is null_measurable 2) there exists a second-countable subspace E such that the preimage of the complement of E has measure zero.

[Sebastien Gouezel]

But still I have the feeling that the theorems will be easier to prove, first for measurable functions taking values in a second-countable subspace, and then for strongly ae measurable functions by taking a representative as in the first step. The issue is that the results will not hold for all measurable functions in any case, so saying that we apply the results for measurable functions to the completed sigma-algebra will not make sense.

[Sebastien Gouezel]

Having said that, I am convinced that the theory can also be built using the null_measurable route using the trick you mention, so if you feel strongly about it you can go ahead! But keep in mind that we will need strongly_measurable(for measurable functions taking values in a second-countable subspace) and strongly_null_measurable (null-measurable function with a second-countable subspace E such that the preimage of the complement of E has measure zero), and that the latter notion is not the former notion for the completed sigma-algebra...

[Yury G. Kudryashov]

Am I right that you can define both as "the limit of a sequence of (null) measurable simple functions"?

[Yury G. Kudryashov]

Anyway, (a) I formalized ae_measurable.sum_measure, so I feel no urge to refactor; (b) rewriting (some of) basic facts in terms of null_measurable_sets wouldn't harm.

[Sebastien Gouezel]

strongly_measurable would be: the everywhere limit of a sequence of measurable simple functions. strongly_null_measurable would be: the almost everywhere limit of a sequence of measurable simple functions. But it would not be: the everywhere limit of a sequence of null-measurable simple functions (as such an everywhere limit takes values in a second-countable subspace).

[Yury G. Kudryashov]

It seems that I'm too sleepy to say something useful. Also it seems that we'll need an ae_measurable-style trick anyway, so there is no need to refactor.

[Floris van Doorn]

One question: when we have strongly_measurable functions (or strongly_null_measurable/strongly_ae_measurable), do we have a need for measurable functions without the strong part?
For second-countable spaces the concepts coincide, and for non-second-countable spaces it seems like the only well-behaved functions are the strongly_measurable ones.

[Yury G. Kudryashov]

We want measurable functions, e.g., for measurable self-maps of a measure space.

[Floris van Doorn]

Ok, fair. But almost everything related to integrals will be formulated in terms of strongly_measurable, right?

[Floris van Doorn]

I just realized that strongly_measurable only makes sense for topological spaces. Then indeed we want measurable for spaces that are not assumed to be a topological space.