Refactoring measure.map

Stream: maths

[Sebastien Gouezel]

Currently, measure.map f μ is defined to be 0 if f is not measurable (in docs#measure_theory.measure.map). This global measurability assumption is nice as it ensures that this operation is linear on measures, from which a bunch of nice properties follow automatically. However, it is creating difficulties to me in a probability theory context: if I have two integrable random variables X and Y and I want to say that they have the same distribution, the natural formulation would be to require that measure.map X ℙ = measure.map Y ℙ, however this fails if X or Y is not measurable (note that they are ae measurable by the integrability assumption). So I am considering refactoring measure.map to allow ae measurable functions, but I'd like to check here for thoughts before -- it's probably gonna be a bit of work, so if it doesn't look like a good idea I'd rather not start on it. Thoughts, anyone?

[Jason KY.]

I thought we had decided to only care about measurable functions in probability theory. Is this not the case anymore?

[Vincent Beffara]

So you want measure.map f μ to be well-defined (and not 0) if f is μ-ae-measurable? That sound like a natural thing to do.

[Vincent Beffara]

But indeed losing linearity means that you would have to rewrite many things ... would it make sense to have two versions?

def measure.map' f μ (h : ae_measurable f μ) := measure.map (h.mk f) μ

[Sebastien Gouezel]

Jason KY. said:

I thought we had decided to only care about measurable functions in probability theory. Is this not the case anymore?

Yes, in most situations. But if a theorem is true assuming only integrable X, it would be a shame to prove it assuming measurable X and integrable X.

[Sebastien Gouezel]

Vincent Beffara said:

But indeed losing linearity means that you would have to rewrite many things.

I am not sure it will be that painful. But I won't know before I try!

[Vincent Beffara]

Losing linearity should not be a big issue for probability as long as you still preserve convex combinations?

[Vincent Beffara]

Ah but you wouldn't either ...

[Sebastien Gouezel]

Whenever the function is measurable this would coincide with the previous definition, so you would keep all the nice properties.

[Jason KY.]

I think as long as we have the same APIs for measurable functions it will work fine so I'm in favour of the refactor

[Sebastien Gouezel]

That's now #13241