Should `PMF` be supported by mathlib?

Stream: mathlib4

[David Ledvinka]

To me this should just be a special case of withDensity or pdf when the reference measure is the counting measure. To support PMF properly we basically have to duplicate every theorem about pdfs and/or with withDensity.

[Jakub Nowak]

One argument about keeping PMF, is that I understand what "a function α → ℝ≥0∞ such that the values have (infinite) sum 1." means, and I have absolutely zero idea what "Radon–Nikodym derivative of the push-forward measure of ℙ along X with respect to μ." means. :sweat_smile:
But I'm not against defining docs#PMF in terms of docs#MeasureTheory.pdf.

[Jakub Nowak]

That's a half joke though, I know what a pdf is. If you want to remove docs#PMF what API would you propose instead? I've been using it for finite sets and often it doesn't require going into measure theory at all.

[David Ledvinka]

Technically docs#PMF does not correspond to docs#MeasureTheory.pdf directly, since PMF as defined is more like a "pre density" (for either a measure or a random variable) but I assume most theorems about PMFs generalize to functions that integrate to one with respect to a reference measure (unclear if a definition for this like probabilityDensity is needed, or the theorems that are actually desired can be restated with withDensity and/or pdf)

[David Ledvinka]

Personally I don't think not requiring measure theory is a good reason to support it in mathlib similar to how there is not an API in mathlib to do limits without filters, especially for contributions in mathlib that would also work in more general cases. I do think it could be good to have a top level API (whether its hosted in mathlib or not) for doing elementary probability which specializes the measure theoretic approach so that people can play around with it, but I don't think it should be used to prove stuff in mathlib.

[David Ledvinka]

The thing about filters though, is that once you understand them it doesn't "get in your way" (and can often help). If it were the case that even for someone who understands the theory it is still much easier to use PMFs to prove things then pdfs/densities then I think there is an argument to keep it. But I think that is unlikely to be the case once the API for pdfs is good enough (although right now I think pdf and PMF are still missing a lot).

[David Ledvinka]

FWIW I think if the API is good enough you shouldn't have to actually understand the theory of Radon-Nikodym derivative is to use it (similar to how Measure is defined in terms of Outer measure but with the great Measure API this is almost never relevant). However I think understanding some measure theory (even if its just enough to figure out how to reduce to the special case) is a reasonable expectation for mathlib.

[Alex Meiburg]

In one of my larger projects I don't use PMF, specifically because it has the somewhat annoying (to me) aspect that it uses ENNReal. The numbers must, of course, all be between 0 and 1, so they could at least be NNReal, but really I think that a "probability" is its own first-class type (identified with Set.Icc 0 1) and that's what it uses.

(I could see myself, later, changing it to use HasSum 1 instead of Fintype.sum.)

[Jakub Nowak]

David Ledvinka said:

Technically docs#PMF does not correspond to docs#MeasureTheory.pdf directly, since PMF as defined is more like a "pre density" (for either a measure or a random variable) but I assume most theorems about PMFs generalize to functions that integrate to one with respect to a reference measure (unclear if a definition for this like probabilityDensity is needed, or the theorems that are actually desired can be restated with withDensity and/or pdf)

I agree with you. I think it's probably better to replace PMF with pdf/wthDensity and would welcome such an API.