Probability Measure Type in Mathlib

Stream: mathlib4

[Fred Rajasekaran]

Currently, probability measures take values in the extended nonnegative reals. This makes manipulating probabilities pretty clunky, as simple tactics like ring do not work and I need to use the ENNReal version. Would it be possible to change probability measures in mathlib so they take values in the non-negative reals (or just reals)?

@Floris van Doorn @Rémy Degenne @Yaël Dillies

[Aaron Liu]

Maybe something with docs#MeasureTheory.FiniteMeasure

[Floris van Doorn]

I spoke with Fred this week, and I think this would be useful to do.
Carleson has the MeasureReal file (coming from PFR) which defines for an arbitrary measure the .real function, which is a real value.
This will give you the right function, and I think it's worth it to duplicate a whole lot of lemmas about measure to also work with this function.

For probability theory, I can imagine that we want the coercion-to-functions of a probability measure (or finite measure) to use this function by default. If we want to do that, I think we have to make FiniteMeasure a separate structure (not a mixin on top of Measure).

I'm curious what the people that actually use probability theory think.

[Floris van Doorn]

(additional ping: @Sébastien Gouëzel)

[Yury G. Kudryashov]

Currently, probability in Mathlib is done with {P : Measure α} [IsProbabilityMeasure P], not {P : ProbabilityMeasure α}. A bundled ProbabilityMeasure type is used as a tool to define/use the topology on the space of finite/probability measures.

[Yury G. Kudryashov]

If we want to change this, then we should figure out how to make definitions like docs#MeasureTheory.ae and docs#MeasureTheory.Measure.AbsolutelyContinuous codomain-polymorphic.

[Floris van Doorn]

Adding a separate FiniteMeasure structure might be a bigger endeavor than I anticipated. It will also affect integrals etc. That might not be worth it.
I didn't know we have docs#MeasureTheory.OuterMeasureClass for Measure.ae.

[Yury G. Kudryashov]

I added it a few months ago, because I wanted to generalize some lemmas so that they work for OuterMeasure and Measure.

[Sébastien Gouëzel]

We already have thought about it, and we definitely want to keep probability measures as genuine measures with a typeclass [IsProbabilityMeasure P], because there is so much API for measures (integrals, almost everywhere behavior, restrictions, and so on). However, it's true that having the real-valued versions has definitely proved useful, both in PFR and in Carleson, which is why we had introduced P.real there. Since this keeps coming back and has already been used in two projects, I think this is ample proof that this is useful, and high time to upstream. I've just opened #23943 for this.

[Yaël Dillies]

Thank you Sébastien! I wasn't feeling very confident upstreaming that myself

[Yury G. Kudryashov]

Does someone plan to replace (μ s).toReal with μ.real s in Mathlib?

[Yury G. Kudryashov]

If not, then I can do it (but I have other plans too).

[Sébastien Gouëzel]

Yury G. Kudryashov said:

Does someone plan to replace (μ s).toReal with μ.real s in Mathlib?

I'm working on it.

[Sébastien Gouëzel]

PR at #24204. long (910/-698), but mostly straighforward and repetitive. Touches 100 files, will rot very quickly.

[Michael Rothgang]

Took a look at the first quarter: I'll need to get off the train soon - but posted where I stopped - so others may continue from there.

[Etienne Marion]

Ah didn't see Michael's message. I went through the whole PR and left a few comments.