Why is the codomain of PMF in mathlib ENNReal and not NNReal

Stream: new members

[Jasper Ganten]

Hi all,

While working with PMF in mathlib, I noticed that the codomain is ENNReal (extended non-negative reals), rather than NNReal or even just the unit interval [0,1]. This makes some calculations more cumbersome, and I was wondering about the motivation for this design choice. Is it mainly for compatibility with measure theory?

Additionally, is there a theorem in mathlib that guarantees that the values of a PMF are always ≤ 1 (i.e., that the codomain is "effectively" bounded because of the sum property)? Or could a PMFin Lean actually take the value ∞ somewhere?

Finally, I am also curious about the reasoning behind the separation between PMFs and distributions in mathlib. To me, the distinction seems a bit arbitrary—could someone explain the motivation or use cases for keeping them separate?

Thanks in advance for any insights!

[Joachim Breitner]

I tried changing PMFs to NNReal a long while ago (https://github.com/leanprover-community/mathlib4/pull/7155), but gave up. It's just super convenient that all infinite sums are Summable

[Aaron Liu]

I have no problems with taking ENNReal codomain, as long as we get more lemmas about how ENNReal.ofNNReal interacts with arithmetic.

[Jasper Ganten]

So effectively working in status quo I always have to try to simplify the equality expression by showing that

• p is real
• using PMF.coe_le_one the expression itsself is bounded

this should yield me an expression in the reals which then can be manipulated easily?
Or is there a more idiomatic procedure?

[Yaël Dillies]

Why is PMF even a thing? To me, it should be a constructor for Measure

[Jasper Ganten]

Yaël Dillies said:

Why is PMF even a thing? To me, it should be a constructor for Measure

to my understanding it's separate because it defines a monad structure (see here) and because not all stochastics is interesting for measure theory.

[Yaël Dillies]

Sorry, I should clarify. To me, PMF currently fills two roles:

• It is a way to build a measure from given weights. This use can be replaced by a constructor for docs#MeasureTheory.Measure
• It is a type representing probability measures over a finite space. This use can be replaced by docs#MeasureTheory.ProbabilityMeasure

[Bolton Bailey]

Pointer to more recent discussion here. #new members > Performing arithmetic with ENNReals @ 💬

It feels like we should at least have a function PMF S -> S -> NNReal.

[Bolton Bailey]

It also feels like it would be more convenient API if functions like docs#PMF.bernoulli did not take ENNReals as arguments, I am having trouble even defining the Bernoulli(1/2) variable.

[Joachim Breitner]

That may be a youth sin of mine…

[Bolton Bailey]

#26596