elementary probability advice

Stream: general

[Jeremy Avigad]

I have a student with limited mathematical background -- the only proofs he has seen are in an intro to proof course for non-math majors. He wants to formalize some elementary probability, i.e. discrete spaces only. The mathlib API will force him to figure out measurability, ennreals, etc., and I am worried that he will have a hard time with all that. So instead I encouraged him to use a class that axiomatizes a discrete probability measure directly, i.e. the probability maps arbitrary sets to the reals. Dealing with countable additivity (with tsum) might also be too challenging, but it should be enough for him to use finite additivity.

In short, I am advising him to ignore mathlib's notion of probability and roll his own simpler version to work with. Is there an easy way to get a similar effect using notions in mathlib? I know that pmf.to_measure should provide an instance of whatever he writes down, but I want him to have an API that is as simple as possible.

[Kevin Buzzard]

There is an area called probabilistic graph theory, which uses the language of probability and proves theorems of the form "a graph with the following properties must exist" by arguing that if you fix a sufficiently vertex set and then define edges randomly, the probability that the graph has all the properties is positive, and hence such a graph must exist. This can all be translated down into concrete statements involving counting rather than probability, but my understanding is that when people tried this in the past mathlib's probability API was not particuarly well-equipped to deal with such arguments. The same might be true here. In a finite situation of course finite additivity is enough. I'm wondering whether you're just adding to the evidence that we need to either rethink or simply implement anew probability in this finite setting. @Jason KY. @Bhavik Mehta do you have any thoughts on this?

[Jason KY.]

I think Bhavik has the G(n,p) model formalized in a branch (am I correct?)

[Bhavik Mehta]

Somewhat correct - I have the distribution on finite sets where each element is present iid, probability p with some basic api. But I didn't explicitly link this to mathlib graphs, though it's technically more general

[Jeremy Avigad]

@Kevin Buzzard Yes, I had that in mind. Such an API would be good for teaching, but it should also really helpful for proofs involving the probabilistic method.

[Jason KY.]

Most of the current finite probability stuff in mathlib is built on the measure theory sections (I don't know much about the pmf part of the library so maybe it's different there) so it might be difficult to avoid measure theory if they want to use mathlib. Doing probability without measure theory is certainly doable however (there are libraries in Coq and Mizar that only do discrete probability) and I think @Wrenna Robson was interested in fromalising finite probability without measure theory in Lean.

[Jeremy Avigad]

I don't think it has to be linked to graphs per se. Just a nice library for calculating with finite probabilities, without all the side conditions, would be good. My students are doing a small project now and will do a bigger one after that. I'll see if I can sell it to one of them.

[Wrenna Robson]

Yes. I have less time currently for this stuff as I'm an internship but I do think it would be a good idea. The point is that a lot of fields use this fundamentally "naive probability" view and it's quite useful.

[Wrenna Robson]

As it happens I'm currently on an internship at a quantum computing company and one thing I've been wondering is: what do we actually need to use the language of probabilities as featured in quantum physics/quantum information theory? If I'm entirely honest... I think it's a lot closer to the finite distributions case.

[Wrenna Robson]

Or to pick another applied example that I'm familiar with, look at the use of probability in probabilistic relational Hoare logic.

[Bhavik Mehta]

All of the other probability things I've done were all avoiding the probability library, but I think it's possible to combine them - I can put together a basic example tomorrow of a proof in probabilistic graph theory if it'd be helpful?

[Wrenna Robson]

The point is not so much that we need any one of these things, or graphs, etc. (though it would be good). The point is that there are a number of fields, inside and outside probability, which use probability while not really expecting the user to have any kind of grasp of the true details of measure theory etc.

[Yaël Dillies]

I am taking the Cambridge Extremal and Probabilistic Combinatorics course this term, and I would be very interested in applying the probability theory library in this finite setting.

[Wrenna Robson]

It shouldn't be the case that you have to have that kind of background in order to use it, because as we see here with Jeremy's student, sometimes people don't. We are limiting the ability of mathlib to be a foundation for later work if we don't look at creating a good interface onto naïve probability theory/a "theory of finite distributions". Really a lot of it is "theory of weighted finite non-negative sums where the sum of the weights is 1".

