Looking for how to contribute to mathlib

Stream: new members

[Torey Hilbert]

Hello, I am a student in statistics and I'm interested in trying to contribute to mathlib for topics in either probability theory or theoretical statistics (be that Markov Chains / Stochastics stuff, or stuff about distributions) but I'm not what to do.

I found in src/measure_theory/probability_mass_function/constructions.lean that currently only three-ish distributions are present. Is a desireble first contribution adding a few more common distributions there, and if so, how would I decide which ones? Thank you so much!

[Torey Hilbert]

Also, it's unclear why it's in the measure theory folder when there's a separate folder for proabability, but I figure there's a reason

[Johan Commelin]

Welcome! The folder issue might very well be due to history...

[Johan Commelin]

There's currently stuff happening with martingales.

[Johan Commelin]

@Torey Hilbert Do you already have some lean code somewhere, that you would like to contribute?

[Torey Hilbert]

Not yet, the contributing to mathlib guide suggests asking the Zulip chat before and during writing the code so I figured I wouldn't embark on something if the pulse of the project implied it was a bad idea etc.

[Torey Hilbert]

Thank you for the response btw!

[Johan Commelin]

Yeah, discussing here early on is certainly a good idea!

[Johan Commelin]

How much experience do you have with Lean? Did you follow the tutorials? Or #nng, or something else?

[Torey Hilbert]

Ope sorry for the slow response. I don't have a ton of experience with Lean - I played the natural numbers game a while ago and I'm working through both the tutorials and the measure theory code directly.

[Kevin Buzzard]

Martin Hairer once told me that he couldn't take Lean seriously until it had an API for the Gaussian distribution

[Johan Commelin]

Which seems like a fair point (if you s/Lean/mathlib/)

[Vincent Beffara]

You could try to do e.g. the "hard" direction of Borel-Cantelli (see docs#measure_theory.measure_limsup_eq_zero for the "easy" direction) or start filling in something else in undergrad.yaml, say the laws of large numbers? It could be more motivating than adding the definitions of the usual distributions!

[Rémy Degenne]

Welcome! You may want to have a look at this topic: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Getting.20started.20contributing.20to.20probability.20theory
Since you mentioned markov chains: a useful and interesting direction would be to define markov kernels and conditional probability distributions (https://en.wikipedia.org/wiki/Regular_conditional_probability). The book "foundations of modern probability" by Kallenberg looks like a good reference for that.

[Yaël Dillies]

There's the binomial PMF in branch#hedetniemi.

[Kalle Kytölä]

I agree with @Rémy Degenne that kernels as in Kallenberg looks like a great approach to Markov processes (at least discrete time, but probably beyond).

We have had some discussion that @Jason KY. might do Markov processes in the summer (I'm very happy that he'll be with us at Aalto during the summer :tada:). So to coordinate who is working on what in this area is a good idea. To be clear, I will just be extremely happy when anyone puts Markov processes in mathlib!

[Kalle Kytölä]

I also agree with Vincent (how could I not).

But having various common distributions with more or less similar APIs added to mathlib would be very valuable! And it would not just be about giving the definitions of the distributions: probably one would want to prove a few properties about each distribution to stress test the implementation of the definition. (Say, provide some lemmas about characterizations, at least the cdf and perhaps characteristic function and more interestingly specific ones for each distribution, lemmas about properties such as expected value and variance, etc.). Also many distributions would probably be defined by specifying either their densities or characteristic functions (the latter of which admittedly don't exist yet), so they would serve as tests for parts of the existing library (integration, perhaps Radon-Nikodym theorem, perhaps the still-non-existent characteristic functions, ...). Depending on the background, all of this this might be quite nice!

[Torey Hilbert]

This is very helpful information! I'll try to work towards the Markov Kernels for now, but I'll probably need some guidance and won't hesitate to ask :+1:

[Torey Hilbert]

About the characteristic functions thing, a comment in one of the files mentions that we are waiting on Fourier Analysis results for that. Is it worth pursing just directly proving the relevant results we'd need about characteristic functions instead of waiting?

[Kevin Buzzard]

@Torey Hilbert for a recent overview of a related area you might like @Jason KY. 's London Learning Lean talk here.

[Vincent Beffara]

Perhaps while waiting for Fourier Analysis it would make sense to start with discrete distributions on the integers and to define the generating function instead.