Pmf: ENNReal vs. NNReal

Stream: mathlib4

[Joachim Breitner]

Probability mass functions are currently defined as

A probability mass function, or discrete probability measures is a function α → ℝ≥0∞ such that the values have (infinite) sum 1.

I wonder why ENNReal is used here as the codomain – surely there can never be an ∞ if the norming conditions doesn’t hold?
Might it be nicer to use NNReal there, so that one doesn’t have to worry about ∞ when applying a Pmf or doing proofs about it?

[Jireh Loreaux]

I'm not sure why it's like that, but one guess: measures take values in ENNReal, so for parallelism it's nice. It's also a complete lattice, and that makes various things behave nicer. I'm not sure if any of these are sufficient to justify the design decision though.

[Joachim Breitner]

Yeah, the connection with measures was also my guess. But Pmf.toMeasurecould coerce to ENNReal in the right place… I’ll see if I get to a point where this is actually impeding me. Maybe it’s fine to just use toReal where necessary, although my gut feeling leans towards sticking to NNReal as long as possible.

[Jireh Loreaux]

Yeah, I think the bigger issue may be having the complete lattice handy, but probably this is also only a minor convenience. If you are using docs#ENNReal.toReal a bunch, then my gut feeling is that switching to ℝ≥0 would be preferable (but I have not thought a long time about this, and I'm not familiar with the probability theory part of the library).

[Sebastien Gouezel]

The initial design what using NNReal-valued functions, and we switched to ENNReal-later on for the reasons you're mentioning above -- clearer relationships with measures, and avoiding summability issues.

[Joachim Breitner]

It might be one of those trade offs where the general theory (connection to measurements etc) is easier with one, and concrete applications (calculating specific probabilities and expectations) is easier with the other. I see more of the former in mathlib right now.

[Sebastien Gouezel]

Yes, definitely. For concrete applications, it is likely that we will need more API hiding away the concrete definition -- but such an efficient API can only be constructed while doing the applications, and seeing what would be handy there.

[Kalle Kytölä]

There was some previous discussion around here (not specific to pmfs, but maybe "elementary"/concrete probability more generally). In particular, I think there is a relatively convincing case that for concrete applications much of the API might use Real instead of either NNReal or ENNReal. The tactics (ring, linarith, ...) are much better at handling reals than those other types.

[Kalle Kytölä]

The only "advantage" of NNReal seems to be guaranteed nonnegativity by bundling (which is why I made for example the fun-like coercion from FiniteMeasure and ProbabilityMeasure an NNReal). But I think even this is outweighed by some positivity extensions, and the other advantages of reals are much more substantial. (In particular I plan to revisit the fun-like coe choice for finite measures and probability measures.)

The advantage of ENNReal is of course the direct link to Measures and lintegrals (by contrast integrals are going to have some more tedious aspects anyway, because integrability guarantees are always needed to avoid junk values). But I think the advantages of Reals for many concrete applications still look significant. Of course the only way is to try...

[Kalle Kytölä]

I'm currently (slowly) PRing the remaining parts of the portmanteau theorem (e.g. #6253 and this branch) and will continue with some API of convergence in distribution afterwards, including probably at least some example cases of distributions. Maybe I'll learn something about the concrete applications along the way. :fingers_crossed: I'm of course very interested in hearing about your (and others') experiments in concrete probability!

[Jireh Loreaux]

Kalle, I really doubt that using ℝ is the way to go here. I think the automatic nonnegativity gained by bundling is extremely useful, the positivity tactic (or even gcongr) notwithstanding. Moreover, if one ever wants to apply linarith, all one needs to do is apply Subtype.ext or NNReal.coe_le_coe.

[Kalle Kytölä]

Ok, interesting.

I currently deal with a lot of NNReal and ENNReal-valued things, which are much more tedious to manipulate than I think they should be. I get a feeling that working with reals would make a lot of pain go away. (Incidentally, the direct reason for the generalization #6107 of some limsup/liminf results to conditionally complete linear orders is that I am simplifying the proof of one implication in portmanteau by getting out of ENNReals). The point about linarith is good --- in principle it should be a matter of just invoking one extra coercion step (or in the worst case one per each transitively chained inequality?). But for example just letting ring cancel out things in obvious simplification steps instead of making sure that each and every truncated subtraction satisfies what it needs is a frequent pain that should in my opinion be avoidable.

But I have not really experimented with using Reals in probability yet, so I'm only speculating about the practical difference. I'm obviously happy to stick to what is found out to be the smoothest (or least rough) way.

[Joachim Breitner]

In the concrete case of Pmfs it seems particularly strange to allow infinity, since by definition the function has to be real valued everywhere. Of course one can cast to ENNReal when connecting to measures, but that direction is presumably simpler than dealing with toReal when getting the probability of a certain outcome.

[Jireh Loreaux]

@Kalle Kytölä how often are you dealing with subtraction (because this is a fair point, but perhaps we just need better tactic support for tsub)? Can you point me to some example code?

[Kalle Kytölä]

I think more common than subtraction is simplifications involving cancellations (say wanting to invoke ring).

But sorry, I don't currently remember a very clear case, it is just an overall feeling of where I struggle in Lean vs. math, or maybe as a fairer comparison, in probability Lean vs. e.g. algebra, topology, and analysis Lean (ok, analysis definitely has its own difficulties :sweat_smile:). But almost surely (i.e. with probability 1 : ENNReal :wink:) I'll find some examples again in the near future, and I'll let you know!

It is likely that I'm doing some things suboptimally, and I will be happy to learn better ways to avoid the difficulties. I still believe more experimentation by many people will be valuable. I will at least try to provide concrete examples of where I feel NNReals turn out more difficult than needed and maybe at some later point even test refactoring and seeing if reals are in fact any easier (since this is what I certainly haven't done yet).