[Bhavik Mehta]

My belief right now is that the current setup can be made to work without a good understanding of measure theory, just with a few examples of how to use it and perhaps a guide, but no need to explicitly talk about any measure theory

[Patrick Massot]

I don't know anything about probability theory, but it seems it would be nice to have a bunch of lemmas relating the general theory to the elementary one, just like we have lemmas recasting all topology definitions in terms of epsilons and deltas when working with metric spaces.

[Wrenna Robson]

My longer-term suggestion for the health and future of the library is to get advice from different people who use probability in different ways when designing this (I have tried to sketch out a few above). I think it's a really good opportunity not simply to do interesting mathematics but to make mathlib better as a foundation for people to do mathematics and mathematical reasoning in a formal context.

[Wrenna Robson]

Yeah agreed Patrick and that wouldn't surprise me Bhavik, but currently we don't have a way into that.

[Yaël Dillies]

Jason and I will probably formalise some of the aforementioned course, and I am planning to take this as an opportunity to develop elementary probability theory in mathlib.

[Wrenna Robson]

Ultimately most of the maths of QM, I think, isn't "really" probability but has a probabilistic interpretation. But that probability does keep coming up.

[Wrenna Robson]

That would be really great Yaël.

[Jeremy Avigad]

Agreed all around. Bhavik, maybe hold off on experimenting? I have some talented students in my class, and this will be a good project if I can talk them into it.

[Wrenna Robson]

One notion I've seen in some areas of probabilistic logic/formal methods btw is the notion of "subdistributions", which are basically just probability distributions where the sum of the probabilities is at most 1 rather than being exactly 1. Quite nice to have the flexibility to allow for things like that if it's natural.

[Jeremy Avigad]

Oh, sorry, our messages are crossing. Yael, Jason, let me know if you are likely to do this within the next month or two.

[Bhavik Mehta]

