About common distribution independence-additivity lemmas

Stream: mathlib4

[huaizhangchu]

Hi everyone,

I’m working with probability theory in mathlib, and I noticed that some commonly used properties — such as independence additivity for common distributions(for example: sums of independent Poissons, exponentials, etc.) — are frequently needed in practical proofs.

Before I start preparing a PR, I’d like to ask:
Do you think these lemmas belong in mathlib?

Is there an existing place in the library where such results should live?

Are there related ongoing efforts or recommended directions I should review first?

My motivation is to help reduce boilerplate and make probabilistic reasoning more convenient. I’m happy to contribute if this aligns with current goals of the probability theory library.

Thanks for your advice!

[Kevin Buzzard]

@Bhavik Mehta and @David Ledvinka have been thinking about making probabilistic reasoning more convenient in mathlib over the last few weeks (motivated by my Annals-formalisation project; the Annals has published several theorems in probability in the last few years).

[huaizhangchu]

Kevin Buzzard 說：

Bhavik Mehta and David Ledvinka have been thinking about making probabilistic reasoning more convenient in mathlib over the last few weeks (motivated by my Annals-formalisation project; the Annals has published several theorems in probability in the last few years).

Thanks again for the pointers!
Just to mention — I’m still quite new to mathlib and to contributing, so I’m very happy to learn and follow existing plans. My current motivation came from actually needing these lemmas in some work I’m doing, and I thought they might be useful more broadly.

If there is anything I should read or any way I could help (even small tasks), I’d love to try!

[David Ledvinka]

These sound useful but I am not entirely sure what you mean. Maybe post the statements of the lemmas? In general Mathlib is missing a lot of basic probability stuff which should/will eventually be there.

[Etienne Marion]

I guess something like ProbabilityTheory.gaussianReal_add_gaussianReal_of_indepFun for other distributions

[Etienne Marion]

This should probably be stated in terms of ProbabilityTheory.HasLaw by the way.

[huaizhangchu]

Thanks a lot for the feedback!

Yes — what I had in mind is similar to ProbabilityTheory.gaussianReal_add_gaussianReal_of_indepFun: lemmas stating that the sum of independent random variables with certain distributions has another known distribution (e.g. Poisson, Binomial, Exponential, etc.).

I’m considering experimenting with adding a new section within the corresponding distribution files (e.g. Poissons, exponentials, …) to develop independence-additivity lemmas, probably phrased using ProbabilityTheory.HasLaw as @Etienne Marion suggested.

Do you think this approach makes sense from a design perspective?
Or would it be better to place them somewhere more general (e.g. in a dedicated file for probabilistic reasoning infrastructure)?

I’d really appreciate any guidance before I start drafting something.
Thanks again for the suggestions!

[Etienne Marion]

I think it makes sense to have each statement in the folder corresponding to the distribution, so eg the result about Poisson should go in the file about Poisson distribution. For the exponential this should go in the folder about the Gamma distribution.

[huaizhangchu]

Thanks a lot, that makes perfect sense — I’ll try putting each lemma in the corresponding distribution file and see how it works out.
Thanks again for the guidance!

[David Ledvinka]

Binomial is currently in active PRs (see #31908 and #28248), but I think Poisson and Exponential should be fair game.

There has been some discussion recently on how discrete distributions should be defined but nothing concrete decided. I have advocated for moving away from the PMF approach and using a linear combination of diracs instead (Poisson is already defined in Mathlib using the PMF approach). There is another formalisation specific issue: which domains should we primarily develop the random variable APIs (and measures) for? As the most extreme example, for positive finite distributions one could define them on Fin n, ℕ, ℤ, ℝ≥0, ℝ. Should these all be defined in Mathlib with the appropriate relations and duplicated APIs for each one? Note for exponential we don't have a ℝ≥0 version. My current opinion is that perhaps the answer for distributions like Poisson is ℕ or ℤ and ℝ but I am very unsure here. Nevertheless perhaps its hard to know the right answers to these problems without getting it wrong first. So I encourage you to just try "something", but I figured I would give you a sense of a few of the "formalization specific" issues in this area.

[huaizhangchu]

Thanks a lot for the detailed explanation — this gives me much clearer context about the design questions around discrete distributions, PMF vs. linear combination of diracs, and domain choices. I really appreciate the overview.

Since Poisson and Exponential seem like fair starting points, I’ll explore drafting a few concrete independence-additivity lemmas in the current structure without committing to strong architectural choices. Then hopefully we can evaluate whether this direction fits well or needs adjustment.

I’ll also take a careful look at the active Binomial PRs (#31908 and #28248) so that whatever I try stays consistent with ongoing work.

Thanks again for the encouragement!

[Etienne Marion]

I am guessing that you are writing with an LLM. If that is the case, I think it would have been nice to say it from the beginning, as we regularly get AI-generated messages coming from people who completely rely on AI and produce very low quality conversations. I am not saying it is your case, it does look like you are willing to learn and contribute which is great!

[Rémy Degenne]

David Ledvinka said:

There has been some discussion recently on how discrete distributions should be defined but nothing concrete decided. I have advocated for moving away from the PMF approach and using a linear combination of diracs instead (Poisson is already defined in Mathlib using the PMF approach). There is another formalisation specific issue: which domains should we primarily develop the random variable APIs (and measures) for? As the most extreme example, for positive finite distributions one could define them on Fin n, ℕ, ℤ, ℝ≥0, ℝ.

I agree that weighted sums of Diracs seems like a better approach than PMF.
For the domain, it looks like a tricky question that depends a lot on what you want to do with the distribution in your application. I recently implemented Bernoulli distributions for a project, in which it was very convenient to have a space with two points, but I also got to Bernoulli by mapping real distributions while not changing the mean, so having something not too far from ℝ was important. To my surprise, I ended up choosing the subtype ({0, 1} : Set ℝ). I will never advocate for that to be the standard domain for Bernoullis, so it would be nice to somehow have an implementation in Mathlib that can apply to multiple two-points domains.

[David Ledvinka]

Yeah I agree that for specific applications it depends. I guess (for Mathlib) its a balancing act of maintainability, usability and flexibility. Infact I have written up a "two-point distributions" file multiple times but never PRed anything because I have been unhappy with some part of the design. I definitely think I tend to be "too" perfectionist though.

May I ask why just having it be a measure on ℝ (say defined like p • .dirac 1 + (1 - p) • .dirac 0 or equivalently pushing the measure defined on a smaller type into ℝ) didn't work for you? I ask not because I doubt you but because I want to collect all the different considerations for design.

[Rémy Degenne]

I was manipulating a quantity similar to a Renyi divergence, which is an infimum over probability measures of something. If my measure was on Real I would have to argue that the minimum was attained at a Bernoulli distribution (otherwise the thing in the infimum would be infinite). With a measure defined on a two points space I get it automatically and can compute the divergence easily.

[huaizhangchu]

Etienne Marion 說：

I am guessing that you are writing with an LLM. If that is the case, I think it would have been nice to say it from the beginning, as we regularly get AI-generated messages coming from people who completely rely on AI and produce very low quality conversations. I am not saying it is your case, it does look like you are willing to learn and contribute which is great!

Thanks for pointing that out — and apologies for not mentioning it earlier.
Yes, English is not my first language, so I sometimes use an LLM to help polish my wording, but the ideas and technical content are my own. I will make sure to state this explicitly next time.

I really appreciate your understanding and the guidance so far. I’m genuinely trying to learn and contribute, and I’m grateful for the patience and help from the community.