PMF Refactor: FunLike vs Definition Change

Stream: mathlib4

[Peter Hansen]

Following the discussion on the awkwardness of ENNReal arithmetic in PMF (and @Bolton Bailey's recent WIP PR #33689), I'd like to revisit the design choice for Probability Mass Functions.

Currently, we have:

def PMF (α : Type u) : Type u := { f : α → ℝ≥0∞ // HasSum f 1 }

As noted in the chat, this causes friction when trying perform standard arithmetic, even though we know the values are always finite.

There seem to be three paths forward:

1. Status Quo (ENNReal)

• Pros: Sums always exist.
• Cons: Arithmetic is painful.

2. Change the FunLike instance (Bolton's PR #33689)
Keep the internal definition as ENNReal, but change the FunLike instance to return NNReal.

• Pros: Improves the user experience for evaluation (p x returns a nice NNReal) without changing the underlying storage.
• Cons: It creates a disconnect between the internal representation (ENNReal) and the interface (NNReal)..

3. Change the definition to NNReal
Refactor the type entirely:

def PMF (α : Type u) : Type u := { f : α → ℝ≥0 // HasSum f 1 }

• Pros: The type accurately reflects that probabilities are finite. NNReal makes doing standard arithmetic nicer.
• Cons: We lose the "sums always exist" convenience.

Question for the community:
Is the convenience of ENNReal summation worth the friction in arithmetic? It seems the summability burden is largely an internal implementation detail (e.g., inside bind), whereas the arithmetic friction is a recurring tax on every user. It feels better to pay the cost of convergence proofs once in the library structure than to force every user to deal with ENNReal casting.

I am leaning towards Option 3, as it aligns better with the mathematical definition of a discrete probability distribution, but I would appreciate insights on whether this is the way to do it. To test things out, I rewrote ProbabilityMassFunction.Basic with PMF defined as NNReal valued, and it ended up taking slightly fewer lines of code than the original version. The ProbabilityMassFunction.Monad might be a bit trickier though.

[Bolton Bailey]

I might actually suggest/change my PR to a fourth option, to use a more specialized type like docs#unitInterval. It seems like if we are going to change the return type to a subtype of the reals, it ought to be the subtype which consists of exactly those values it is possible for it to return. Perhaps this would make it more convenient to deal with inequalities, but I don't know how much harder it would make the algebra.

[Sébastien Gouëzel]

The initial definition was in terms of NNReal functions, and it's after a lot of gained experience in this context that we decided to switch to ENNReal (see https://github.com/leanprover-community/mathlib3/pull/17032). Since it was a deliberate and thought-through move, I'm not sure it's a good idea to undo it.

[Sébastien Gouëzel]

Discussion at #maths > `nnreal` vs. `ennreal` in `pmf` @ 💬

[Kevin Buzzard]

I think that I would like to see more evidence of "arithmetic is painful". I'd like to check that this doesn't actually mean "arithmetic is painful if you don't know the tricks" or "arithmetic is painful because there is a specific tactic which would solve everything and which we don't have" (so another potential path forward might be a concrete specification of a tactic, followed by an implementation of that tactic). Can we see some concrete examples of this pain? My understanding of tactic-writing to alleviate pain is that a good way to start is to have 5 or more self-contained examples of goals which are currently painful and should ideally be one- or two-liners if the appropriate tactic existed.

[Peter Hansen]

@Sébastien Gouëzel Thanks for the context. I am curious to dig a bit deeper into the "why" of the original switch.

Is the "summability burden" of NNReal primarily an issue when constructing the library (e.g., proving bind and map are well-defined), or does it leak out to the end-user frequently?

My current intuition is that it feels better to be diligent with summability proofs once (at the implementation level) if it guarantees the user a clean NNReal interface forever after. But perhaps I am missing cases where summability becomes a constant headache for the user as well?

[Peter Hansen]

@Kevin Buzzard I admit I don't have 5 concrete snippets ready to go—my motivation is more that to me, a PMF taking values in ENNReal just feels like it is lacking in moral fibre. Not the best justification, I suppose...

Regarding the tactic argument, I wonder if we could flip it? If the downside is proving summability, couldn't we just have a summability tactic? It seems cleaner to fix the definitions (NNReal) and automate the convergence proofs, rather than keep a "loose" definition (ENNReal) and try to build tactics to retrofit standard arithmetic onto a type designed to handle infinity.

[Sébastien Gouëzel]

I have never used PMFs myself, so I can't really comment on the original motivation. But as far as I understand concrete manipulations of PMFs need summability checks all the time, not just the API construction, if I read the original thread correctly.

[Peter Hansen]

That is a fair concern. Though, I suspect most of those summability checks arise from jumping from HasSum to tsum too quickly. If one stayed in HasSum during concrete manipulations of PMF, I would expect many of those summability issues could be avoided.

[Kevin Buzzard]

The other thread mentioned this tactic: https://github.com/wvhulle/ennreal-arith (see "Usage" in the README). If this looks like it solves some problems then perhaps this could be upstreamed somehow. It looks to me like it might be a solution to "arithmetic is painful" (the only listed disadvantage to the status quo) but without an explicit list of examples of how it's painful, it's difficult to check whether this tactic is a solution.

[Bhavik Mehta]

Kevin Buzzard said:

I'd like to check that this doesn't actually mean "arithmetic is painful if you don't know the tricks" or "arithmetic is painful because there is a specific tactic which would solve everything and which we don't have" (so another potential path forward might be a concrete specification of a tactic, followed by an implementation of that tactic).

I'd argue the latter; things like ring and field work nicely for the reals but not for ENNReal, because they're not a ring, and so for "obvious" algebraic manipulations it sometimes feels like we're in a pre-ring world again. (I don't have concrete examples to hand, but I expect they'll be easy to list for anyone who works with ENNReal regularly)

[David Ledvinka]

I have expressed this in other threads but I think PMF itself is somewhat outdated. It encourages developing API which will hold in greater generality and then need to duplication. For example your PR #33668 would hold equally well for the (nonexistent) MF. This is relevant even to discrete probability because you may encounter things like flat priors or sub probability measures in certain arguments (just to name some examples). Like how we don't develop a seperate API for Probability measures we instead use the class IsProbabilityMeasure I think it probably makes more sense to refactor to MF and have a sum to 1 hypothesis or possibly even better [IsProbabilityMeasure p.toMeasure] (with appropriate API) when you actually need it.

[David Ledvinka]

As for ENNReal vs NNReal I think it may make sense to switch to the approach that the continuous distributions take with PDFReal and PDF. You first define PDFReal with real weights and then define PDF on ENNReal by composing with ENNReal. You could do the same with PMFReal and PMF. But regardless I think that the automation for ENNReal computations should (and eventually will) be improved. The reason this works nicely is that for lintegrals you use the PMF/MF but for (bochner) integrals the toENNReal "peels off".

[Bolton Bailey]

If people wanted to see the pain point that motivated me to start working on this again, it's here.

I think that regardless of which return type is better for the funlike instance, there are probably proofs where one version would be more convenient and other proofs where another version would be more convenient. So I would like to see some kind of PMF α → α → ℕ≥0 function and ext-like API around it.

[David Ledvinka]

Fwiw I think it makes more sense to define the (TV) metric space more generally on FiniteMeasure and ProbabilityMeasure and then have a lemma that states this reduces to a sum in the discrete case.

[Bolton Bailey]

We actually have MeasureTheory.FiniteMeasure.mass and MeasureTheory.ProbabilityMeasure.instFunLike that return NNReals, so perhaps there is another argument for making a change somewhere for the sake of consistency.

[Bolton Bailey]

The idea of defining TV through measure theory was discussed here. @Yannick Seurin might have been interested in doing work along these lines.

[Bolton Bailey]

David Ledvinka said:

the (nonexistent) MF

Perhaps you can explain this more? Is this just the type of countably supported functions to ENNReal?

[Bolton Bailey]

My reluctance to personally implement measure-theory related solutions to PMF probably has to do with my unfamiliarity with the measure theory part of the library. Is there some kind of map that can take any type and give us a discrete measure space on that type, so that PMF a is really just the type of probability measures over this space? If so, could we just redefine all of PMF in terms of that, and inherit all the measure API directly?

[Bolton Bailey]

@loogle ?a -> MeasurableSpace ?a

[loogle]

:shrug: nothing found

[Bolton Bailey]

Ok I have found instDiscreteMeasurableSpace, I guess this is effectively the function I was searching for. And I guess another way we could write this is just as the top element of the type of measure spaces.

So I guess my next question is, is PMF α just equivalent to @MeasureTheory.ProbabilityMeasure α ⊤?

[David Ledvinka]

I had in mind MF : α → ℝ≥0∞ and you include additional hypothesis when you need them. Its not clear that we even need this to be a "named" type (similar to how the use of PDFReal and PDF is not). It may or may not help with API.

A stronger philosophical point here (which may be proven wrong) is that I believe that this kind of API or "templating" is necessary to work with certain concrete distributions that naturally come from PMFs/MFs but it is not a good idea to design a discrete probability API around PMF/MFs as if all your discrete distributions will come from PMF/MFs.

There are lots of obvious reasons for this that come from the fact that you will likely prove facts that should be special cases of more general measure theory and also will likely cause trouble when you try to mix these together (for example a setting where you are considering discrete random variables and continuous random variables on the same probability space).

However I think even in the case where you only care about discrete probability it will often not be natural to think of the distributions as coming from PMFs. In many cases, for example when you construct a random graph from some procedure it often is not natural to view it first and foremost as coming from a PMF, for example here. In the setting of random graphs (or other things like this) the measure theoretic definition of TV is actually still more natural and you may use it to bound TV between distributions by exhibiting some event where you show two measures on the graph differ in probability by some amount (of course you could translate this to PMFs but I claim it is actually much more awkward in this case despite being discrete).

But I do agree with you that in the case that we have measures on a discrete measure space, it should be easy to reduce to discrete objects like sums etc when desired without having to understand the measure theory library (and measure theory) well enough to unravel it. As an example, one should be able to prove that the sum of Bernoulli random variables is Binomial while understanding little to no measure theory (especially since in a case like this there is no risk that the statement is not general enough). I have work on this a little bit but just haven't found a complete solution I was happy to PR yet. I think if the (p-medium) issue solved from this thread was completed then you could get simp to do most of these reductions .

[David Ledvinka]

Bolton Bailey said:

So I guess my next question is, is PMF α just equivalent to @MeasureTheory.ProbabilityMeasure α ⊤?

Essentially yes. Though as I mentioned above we only use ProbabilityMeasure when one cares about some structure on the space as a whole (so a metric space structure would be an example)

[Bhavik Mehta]

it is not a good idea to design a discrete probability API around PMF/MFs as if all your discrete distributions will come from PMF/MFs.

Just to add that as someone who mostly only needs probability in the discrete finite case, I completely agree with this point. We should make it easy to specialise the general case to the discrete finite situation, but the theory should be developed in the general case without PMF.

[Bolton Bailey]

Thanks for the explanation!

[Rémy Degenne]

@Peter Pfaffelhuber the discussion above is related to what you want to do.

Peter told me he wanted to define a DiscreteMeasure type, which sounds very similar to what David Ledvinka calls MF in the messages above. Peter wants it to be a type, because then it's a monad and you can use do notation, for example to define a Binomial by describing the sampling of several Bernoulli and recording the successes.

[Peter Pfaffelhuber]

Personally, the point of the 2022 NNReal to ENNReal change convincing, since in particular, Measure maps Set α → ENNReal and I think there should be a coercion from PMFtp Measure (which does not exist yet). Thanks @Kevin Buzzard for the pointer to ennreal-arith, which I will check.

I am also in favour of having something like MF (as a type). My imagination is that they are e.g. used as the state of a point process.

[Kevin Buzzard]

Note that I'm not vouching for the tactic, it was just something that came up in one of the other threads discussing this. I don't know anything about the tactic or its spec.

[Peter Pfaffelhuber]

David Ledvinka schrieb:

I have expressed this in other threads but I think PMF itself is somewhat outdated. It encourages developing API which will hold in greater generality and then need no duplication. This is relevant even to discrete probability because you may encounter things like flat priors or sub probability measures in certain arguments (just to name some examples). Like how we don't develop a seperate API for Probability measures we instead use the class IsProbabilityMeasure I think it probably makes more sense to refactor to MF and have a sum to 1 hypothesis or possibly even better [IsProbabilityMeasure p.toMeasure] (with appropriate API) when you actually need it.

I would vote for this approach. @Rémy Degenne's impression was that several people started to develop something similar as MF (e.g. in the SampCert-differential-privacy-project), so this is useful anyway. Using the class IsProbabilityMeasurewould also be inline with other parts of the probability theory part of the library as far as I can see.

[Yuval Filmus]

Kevin Buzzard said:

The other thread mentioned this tactic: https://github.com/wvhulle/ennreal-arith (see "Usage" in the README). If this looks like it solves some problems then perhaps this could be upstreamed somehow. It looks to me like it might be a solution to "arithmetic is painful" (the only listed disadvantage to the status quo) but without an explicit list of examples of how it's painful, it's difficult to check whether this tactic is a solution.

Is ENNReal arithmetic even a little bit more difficult than real (not NNReal!) arithmetic?
If so, it's a deal breaker.

The discussion here might reflect two very different styles of doing mathematics: highly abstract ones, where explicit computations are shunned (cf. the discussion on matrices), compared to discrete mathematics (most of combinatorics, parts of probability theory, etc.), where computations are the norm, and we are more interested in dealing with concrete objects rather than working in the greatest possible generality.

It's nice that Mathlib is very general, but if that makes it impossible to work concretely , then you're essentially kicking out anybody working in discrete mathematics, which would be a shame.

Can you prove that a sum of independent Bernoullis has a binomial distribution? Can you prove that if you toss a coin infinitely many times, then the distribution of the first time you get heads is geometric? Can you determine the threshold for the appearance of triangles in G(n,p) random graphs? Can you construct a coupling between G(n,p) and G(n,q) and use it to show that the probably of monotone properties is increasing in p?
If these are impossibly difficult (for anybody other than Yaël and Bhavik), then we have a problem.

[Johan Commelin]

I don't think Mathlib is trying to be very general because it wants to kick out discrete maths.
I think it's trying to be very general because in the past we've seen many times that it pays off.
We want to answer concrete questions, prove lemmas about concrete objects. But we don't know in advance which ones, and how many. So we try be general and abstract, in the hope that this can be applied in many cases.

If it turns out that the abstractions don't apply in the concrete cases, then that is a problem.

But the solution is not to have 370 proofs and computations that are all very similar.
Because we don't have a tactic "apply the same proof strategy as in lemma X, but tweak it where necessary".

[Sébastien Gouëzel]

In the PMF case, it's really the opposite: it's when people started to use it (to prove things about sums of binomials and so on) that they realized that the initial NNReal-valued definition was clumsy to work with, and that things were better with ENNReal. And that's why we switched. It wasn't an ideological decision based on a priori ideas, it was just a pragmatic move based on experimentation. And I'd argue it's the way it should be: often we have a priori ideas on good designs, and when we realize they don't work out as well as we thought, then we change.

[Peter Pfaffelhuber]

Yuval Filmus schrieb:

Can you prove that a sum of independent Bernoullis has a binomial distribution? Can you prove that if you toss a coin infinitely many times, then the distribution of the first time you get heads is geometric? Can you determine the threshold for the appearance of triangles in G(n,p) random graphs? Can you construct a coupling between G(n,p) and G(n,q) and use it to show that the probably of monotone properties is increasing in p?

The first task is around here (in a slightly different setting, not PRed to Mathlib yet, but still using ENNReal rather than NNReal or Real). The second task is more difficult and will need the MeasureTheory library, since you need a probability space with a (countably) infinite number of Bernoullis. (I would be interested to try to prove this.) The other questions really deal with couplings, so they need a way to properly extend a given probability space, show that some random variables on that space have certain distributions etc. Nothing like this is in Mathlib as far as I know, but I cannot see a way around defining the probability space and using monotonicity of the underlying measure in order to prove e.g. the mentioned triangle property.

In addition to what Johan and Sebastian wrote, for me the Natural Number Game is a very good example of having something very concrete, but still fun to get started with formalizing mathematics.

[Peter Pfaffelhuber]

What might be different in probability theory: Often, abstraction makes things easier (i.e. easier to prove, e.g. using filters rather than other tools), whereas in discrete probability theory, in the less abstract setting, computations and proofs should be easier since there are no measurability issues.

[Michael Rothgang]

Let me comment on the "working with ENNReal" aspect, grounded from experience in the Carleson project. (That's a project in harmonic analysis; it involves lots of manipulations of explicit integrals --- i.e., involving analysis and measure theory, but not related to probability measures or PMFs.)

Initially, we tried to make all definitions take real values; this failed badly.

• many suprema involved take potentially infinite values (and even if they are finite, proving this all the time is cumbersome),
• mathlib has much more API for infinite suprema here,
• converting back and forth between Real, NNReal and ENNReal is painful. We have some tools for this, but by far the best way to deal with this is to avoid the conversion in the first place.

Another story involves switching from real-values norms norm to extended norms enorm. Our initial motivation was mathematical (avoid code duplication and a tedious limiting argument), but it turns out to be useful for formalisation: many statements in mathlib actually become clearer by using enorm instead of norm or nnnorm (a norm, but returning non-negative real numbers). This deviates slightly from the mathematical literature, but I consider this to be a good decision all around.

It did imply, however, changing some proofs from Real to ENNReal. Indeed, this is more painful than it should be. There's no ring or field_simp support, so you're back to long rw chains. finiteness can help a bit, by discharging finiteness conditions; overall, the experience is too cumbersome. To me, however, the right fix is to create better tactics, not to avoid ENNReal.

[Yuval Filmus]

A similar issue arises with polynomial degree, which is defined using WithBot, making working with it extremely awkward.
I agree that the best solution is better tactics.
The tactic should enable doing real arithmetic whenever all the quantities involved are finite.
Similarly, there should be a tactic that reduces WithBot arithmetic to natural arithmetic.
In both cases, lift only goes part of the way, and the issue even stumps grind.
For an example with WithBot, you can take a look at #33194.

[Kevin Buzzard]

We have docs#Polynomial.natDegree if using degree is awkward. Mathematically degree is "more correct" but natDegree is often more convenient.

[Peter Pfaffelhuber]

Here is what I would like to do related to PMFs:

• Introduce a type MF := α → ℝ≥0∞ (MF for mass function), which is like PMF but no HasSum 1 property.
• Change the definition of toMeasure from PMF to MF.toMeasure (w : MF α) : @Measure α ⊤ := Measure.sum (fun a ↦ (w a) • @Measure.dirac α ⊤ a). The resulting measure is defined on the power set, so does not require MearurableSpace α.
• Probably, do not define toOuterMeasure as in PMF, since the outer measure defined by a (P)MF and the measure agree anyway. In addition, I know no calculations based on outerMeasures. Otherwise, all results for PMF (if they do not require HasSum 1) should as well be available to MF.
• Give an instance LawfulMonad MF, unlocking do-notation. For map, pure, bind, show that they mean the same as for MF.toMeasure.
• If IsProbabilityMease μ.toMeasure, show that IsProbabilityMeasure is valid after applying map, pure, bind from the monad as well.
• Show that MF α plus IsProbabilityMease μ.toMeasure is the same as a PMF.

Would that be a good way to proceed?

[Artie Khovanov]

Kevin Buzzard said:

We have docs#Polynomial.natDegree if using degree is awkward. Mathematically degree is "more correct" but natDegree is often more convenient.

Yeah I never know which one to use. In practice natDegree is always easier but a lot of stuff is stated with degree. Some sort of lia extension would be very useful here.

[Bolton Bailey]

Peter Pfaffelhuber said:

Here is what I would like to do related to PMFs:

This seems like a good suggestion, but I am still wondering if there is an even better way that does not use ⊤ and instead uses the countable-cocountable measure. I still don't feel like I understand this subject well, but I got the sense from (this thread #maths > Are discrete measures determined by their points? ) that this measure is perhaps easier to prove things about, while being closer to the space of things currently allowed by the PMF definition.

[Bolton Bailey]

I guess it's unfortunate that this particular measure isn't defined directly as an object in mathlib yet #Is there code for X? > The sigma algebra of countable and cocountable Sets

[Bolton Bailey]

So to try to put this proposal in Peter Pfaffelhuber 's terms

• Introduce a type MF := @Measure α (countableCocountable α)
• Redefine PMF (α) as a subtype of MF with docs#IsProbabilityMeasure
• The definition of toMeasure is just the value itself
• (if we want a measure for a different measurableSpace structure on α, as in the current definition, we MeasureTheory.Measure.map over the identity)
• define toOuterMeasure Using docs#MeasureTheory.Measure.toOuterMeasure
• Give the monads
• Again, MF α plus IsProbabilityMeasure μ.toMeasure is the same as a PMF by definition.

[Peter Pfaffelhuber]

In order to define map in the sense of a LawfulMonad, every function needs to be measurable. I can only see this working if I take @Measure α ⊤. In your suggestion, I did not see how this would improve computing things with MFs.

[Etienne Marion]

The sigma algebra of countable and cocountable sets is rather poor (ie very few sets), while in general you prefer to have more measurable sets. For instance the Dirac mass is often defined over the power set, I don’t understand why you would like to restrict measurable sets.

[Sébastien Gouëzel]

Just for the record, as the lack of automation in ENNReal has been mentioned in this thread:

import Mathlib
lemma foo : (16 : ENNReal)⁻¹ * 2 = 8⁻¹ := sorry

doesn't seem to be covered by our standard automation as far as I can tell.

[Bolton Bailey]

Etienne Marion said:

I don’t understand why you would like to restrict measurable sets.

I guess I had assumed that if a PMF is a summable function, which therefore has countable support, it would make more sense for MF to also be only functions of countable support, and that might let us avoid the things mentioned in this thread (#maths > Are discrete measures determined by their points? ) where I am told that determining if two @Measure α ⊤ are equal on the basis of the measures of their points being equal depends on the existence of some cardinal that can't be proved in ZFC.

Perhaps the issue is just that my intuitions about what a "mass function" means are wrong.

[Violeta Hernández]

Artie Khovanov said:

Kevin Buzzard said:

We have docs#Polynomial.natDegree if using degree is awkward. Mathematically degree is "more correct" but natDegree is often more convenient.

Yeah I never know which one to use. In practice natDegree is always easier but a lot of stuff is stated with degree. Some sort of lia extension would be very useful here.

degree carries more information. If p.degree = 0 then p must be constant and non-zero, but it p.natDegree = 0 then all you know is p is constant. So I stick to degree, unless I do need a natural number (to pass it into a function, for instance).

[Artie Khovanov]

Yeah but then I can't use lia :sob:

[Etienne Marion]

Bolton Bailey said:

Etienne Marion said:

I don’t understand why you would like to restrict measurable sets.

I guess I had assumed that if a PMF is a summable function, which therefore has countable support, it would make more sense for MF to also be only functions of countable support, and that might let us avoid the things mentioned in this thread (#maths > Are discrete measures determined by their points? ) where I am told that determining if two @Measure α ⊤ are equal on the basis of the measures of their points being equal depends on the existence of some cardinal that can't be proved in ZFC.

Perhaps the issue is just that my intuitions about what a "mass function" means are wrong.

But if you cannot distinguish measures by just looking at singletons restricting the measurable sets won't solve the problem. A mass function is a way to represent a measure which is only composed of atoms, i.e. it is a sum of Dirac masses (each mass being multiplied by a coefficient).

[David Ledvinka]

Yuval Filmus said:

Can you construct a coupling between G(n,p) and G(n,q) and use it to show that the probably of monotone properties is increasing in p?

G(n,p) and G(n,q) are not in mathlib yet, currently in a PR by @Yaël Dillies #31364. However @Bhavik Mehta had already done this argument in Lean 3 and I spoke with him on how to update the argument to our current state of probability in Mathlib. We demonstrate here the use of this coupling argument to prove a lemma which can be used to deduce the fact you mention above (without an additional coupling argument). Our proof is not optimized (could be both golfed and API added to mathlib) but I think it actually demonstrates why it is important for Probability Theory to have a cohesive API.

import Mathlib

open MeasureTheory Measure ProbabilityTheory unitInterval

open scoped ENNReal Finset Set

namespace ProbabilityTheory
variable {ι Ω : Type*} {m : MeasurableSpace Ω} {P : Measure Ω}

noncomputable def bernoulli_prop_measure (p : I) : Measure Prop := ENNReal.ofReal p • dirac (True) + ENNReal.ofReal (σ p) • dirac (False)

/- I don't use `setBer` and abuse the Set/Prop defeq throughout the file just to make things a bit easier for the demonstration. -/
noncomputable def bernoulli_prop_iid_measure (ι : Type*) (p : I) : Measure (ι → Prop) := infinitePi (fun _ : ι ↦ bernoulli_prop_measure p)

lemma uniform_indicator_hasLaw (p : I) {U : Ω → I} (hU : HasLaw U ℙ P) :
    HasLaw (U · ≤ p) (bernoulli_prop_measure p) P where
  map_eq := by
    apply ext_of_singleton
    intro prop
    conv => enter [1, 1, 1, x]; change ((· ≤ p) ∘ U) x
    rw [← AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop) ,
      map_apply_of_aemeasurable (by fun_prop) (by measurability), hU.map_eq]
    by_cases h : prop = True
    · have : {x : I | x ≤ p} = Set.Icc 0 p := by
        ext x
        exact ⟨fun hx ↦ by simpa using hx, by grind⟩
      simp [h, bernoulli_prop_measure, this]
    · simp only [eq_iff_iff, iff_true] at h;
      have : {x : I | p < x} = Set.Ioc p 1 := by
        ext x
        exact ⟨fun hx ↦ ⟨hx, le_one'⟩, by grind⟩
      simp [h, bernoulli_prop_measure, this]

variable [Countable ι] [IsProbabilityMeasure P]

def hasLaw_bernoulli_iid_of_uniform_iid (p : I) (U : ι → Ω → I) (hU : ∀ i, HasLaw (U i) volume P) (hU' : iIndepFun U P) :
    HasLaw (fun i ↦ U i · ≤ p) (bernoulli_prop_iid_measure ι p) P where
  map_eq := by
    unfold bernoulli_prop_iid_measure
    rw [(iIndepFun_iff_map_fun_eq_infinitePi_map₀ (X := fun i ω ↦ U i ω ≤ p) (by fun_prop)).mp]
    conv => enter [1, 1, i]; rw [(uniform_indicator_hasLaw p (hU i)).map_eq]
    change iIndepFun (fun i ↦ (· ≤ p) ∘ (U i)) P
    apply hU'.comp
    fun_prop

/- Proof that the bernoulli_prop_iid_measure is monotonic in `p` on any `UpperSet` using a coupling argument. -/
example {𝓕 : Set (Set ι)} (h𝓕_meas : MeasurableSet 𝓕) (h𝓕 : IsUpperSet 𝓕) : Monotone (fun p ↦ bernoulli_prop_iid_measure ι p 𝓕) := by
  intro p q hpq
  obtain ⟨Ω, hΩ, P, U, _, hU_law, hU_indep, _⟩ := exists_iid ι (ℙ : Measure I) -- Sample i.i.d Uniform RVs `U i` for each `i : ι`
  /- Couple `bernoulli_prop_iid_measure ι p` and `bernoulli_prop_iid_measure ι q` by "generating" both with `U`. -/
  simp only [← (hasLaw_bernoulli_iid_of_uniform_iid p U hU_law hU_indep).map_eq,
    ← (hasLaw_bernoulli_iid_of_uniform_iid q U hU_law hU_indep).map_eq]
  rw [map_apply (by fun_prop) (by measurability), map_apply (by fun_prop) (by measurability)]
  apply measure_mono
  intro ω
  apply h𝓕
  change {i | U i ω ≤ p} ⊆ {i | U i ω ≤ q}
  rw [Set.setOf_subset_setOf]
  intro x h
  grind

Although this is a discrete probability problem, and the objects involved could in theory be defined using PMF any natural formal translation of the proof would have to use the Unit Interval in some way. (I say "natural" because I believe you could construct the coupling using only discrete spaces but it would be harder and necessarily further from the paper argument).

[Peter Pfaffelhuber]

Nice approach for the coupling! (Percolation would be another nice example.)

If the goal is to show monotonicity, it would suffice to take two values (p q : ℝ≥0∞) (hp : p ≤ 1) (hq : q ≤ 1) (hqq : p ≤ q) and some bernoulli p hp and bernoulli (q - p) _, and add them to have bernoulli p _ for the coupling. This would not leave the space of PMFs.

[Yuval Filmus]

Peter Pfaffelhuber said:

Nice approach for the coupling! (Percolation would be another nice example.)

If the goal is to show monotonicity, it would suffice to take two values (p q : ℝ≥0∞) (hp : p ≤ 1) (hq : q ≤ 1) (hqq : p ≤ q) and some bernoulli p hp and bernoulli (q - p) _, and add them to have bernoulli p _ for the coupling. This would not leave the space of PMFs.

If you add (actually, take the maximum of) Ber(p) and Ber(q-p) you don't get what you want. The second Bernoulli should have bias (q–p)/(1–p).
Another approach would be to directly sample both variables: (0,0) w.p. 1–p, (0,1) w.p. q–p, (1,1) w.p. p. The marginals would have laws Ber(p) and Ber(q).
The approach using U(0,1) has the advantage that we get a coupling of G(n,p) for all p at once. This allows us to state results such as "a.a.s., G(n,p) becomes connected the moment the last isolated vertex disappears".
It would be nice if all of these arguments would be easy to state.

Another nice nugget is to show that if you sample G(ℕ,p) for any constant p, then almost surely you get the same graph (up to isomorphism), known as the countable random graph or Erdos–Rado graph, which also has simple explicit constructions. The probabilistic part of the proof boils down to Borell–Cantelli, and involves some easy calculation.

We would know that we have a workable theory of discrete probability when results such as these become manageable to prove.

[Peter Pfaffelhuber]

Thanks for correcting by Bernoulli-calculation. Just one quick note: If you have a probability space with multiple (infinitely many?) $U(0,1)$ random variables, you certainly leave the space of discrete probability (although the objects you aim to construct are discrete). One of my goals is to introduce do-notation, such that you are able to write something like:

noncomputable def binom (p : ℝ≥0) (h : p ≤ 1) (n : ℕ) :=
example (p : ℝ≥0) (h : p ≤ 1) (P : ℕ → MassFunction ℕ) (zero : P 0 = pure 0) (succ : ∀ n, P (n + 1) = do
    let X ← P n
    let Head ← coin p h
    return X + Head.toNat) : P = binom p h

This will at the moment (i.e. restrictions in do notation) not work if $U(0,1)$ random variables are used.

[Peter Pfaffelhuber]

I started to PR my ideas to mathlib (#34138)

[Peter Pfaffelhuber]

Thanks, @David Ledvinka for the review! Can we please discuss the consequences of changing

noncomputable def toMeasure (w : MassFunction α) : @Measure α ⊤ :=
  Measure.sum (fun a ↦ (w a) • @Measure.dirac α ⊤ a)

to a version where the sigma-algebra is a variable which defaults to ⊤, i.e.

noncomputable def toMeasure' (w : MassFunction α) (mα : MeasurableSpace α := ⊤) : Measure[mα] α :=
  Measure.sum (fun a ↦ (w a) • @Measure.dirac α mα a)

At first glance, this means that all calculations with toMeasure' involving some s : Set α will need to show/assume MeasurableSet s. I want to avid this, since (i) as a more accessible approach to discrete probability, measurability should never be an issue for MassFunction, (ii) often it simply depends on the sigma-algebra if measurability is in fact true, so I will have to assume several things about mα in various places and (iii) in the (not yet PRed) code treating MassFunction as a monad, I will have to require MeasurableSpace α = ⊤.

For the standard finite/countable types, there are things like Bool.instMeasurableSpace or Nat.instMeasurableSpace, giving the correct ⊤ sigma-algebra anyway.

However, there is the case, where one wants to define something like a binomial distribution on ℝ, which is equipped with the Borel sigma-algebra. In this case, it is unclear how to proceed.

My suggestion would be to use a trimmed version of binomial.toMeasure to the Borel sigma-algebra, instead of carrying around the sigma-algebra in many lemmas. So, my suggestion is to provide some API to show equality of a sum of diracs in case they are not defined on ⊤.

[Peter Pfaffelhuber]

As an example, I would try to show:

noncomputable def coinReal (p : ℝ≥0∞) : MassFunction ℝ :=
fun (b : ℝ) ↦ if b = 1 then (p : ℝ≥0∞) else (if b = 0 then (1 - p : ℝ≥0∞) else 0)

example {α : Type*} [MeasurableSpace α] (P : Measure α) [IsProbabilityMeasure P] (s : Set α) :
Measure.map (s.indicator 1) P =
(coinReal (P s)).toMeasure.trim (le_top) := by
  sorry

[David Ledvinka]

I just wanted the flexibility for toMeasure and wasn't asking you to provide the API for the rest of MassFunction, since in this case I think it would be provided with API for diracs and sums of measures anyway. I thought you wouldnt have to change any of the rest of your code, however I didn't actually test it and appears it doesnt work this way. In this case I would just provide a secondary toMeasure (with whatever name) with this feature.

[David Ledvinka]

Also its worth noting that you may run into the problem you describe even with finite and countable types. For example:

import Mathlib

open MeasureTheory

def mΩ₁ : MeasurableSpace (ℕ × ℕ) := by infer_instance

def mΩ₂ : MeasurableSpace (ℕ × ℕ) := ⊤

example : mΩ₁ = mΩ₂ := by rfl -- error

example : mΩ₁ = mΩ₂ := by
  simp [mΩ₁, mΩ₂]
  ext; constructor <;> intros <;> measurability

noncomputable def μ : Measure (ℕ × ℕ) := Measure.dirac (0,0)

noncomputable def μ' : Measure[⊤] (ℕ × ℕ) := @Measure.dirac (ℕ × ℕ) ⊤ (0,0)

example : μ = μ' := sorry -- error

/- Type mismatch
  μ'
has type
  @Measure (ℕ × ℕ) ⊤
but is expected to have type
  @Measure (ℕ × ℕ) Prod.instMeasurableSpace -/