Probability projects

Stream: general

[Rémy Degenne]

There will be a Lean for the Curious Mathematician event next week in Düsseldorf with several days of tutorial and a colloquium at the end. I am giving a talk in the colloquium, which will be about probability in mathlib.
In the last part of the talk, I want to highlight formalization projects in probability that could now be done, given what is already in mathlib. I want to focus on small to medium scale projects that could interest people that are relatively new to Lean and want to start with something cool related to probability. I have a short list of topics but the best way to have diverse and interesting ideas is to ask everybody, hence this message.

Do you have ideas about fomalization goals related to probability that could interest new contributors? Also, would you like me to tell people to contact you about that project, for you to work with them or guide them?

[Yaël Dillies]

There are many low hanging fruits in probabilistic combinatorics now that the basic definitions are done in LeanCamCombi. My code is still in Lean 3, but I have acquired mathport output and can get it ready for next week. Feel free to tell people to contact me!

[Rémy Degenne]

Thanks! Do you have a concrete example of one of those low hanging fruits?

[Kevin Buzzard]

What happened to the hedetniemi project? Could that be done now or is it old news?

[Jason KY.]

How about setting up the theory for white noise. It shouldn't be too difficult and it will finally let Kevin say that we have the Gaussian.

[Yaël Dillies]

Hedetniemi is too hard. Its prerequisite (there are graphs of arbitrarily large chromatic number and girth) is definitely doable although I'm not sure it is new contributor-doable.

[Kevin Buzzard]

Oh yes let me +1 the Gaussian -- Martin Hairer told me years ago that he would expect to see that in any formalised mathematics library. @Jason KY. you have a sketch plan for the formalisation, right?

[Jason KY.]

I do not. I had a sketch for the formalization of the Gaussian in Rn which was formalized by @Joy Hu but I don't think thats the correct generality that Martin was talking about

[Yaël Dillies]

Okay, there's a stupid problem for the chromatic-girth theorem: We have no definition of girth! Let me fix that quickly.

[Vincent Beffara]

Something like https://en.wikipedia.org/wiki/Abstract_Wiener_space should be closer to what Martin would call "the Gaussian", and it might be doable.

[Jason Rute]

Here are some ideas off the top of my head