One thing to bear in mind is that even when working with explicit distributions on finite spaces, some arguments still use infinite spaces under the hood - consider the G(n, p) model of random graphs, and the random variable on it given by "number of k-cliques in the graph". Now the expectation of this rv would be increasing in p, and the easiest way of showing this is to instead assign a uniform [0,1] to each edge, and derive G(n, p) and G(n, p') on that, then the coupled variables give the result immediately

[Wrenna Robson]

Yes. I do worry about this - that there's often sneaky uses of infinite stuff.

[Bhavik Mehta]

And this is precisely what I did (in a more general form) in the branch I mentioned earlier

[Bhavik Mehta]

(actually that's a slight lie - I did the probability of one existing, not the expected number, but the same principle applies!)

[Wrenna Robson]

(For reference: this is the paper I've been reading lately. The author has formalised this content in a tool built on top of Isabelle/HOL-Analysis, if you want a point of comparison of what other libraries can do.)

https://arxiv.org/abs/1802.03188#:~:text=This%20logic%20follows%20the%20spirit,proofs%20of%20classical%20cryptographic%20protocols.

[Wrenna Robson]

See the definition of "distributions" on page 11 (which isn't actually finitary, but it's also not really a measure theory perspective either...).

[Wrenna Robson]

Indeed in a footnote: "we do not consider distributions over arbitrary measurable spaces, only discrete ones".

[Rémi Bottinelli]

Maybe this is totally off, but I was thinking Structured probabilistic reasonning by Bart Jacobs could be a good resource to formalize "elementary" probability theory ?

[Wrenna Robson]

That actually looks really really good.

[Wrenna Robson]

Wow. Yeah no I think that could be a fantastic foundation.

[Rémi Bottinelli]

Great :) Thought so too but one never knows!

[Jason KY.]

Jeremy Avigad said:

Oh, sorry, our messages are crossing. Yael, Jason, let me know if you are likely to do this within the next month or two.

I'm not sure what @Yaël Dillies's timeframe for this is. I don't plan to write too much serious lean for a bit while I'm doing phd applications so I think your student's project won't conflict with us.

[Frédéric Dupuis]

Wrenna Robson said:

As it happens I'm currently on an internship at a quantum computing company and one thing I've been wondering is: what do we actually need to use the language of probabilities as featured in quantum physics/quantum information theory? If I'm entirely honest... I think it's a lot closer to the finite distributions case.

I'd say the situation is quite similar to probability theory: the finite-dimensional case is easy like finite distributions, and in the infinite-dimensional case you have to get into much more complicated stuff like von Neumann algebras.

[Kalle Kytölä]

I completely agree with Patrick Massot , the problem is the lack of an API for finite probability spaces --- and the ideal solution would be an API. Bhavik Mehta's innocent-looking coupling example about graph probability brilliantly illustrates that the API really needs to connect to mathlib's measure theoretic probability.

[Kalle Kytölä]

Incidentally, there was a recent discussion (and a PR #17032) about making probability mass functions (pmf) ennreal-valued, instead of nnreal valued. I did not weigh in, since I have had very little time to contribute, but my fear is such a design choice will make elementary uses of probability more painful. For instance, if $p$ is a pmf on a finite set $S$, and $f \colon S \to \R$ is a function, one would like to write the expectation of $f$ as

$$\mathsf{E}[f] = \sum_{s \in S} f(s) \, p(s) ,$$

but with ennreal-valued pmfs one can't since there is no multiplication of ℝ≥0∞ with ℝ (the summands don't typecheck). So favoring ennreals might be less painful now that there is no API for finite probabilities, but I'm afraid it will be a worse choice once an otherwise good API would be in place. (This had been my rationale for having docs#measure_theory.probability_measure to have a docs#measure_theory.probability_measure.has_coe_to_fun, which is nnreal-valued instead of simply using the underlying docs#measure_theory.measure.has_coe_to_fun, but admittedly a lot of API is missing before this becomes anything more than a pain).

Anyway, no API is a big problem either way!

[Eric Rodriguez]

I'd just like to point out that for the Birthday problem, I recently tried to restate it as the probability of a function being injective (as opposed to the cardinality of the set of functions/cardinality of the set of injective functions) and it was a pain. Further, I'm told that doing something like turning that into the standard interpretation about n independent iid random variables would be "a pain"

[Eric Rodriguez]

https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/93_birthday_problem.lean

This is the relevant code; there weas missing API that I needed to add for simple things, and also some of the lines are pretty "magical" if you don't know Lean

[Sebastien Gouezel]

I feel that we are really missing is a good notation for (ℙ s).to_real when ℙ is a probability measure (or a finite measure, or even a general measure maybe), and then a basic API around this notation. This would make it possible to avoid completely ennreals in a lot of natural situations.

[Kalle Kytölä]

Is it clear real is better than nnreal?

For a few reasons I had thought ℝ≥0 would be better here (in particular nnreals coerce automatically to reals, whereas the other way around one may need positivity proofs) (although an argument for the opposite is that arithmetic on reals is less pathological). Either way, for such a purpose, in my opinion a decent notation is provided by docs#measure_theory.finite_measure.has_coe_to_fun (and docs#measure_theory.probability_measure.has_coe_to_fun), which allows to write simply ℙ s (which gets pretty-printed as ⇑ℙ s). I think making these coercions to functions a default spelling might be a good idea for elementary probability; either keeping them nnreal-valued as they are or real-valued if we prefer that. Then an acceptable notation would exist, but obviously API around that is still missing.

(Just to clarify: measure obviously has an ℝ≥0∞-valued coe_to_fun, but finite_measure and probability_measure currently have an ℝ≥0-valued and could be changed to have ℝ-valued coe_to_funs.)

[Kevin Buzzard]

Two advantages of real: more tactics work with it, and it's what it says in all the books

[Kalle Kytölä]

Also, does someone have clear ideas about what the API should involve? I'm thinking: finite and countable additivity, monotonicity, complement probabilities, at least, maybe monotone increasing and decreasing convergence of measures. Anything connecting to expected values (integration) quite naturally remains ennreal-valued anyway. (Except on finite types with real-valued functions or more generally bounded measurable functions one could even have direct API for expected values with real values. Where real really in mathlib generality means {R : Type*} [normed_add_comm_group R] [normed_space ℝ R] [complete_space R]. But the elementary API choices start to get more complicated already here.)

This means duplicating some amount of API from measure theory (of course proofs get shorter as they only involve coercions from ennreal to whichever of the two finite alternatives we'd choose).

[Kalle Kytölä]

I have been intending to change the notations in this file to ℙ and Ω instead of μ and α, so I think I could give the very basic API a go at the same time.

[Sebastien Gouezel]

I am not sure about the coercion business. My problem is that most probability measure will comes as (ℙ : measure Ω ) [is_probability_measure ℙ], and for these the ennreal-valued coercion is already registered.

[Sebastien Gouezel]

But we could have something like ℙ.real s, which is not too long. And it is not hard to say to a newcomer that the probability of a set is denoted always by ℙ.real s (and please don't ask why).

[Kalle Kytölä]

I'm definitely biased: I construct most of my probability measures as weak limits (thermodynamical limits, scaling limits) of something else, and then they are probability_measures, since that's the type that has the topology of weak convergence.

Also constructing anything from i.i.d. samples often involves infinite product measures, which don't make a lot of sense for measures or even finite_measures, do they?

So I'm not yet sure most probability measures would come as (ℙ : measure Ω) [is_probability_measure ℙ] rather than as (ℙ : probability_measure Ω).

[Wrenna Robson]

Per that link above, I'm not sure if it's finite or discrete probability distributions that we need an API to. Both, quite possibly.

[Wrenna Robson]

The link that Rémi posted, to be clear.

[Wrenna Robson]

I'm really struck by the formalism presented there.

[Wrenna Robson]

c72144e3-3953-4632-8f68-0759b298c90d.jpg

[Wrenna Robson]

It's a serious formalism but it doesn't use a measure-based approach at all, it's doing quite a different thing for different reasons. But I think there could be a place for it.

[Wrenna Robson]

But to me this points to something built on top of multiset.

[Wrenna Robson]

Frédéric Dupuis said:

Wrenna Robson said:

As it happens I'm currently on an internship at a quantum computing company and one thing I've been wondering is: what do we actually need to use the language of probabilities as featured in quantum physics/quantum information theory? If I'm entirely honest... I think it's a lot closer to the finite distributions case.

I'd say the situation is quite similar to probability theory: the finite-dimensional case is easy like finite distributions, and in the infinite-dimensional case you have to get into much more complicated stuff like von Neumann algebras.

Yeah - in quantum information theory one seems to only encounter finite dimensions, but I'm sure there are exceptions to that even there.

[Oliver Nash]

Kevin Buzzard said:

Two advantages of real: more tactics work with it, and it's what it says in all the books

Also ℝ has a well-behaved subtraction. For example I recently added docs#measure_theory.prob_compl_eq_one_sub but as I explain in the doc string, it's not really the lemma I wanted.

[Wrenna Robson]

Aye.

[Wrenna Robson]

And sometimes you do subtract probabilities

[Wrenna Robson]

(and expect negative results)

[Wrenna Robson]

Wrenna Robson said:

Frédéric Dupuis said:

Wrenna Robson said:

As it happens I'm currently on an internship at a quantum computing company and one thing I've been wondering is: what do we actually need to use the language of probabilities as featured in quantum physics/quantum information theory? If I'm entirely honest... I think it's a lot closer to the finite distributions case.

I'd say the situation is quite similar to probability theory: the finite-dimensional case is easy like finite distributions, and in the infinite-dimensional case you have to get into much more complicated stuff like von Neumann algebras.

Yeah - in quantum information theory one seems to only encounter finite dimensions, but I'm sure there are exceptions to that even there.

(I should say: as in, "in the basic or practical approaches I've read".)

[Vincent Beffara]

From probability/notation.lean,

`ℙ` is a notation for `volume` on a measured space

so calling an explicit probability measure ℙ feels a bit dangerous. But on the other hand, one could change the meaning of the notation to instead take real values (so it would be notation for λ s, (volume s).to_real). I'm guessing that this particular notation is almost never used outside probability spaces anyway? Then, newcomers would say ℙ and have their expected behavior, and more experienced users can still use volume explicitly if needed to fit within the general measurable space API.

[Wrenna Robson]

https://arxiv.org/pdf/1804.01193.pdf - This (essentially similar to the other Brett Jacobs pdf above in its approach) proposes a different notation/concept for probability. It has a lot of advantages as I see it, though the disadvantage of being unfamiliar notation. But at least it would avoid a confusion with the measure-theoretic interpretation of probability.

[Kalle Kytölä]

I have two small concerns about @Vincent Beffara's proposal of having ℙ be notation for λ s, (volume s).to_real for elementary probability purposes.

[Kalle Kytölä]

The first is that even in elementary probability one often has multiple probability measures around, so volume might not be a very universal spelling even under the hood (for example conditional probability versions of some original probability measure, coin tosses with different probability of heads, other parametric distributions such as Poisson, Geometric, ...).

[Kalle Kytölä]

The second concern is a technicality and it might not be an issue at all. Would ℙ as notation for λ s, (volume s).to_real allow for natural development of API that would be convenient for elementary probability theory? I'm thinking in particular of rewrite lemmas and especially @[simp]-lemmas. Is it reasonable to find good simp normal forms for expression that involve (volume s).to_real under the hood (although perhaps with type class [is_probability_measure volume] floating around)? Sorry, I'm just not experienced enough with notations; I don't know if the simp normal form with the notation can be different from the simp normal form of the unfolded notation... ...so this might or might not be an issue at all.

[Vincent Beffara]

Kalle Kytölä said:

The first is that even in elementary probability one often has multiple probability measures around, so volume might not be a very universal spelling even under the hood (for example conditional probability versions of some original probability measure, coin tosses with different probability of heads, other parametric distributions such as Poisson, Geometric, ...).

Not sure I would worry too much about this, because the usual theoretical setup is one probability space \Omega equipped with one probability measure P (a.k.a volume) and many random variables defined on \Omega with values in \R, \N and so on. The image measures are different for sure, but they are not volume : to get the probability that a r.v. X is in s we would not say \bbP s but \bbP {\omega | X \omega \in s}. There are certainly the usual issues of constructing conditioned random variables and so on on the same probability space, but I believe we will have these in any case independent of the notation issue.

But come to think of it, \bbP {\omega | X \omega \in s} is definitely not usual probability notation, we would need something closer to \bbP [X \in s] and \bbP [0 < X] and \bbP [X^2 < 1 \and Y \le X] and ... and I have no idea if this is at all feasible.

[Kalle Kytölä]

For conditioning in elementary probability I have in mind for example the fan favorite "covid home test" from freshman proba. I don't think such applications would be rare, especially if Lean were ever used for teaching elementary proba.

import probability.martingale.borel_cantelli
import measure_theory.measure.finite_measure_weak_convergence

noncomputable theory

localized "notation (name := measure_space.volume.to_real)
  `ℙ` := (λ s, (measure_theory.measure_space.volume s).to_real)" in elementary_probability

namespace elementary_probability

open measure_theory ennreal nnreal
open_locale ennreal nnreal

section covid_test

inductive Ω
| true_pos
| true_neg
| false_pos
| false_neg

instance : measurable_space Ω := ⊤
instance : measure_space Ω :=
{ volume := (4 : ℝ≥0∞)⁻¹ • measure.count .. } -- a better example would really use something interesting here, but...

def sick : set Ω := {Ω.true_pos, Ω.false_neg}
def healthy := sickᶜ
def home_test_pos : set Ω := {Ω.true_pos, Ω.false_pos}
def home_test_neg := home_test_posᶜ

def measure_theory.measure.conditioned {α : Type*} [measurable_space α]
  (μ : measure α) (C : set α) := (μ C)⁻¹ • (μ.restrict C)

def ℙ₁ : measure Ω := volume.conditioned home_test_pos

example : ℙ sick = 1 - ℙ healthy := sorry -- 1 ∈ ℝ
example : ℙ₁ sick = 1 - ℙ₁ healthy := sorry -- 1 ∈ ℝ≥0∞

localized "notation (name := measure_space.volume.conditioned.to_real)
  `ℙcond` := (λ s c, (measure_theory.measure_space.volume.conditioned c s).to_real)" in elementary_probability

example : ℙcond sick home_test_pos = 1 - ℙcond healthy home_test_pos := sorry -- 1 ∈ ℝ again

end covid_test

end elementary_probability

It is of course possible (like above) to define yet another specialized notation for conditional probabilities (assuming they are always conditional versions of volume), but this is definitely not my favorite route. My preferred approach would have the conditioning probability_measure Ω → set Ω → probability_measure Ω with junk value default when conditioning on zero probability events or non-measurable sets. And API around probability_measure.has_coe_to_fun. But Sébastien was not convinced of this coe_to_fun approach...

(measure_theory.measure.conditioned above is not well implemented for instance because it doesn't provide the junk values and can't automatically get the [is_probability_measure] type class, but that's beside the point)

[Kalle Kytölä]

Incidentally I also failed to make simp lemmas hit the notation, but this may be just my incompetence:

import probability.martingale.borel_cantelli
import measure_theory.measure.finite_measure_weak_convergence

noncomputable theory

localized "notation (name := measure_space.volume.to_real)
  `ℙ` := (λ s, (measure_theory.measure_space.volume s).to_real)" in elementary_probability

namespace elementary_probability

open measure_theory ennreal nnreal
open_locale ennreal nnreal

variables {Ω : Type*} [measure_space Ω] [is_probability_measure (volume : measure Ω)]

@[simp] lemma complement_proba
  {E : set Ω} (E_event : measurable_set E) :
  ℙ Eᶜ = 1 - ℙ E :=
begin
  have key := @measure_compl _ _ volume _ E_event (measure_ne_top volume E),
  apply_fun ennreal.to_real at key,
  simp only [function.comp_app, key, measure_univ],
  rw [ennreal.to_real_sub_of_le _ ennreal.one_ne_top, ennreal.one_to_real],
  convert measure_mono E.subset_univ,
  simp only [measure_mono E.subset_univ, measure_univ],
end

example {A B : set Ω} (A_event : measurable_set A) (B_event : measurable_set B) :
  ℙ (Aᶜ) = 1 - ℙ (A) :=
begin
  --rw [complement_proba], -- makes progress as intended.
  simp [A_event], -- doesn't trigger the simp lemma `complement_proba`
  sorry,
end

end elementary_probability

[Yaël Dillies]

As a follow-up to this discussion, Jason and I will start formalising the Extremal and Probabilistic Combinatorics Cambridge course content next week, @Jeremy Avigad.

[Yaël Dillies]

I have little idea how much elementary probability we will need.

[Jeremy Avigad]

Excellent! One of my students is working on a proof of the Lovasz Local Lemma. If he succeeds and you don't do it independently, maybe he can work his proof into whatever framework you develop. Please do keep me posted.

[Bhavik Mehta]

Ah Lovasz Local Lemma is a great choice of project!

[Mauricio Collares]

Yaël Dillies said:

As a follow-up to this discussion, Jason and I will start formalising the Extremal and Probabilistic Combinatorics Cambridge course content next week, Jeremy Avigad.

cc @John Talbot, since he has proved some extremal combinatorics results too

[Nathan Glover]

Jeremy Avigad|110865 said:

Excellent! One of my students is working on a proof of the Lovasz Local Lemma. If he succeeds and you don't do it independently, maybe he can work his proof into whatever framework you develop. Please do keep me posted.

I was a bit late on finishing the proof by the course deadline, but I did eventually get it done! Here it is: https://github.com/nsglover/lean-lovasz-local-lemma

[Nathan Glover]

If anyone has any general suggestions I'd be happy to hear them; this is my first time doing anything with Lean. I hear the community is currently switching to Lean 4 so I'll try to do the same for this proof at some point

[Yaël Dillies]

I shall have a look! On our side, LeanCamCombi has been on hold for the holidays, but there is already some interesting API developed there.

[Nathan Glover]

Good to know thanks, I'll take a more in-depth look at some point. It seems really cool at a glance!