[Joachim Breitner]

This is what I am working towards (in https://github.com/leanprover-community/mathlib4/pull/6454):

theorem integral_eq_sum [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (p : Pmf α)
  (f : α → ℝ) : ∫ a, f a ∂(p.toMeasure) = ∑ a, f a * (p a).toReal := by …

theorem bernoulli_expectation {p : ENNReal} (h : p ≤ 1) :
  ∫ b, cond b 1 0 ∂((bernoulli p h).toMeasure) = p.toReal := by simp [integral_eq_sum]

It works, but it seems pretter if the Pmf in p a would return a NNReal to begin with, and if the bernoulli distribution parameter was not allowed to be infinite.

[Peter Pfaffelhuber]

Actually, pmfs were previously defined to have codomain NNReal. See line 13. I don't know why that changed.

[Joachim Breitner]

It was changed in https://github.com/leanprover-community/mathlib/commit/e50b8c261b0a000b806ec0e1356b41945eda61f7. I'll finish what I want to do with the current setting, and afterwards maybe try to go back and compare. (My gut feeling is that the sweet spot is to define the pmf function to have codomain NNReal, but still do all the integreals and measures in ENNReal, to reap the benefits of easy integration.)

[Kalle Kytölä]

Jireh Loreaux said:

Kalle Kytölä how often are you dealing with subtraction (because this is a fair point, but perhaps we just need better tactic support for tsub)? Can you point me to some example code?

What I said in my original response (below) is stupid or at least sloppy:
Kalle Kytölä said:

I think more common than subtraction is simplifications involving cancellations (say wanting to invoke ring).

Of course NNReal allows for cancellations of just additions (but ENNReal doesn't). So as you correctly suggest, in my trouble with NNReal I must be using subtractions somewhere. At least one place where those come from is passing to probabilities of complements: $\mathsf{P}[A^c] = 1 - \mathsf{P}[A]$ (which is something one does in math without noticing: for example to lower bound a probability one typically upper bounds the complementary probability).

One concrete use of complements in the portmanteau theorem is to pass from $\liminf \mu_i[G] \ge \mu[G]$ for open sets $G$ to $\limsup \mu_i[F] \le \mu[F]$ for closed sets $F$ (complements of open sets :wink:) --- and vice versa.

Also for example any inclusion-exclusion formulas involve (something like) complements, and thus subtraction of probabilities.

I recognize these are not yet the concrete difficulties you were asking for --- I will look for examples and return to this. But I think I generally claim that subtractions are not evil in probability (although they may be in measure theory).

[Kalle Kytölä]

Still not a great concrete example of difficulty in probability (because it has to do with an obvious API hole), but in #6455 I suggest to add 8 easy $\liminf$ / $\limsup$ lemmas which don't work quite as symmetrically as one would hope. The 4 which involve addition work in at least ℝ, ℝ≥0, and ℝ≥0∞. The other 4, which involve subtraction, apply currently only to ℝ, although mathematically they should work in ℝ≥0 and ℝ≥0∞ also. (But I hope these 4 can still be temporarily accepted with less than optimal typeclass assumptions, because their applicability in ℝ is a part of how I plan to simplify one of the missing portmanteau implications... by converting manipulations from ℝ≥0∞ to ℝ to avoid trouble.)

[Joachim Breitner]

I spend some time (probably too much) to see what breaks if I change Pmfs to be NNReal-valued. My first attempt to just rewrite stuff turned out to be too tricky, so now in mathlib4#7155 I do something less invasive, but that would only be a first step towards another sweet spot (if there is one). Maybe one can have the definition to be real-valued, but do computations with infinite sums in ℝ≥0∞ (for example by starting the prof with ENNReal.coe_injecive). But I’m not going to push this much further at this point.