• look for important theorems in other prob formalizations like https://github.com/IBM/FormalML
• go through an undergraduate probably book and look for topics there to formalize
• same but a statistics textbook
• overall probability is about applications both outside pure math, but also inside pure math like in probabilistic combinatorics. One really wants to be able to use this probability theory library for all sorts of basic examples. The notation of prob theory is really designed to make it easy to do prob theory quickly and abstract away all the measure theory details. Can mathlib’s library be used with that level of easy. To stress test it just try to formalize lots of basic examples of probabilistic arguments. For example:
  • the first proof in probabilistic graph theory is often that $R(k,k) > 2^{k/2}$ (see here
  • basic problems about percolation numbers on infinite random grid graphs
  • really just opening up a graduate or undergraduate probability text book and looking at the exercises (not the ones about measure theory, but the ones about problem solving)

[Yaël Dillies]

@Bhavik Mehta has already done your first bullet point.

[Bolton Bailey]

We have now an open PR #5297 for the Schwartz-Zippel lemma which is sorry-free. Part of my goal in writing this was to do something along the lines of verifying probabilistic proofs.

[Bolton Bailey]

I think this goal doesn't exactly fit into the framework of "specific formalizations of mathematical theorems or definitions that can now be done due to new mathlib definitions" but is more along the lines of "New FM/PL techniques that could be developed, but for which we were lacking the ability to do a proof-of-concept without these mathlib theorems".

[Bolton Bailey]

I think Kevin's suggestion here is pretty interesting. You could call it a "derandomizing axiom of choice" or something.

[Kevin Buzzard]

Oh yeah, it would be a cool project to prove that some primality test worked "with probability at least 1/2" or whatever; one could formalise this by saying that if we tried it with all possibilities for the "random" input, at least half would fail if the number isn't prime.

[Kalle Kytölä]

Nice!

Let me add some ideas (various levels of difficulty, but I believe most of these are still not unreasonable given the current state of Mathlib).

Ideas involving somewhat conrete calculations:

• Construct standard distributions on $\R$ (uniform distribution on an interval, exponential distribution, one-dimensional gaussian, Cauchy-distribution, gamma-distributions, ...) and provide results about their cdf, density (Radon-Nikodym derivative), expected value, variance, higher moments, cumulants, continuity with respect to parameters (#6551 provides a cheap route to cases where parameters amount to scaling and shift or other applications of continuous transfromations), Laplace transform or characteristic function, ...
  • (Some steps involve explicit integrations of real functions, which makes these probably rather difficult projects!)
• Univariate extreme value statistics for i.i.d. random variables (i.e., somewhat explicit calculations with cdfs of maxima/minima of i.i.d. random variables, but nothing as bad as actually explicit integrations; Gumbel, Fréchet, and Weibull limits).
  • (To connect the cdf convergence to convergence in distribution will be easy once the last implication of portmanteau lands.)

Less calculation-heavy ideas:

• Construct the total variation distance between probability measures on a given space (hopefully an easy project).
• Construct the Lévy-Prokhorov metric on probability measures on a metric space (this part should be very doable!). Prove that it metrizes the topology of weak convergence if the underlying space is Polish (this should be doable once the last implication of portmanteau lands).
• Construct arbitrary products of probability measures (not just finite products). I haven't checked the status of the existing extension theorems for measures in Mathlib, so it is unclear to me how much is missing.
• Prokhorov's theorem, Lévy inversion (of "Fourier transform"), and then the Central Limit Theorem. There is a cheap way to get the Prokhorov's theorem on $\R$ (a.k.a. Helly's selection theorem) with cdfs, and this suffices for the CLT, but my personal preference is to do Prokhorov via Riesz representation theorem (PRs planned but not properly started yet) in good generality right away.
• Some applications of Kolmogorov's 0-1-law docs#ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTop (e.g., deterministic radius of convergence for random power series with independent coefficients, ...)

[Kalle Kytölä]

Vincent Beffara said:

Something like https://en.wikipedia.org/wiki/Abstract_Wiener_space should be closer to what Martin would call "the Gaussian", and it might be doable.

Yes! Gaussians in a good generality would be absolutely lovely, and probably rather doable! The Wikipedia link you give is definitely in the right spirit, but what are the good references? I can mainly think of Svante Jansson's Gaussian Hilbert Spaces. (But is this still too specific for the Mathlib generality?)

[Rémy Degenne]

Thanks everyone for all the ideas!

@Kalle Kytölä , the directions you highlight overlap a lot with the ones I noted. In particular it would be good to have all the standard distributions and we need to flesh out our tools to describe them. Right now we have for example definitions for cdf and pdf but not many of their properties or links between them.

About the Gaussian distribution: I would love to have it in a very general way and that sounds like a cool project. I also think that having a Gaussian on R^n now might be better than waiting for the full generality. It looks like some people have had that on branches or personal repos for a while and it would be great to see a PR.
With @Peter Pfaffelhuber we have finished a formalization of Kolmogorov's extension theorem (PRs coming after LftCM) and a natural follow up to that could be to define a Brownian motion. I am not sure one of us will do it: other interesting projects may monopolize our attention instead. To define the Brownian motion, two small and very doable projects are building a family of Gaussians indexed on finsets of the reals on one hand, and proving the Kolmogorov continuity theorem on the other hand.

@Jason Rute , thanks for the ideas and for pointing out FormalML. I know about that repository (and exchanged a pair of emails with the authors at some point) and it indeed contains interesting results. The authors also have an interesting approach which is quite different from ours: they seem to build the tools they need in just the right generality to get to their goals and not more, while our probability theory folder contains a lot of code to do the foundations in great generality (which means slower progress towards applications).
There are also a few entries in Isabelle's AFP about Markov decision processes which can inspire mathlib projects.

Something else I saw recently in other theorem provers is https://www.isa-afp.org/entries/Executable_Randomized_Algorithms.html, in which the authors build executable algorithms that consume coin flips as a source of randomness and build links between the algorithms and the probability mass functions that describe their outcomes. Related to that, I would love to be able to prove things about algorithms that interact with a random environment and also actually run them in experiments. That sounds however more long term, especially if we want to deal with continuous random variables and the related issues of floats approximating reals etc.

About probabilistic algorithms like Miller-Rabin, I feel like I need to read all those threads to understand more what we could want to prove about them.

The talk is on Thursday, so if someone thinks about something else (especially something neatly packaged like "prove theorem X!") please let me know.
After the talk I'll gather all those in a document somewhere.

[Peter Pfaffelhuber]

There are certainly many things to be done. Let me add some opinions and ideas:

• In my opinion, many projects involving concrete probability distributions will benefit from an implementation of characteristic functions, which is still lacking. As an example, not all Gaussian distributions on $\mathbb R^n$ have a density, but all have a (unique) characteristic function. In addition, computing moments in various cases is much simpler once the characteristic function is available. (Other examples where characteristic functions may be advantageous include the proof of two rvs to be identically distributed, e.g. $U \sim 1-U$ for $U\sim U([0,1])$ or $-\log U \sim \exp(1)$, or the thinning of a binomal/Poisson distribution is again binomial/Poisson, or the introduction of infinitely divisible distributions.)
• In geometric probability, it is an exercise to prove Buffons needle problem, which is among the list of 100 theorems (if one cares about lists).
• With the formalization of the Kolmogorov Extension Theorem, it is also possible to define a probability space with (countably) infinite iid rvs. This allows to state and prove Kolmogorov's 0-1-law, or to define e.g. percolation or a simple random walk. For percolation, it could be a project to define the model and the event "there is an infinite cluster", for the random walk, the law of iterated logarithm could be achieveable.
• I really like the idea to prove that certain algorithms (which use coin flips, or $U([0,1])$-rvs) produce an output with a certain distribution. This is actually often a problem in applications (mathematical biology in my case).

[Rémy Degenne]

Good point about the characteristic function. It's also an interesting project because it could use the relatively new Fourier transform files in mathlib.

We already have Kolmogorov's 0-1 law. See docs#ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTop . But we don't have any application of that theorem.

[Peter Pfaffelhuber]

Interesting, I was not aware of the formalized Kolmogorov 0-1-law. Then, a project could be: (i) define percolation of any infinite graph (i.e. for some $p$, say any edge is open independently probability $p$), and (ii) prove that the probability that there exists an infinite cluster is either 0 or 1.

[Vincent Beffara]

It would be excellent to have some percolation theory formalized in Lean, and I would be very curious about how much of the basic facts are actually doable - there is so much of "one can clearly see" especially for topological statements that it could actually be very nontrivial.

[Peter Pfaffelhuber]

Let me add that monotonicity in precolation would be nice to formalize. For this, you usually use a coupling, and couplings are in general tedious to construct and often come with hand-waving arguments. The one for percolation (for different $p$), however, seems doable.
Another point to make, e.g. on percolation is: Usually, you write something like: Let $G=(V,E)$ be a connected graph and $X = (X_e)_{t \in E}$ bond-percolation on $G$ with parameter $p$... Here, you are talking more about the distribution of $X$ than on a concrete probability space. In Lean, you always have to construct a probability space first, or is there a way around that?

[Kalle Kytölä]

I agree that these would be very nice!

But for the percolation coupling, one still needs an infinite product $\bigotimes_{e \in E} \mathrm{Uniform}([0,1])$ of probability measures. This is one reason I suggested constructing infinite product measures above. Of course there are workarounds for this particular case and for countable products of Borel probability measures on Polish spaces or whatnot, but I think Mathlib should have the general product of any probability measures.

Another place where the products are needed is in constructions of stochastic processes (even discrete time finite state space Markov chains, let alone more general ones).

(Of course often one can get away assuming that something follows a product measure. In Lean just as in math, you can assume that $(X_e)_{e \in E}$ is a collection of independent random variables --- this we can readily spell with docs#ProbabilityTheory.iIndepFun . This is enough for, e.g., applying the $0$-$1$ law to the event of the existence of an infinite percolation cluster. But at times --- such as for proving monotonicity for percolation --- one actually needs to construct the product measure.)

[Kalle Kytölä]

Another related nice small(ish?) probability project is FKG-inequality, or probably more appropriately the Ahlswede-Daykin inequality. I think these would be rather doable (right away) and useful "probability" projects. (Although the formalization can essentially avoid any use of probability theory...)

[Bhavik Mehta]

I believe @Yaël Dillies has done this

[Yaël Dillies]

FKG is not done yet but AD is, although not in Lean 4.

[Kalle Kytölä]

Oh, nice! Do you have a link to a repo and do you plan to PR it in Mathlib4? I would really love to see it (+Holley+FKG) in Mathlib.

[Yaël Dillies]

Let me dig it up!

[Yaël Dillies]

Btw this is why we have things like docs#Finset.sups

[Vincent Beffara]

Great! Then in terms of percolation, the existence of the critical point should be easy, and the fact that it is positive on a graph of bounded degree should not be too difficult. Proving $p_c<1$ on the square lattice on the other hand, would already be a good test of the probability and graph parts of mathlib and how they interact.

[Kalle Kytölä]

I absolutely love this prospect. But in addition to Kolmogorov's 0-1 law, the existence of the critical point still needs monotonicity, right? Do you see a satisfactory path to monotonicity without constructing the general products of probability measures? (Of course it is just another extension theorem, and many have been done already, so maybe not prohibitively difficult but...)

I fully agree that $p_c(\Z^2) < 1$ is going to be an interesting new kind of test for Mathlib!

[Yaël Dillies]

I think the existence of the critical point is a consequence of Bollobas-Thomason? Not sure though.

[Vincent Beffara]

The definition of the critical point directly in infinite volume is a direct consequence of monotonicity. But indeed it would be great to have some general theory on sharp thresholds as well!

[Yaël Dillies]

This is part of the stuff I'm formalising for LeanCamCombi since it appeared in the Extremal & Probabilistic Combinatorics course this year.

[Vincent Beffara]

Are you doing BKKL and OSSS and all that ?

[Yaël Dillies]

What are those?

[Vincent Beffara]

Criteria on the existence of sharp thresholds in terms of influences or in terms of stochastic algorithms. Many "modern" proofs in perxolation are based on those, e.g. recent work by Duminil-Copin et al

[Mauricio Collares]

I assume the first one is BKKKL (i.e. https://link.springer.com/article/10.1007/bf02808010)

[Yaël Dillies]

Never heard of those! I'm approaching the subject from the (very discrete) combinatorics side of things.

[Vincent Beffara]

Mauricio Collares said:

I assume the first one is BKKKL (i.e. https://link.springer.com/article/10.1007/bf02808010)

Ooops - yes, either this one, or KKL https://ieeexplore.ieee.org/document/21923

[Bolton Bailey]

The talk is up now. I definitely like the idea of multi-armed bandits as a formalization target, there are indeed a few achievable basic results in that field that would be broadly useful.

[Yaël Dillies]

Kalle Kytölä said:

Oh, nice! Do you have a link to a repo and do you plan to PR it in Mathlib4? I would really love to see it (+Holley+FKG) in Mathlib.

See https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Discrete.20correlation.20inequalities !

[Yaël Dillies]

Is there any plan to formalise the Kolmogorov extension theorem?

[Rémy Degenne]

Peter Pfaffelhuber and I have formalized that theorem over the summer. We only need to find time to PR it. I may start with a first piece today.

[Ruben Van de Velde]

Is the code anywhere public?

[Bjørn Kjos-Hanssen]

Kalle Kytölä said:

I agree that these would be very nice!

But for the percolation coupling, one still needs an infinite product $\bigotimes_{e \in E} \mathrm{Uniform}([0,1])$ of probability measures. This is one reason I suggested constructing infinite product measures above. Of course there are workarounds for this particular case and for countable products of Borel probability measures on Polish spaces or whatnot, but I think Mathlib should have the general product of any probability measures.

Where can I find countable products of Borel probability measures on Polish spaces?
I assume the general infinite product measure construction is still missing
https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Constructions/Pi.html#MeasureTheory.Measure.pi_def

[Kalle Kytölä]

I don't think they exists. In the quoted comment I intended to say that there would (in principle) be unsatisfactory ways ("workarounds") to implement products in lesser generality (something like countable products with nice enough spaces). But in my opinion Mathlib should go directly for the full generality.

A workaround for countable product of $[0,1)$ is to map $[0,1) \to [0,1)^\N$ by considering binary representations of $x \in [0,1)$ and then out of the sequence of bits get a sequence of sequences of bits by an enumeration $\N \to \N \times \N$. The push-forward of the Lebesgue measure on $[0,1)$ is then a measure on $[0,1)^\N$ which is a countable product of Lebesgue measures on the factors. (You can then get countable products of probability measures on other nice spaces $\mathfrak{X}_n$ by combining this trick with pushing forward the Lebesgue measures on the $[0,1)$'s further by measurable maps $[0,1)\to\mathfrak{X}_n$.)

But to summarize, I don't think anything beyond finite products of probability measures exists currently! And I still don't think Mathlib should settle for anything less than arbitrary products of probability spaces.

[Kalle Kytölä]

Note that for non-probability measures, the finite product case is the most general reasonable, so docs#MeasureTheory.Measure.pi_def is good generality.

[Kalle Kytölä]

(And to be clear, for the percolation coupling mentioned, the specific trick of $[0,1)^\N$ is immediately sufficient: $\bigotimes_{e \in E} \mathrm{Unif} ([0,1])$ is of this form, since the edge set $E$ is countable.)

[Bjørn Kjos-Hanssen]

Thanks @Kalle Kytölä I am mostly wondering if fair coin measure on ℕ → Bool has already been constructed.