Probability Distributions: Reasoning by Representation

Stream: mathlib4

[Alvan Arulandu]

I've been curious to formalize facts like Gamma(n,r) \sim \sum_{i\in [n]} \Expo(r)_i where the latter are i.i.d. It seems like this is doable with what's been currently proven in the Probability module, but wanted to ask since these facts are super fun!

[Thomas Zhu]

As far as I know, that has not been done before. Indeed this is would be fun to do and will have future applications (e.g. if we were to formalize Poisson processes).

[Thomas Zhu]

For this particular one, I think it would be easier to show this for the sum of two Gamma distributions, since an exponential is a special case of a Gamma distribution. A common way to show these sum relations is via characteristic functions / moment generating functions, which is only preliminarily done in the (inactive) CLT project [Edit in 2025: characteristic functions are much more comprehensively done in some Mathlib PRs]. In any case to show these, one likely needs some notion of convolution between measures / pdfs, which we have at docs#MeasureTheory.Measure.conv (edited)

[Alvan Arulandu]

Yeah, I was planning to approach this with MGF and convolution, but didn't realize that the latter didn't exist yet. How would we go about creating a notion of convolution?

[Rémy Degenne]

See that message for an example of how you can define a convolution of measures: https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Switch.20order.20of.20product.20of.20measurable.20spaces/near/410563609

[Rémy Degenne]

That is, you can define it as the map by the addition of the product of the two measures.

[Thomas Zhu]

I guess then one would still need to relate MeasureTheory.Measure.conv with MeasureTheory.convolution, i.e. show perhaps under continuity assumptions, that rnDeriv (μ ∗ ν) volume is rnDeriv μ volume ⋆ rnDeriv ν volume, so we can plug in PDFs for Gamma? Has that been done before?

[Rémy Degenne]

I just realized that the convolution of measures is in Mathlib: MeasureTheory.Measure.conv

[Rémy Degenne]

Since the file containing the definition is not imported by anything else, all we have about it is in that file.

[Thomas Zhu]

I also thought they were not in mathlib too :sweat_smile: and then I saw the PR in your link

[Alvan Arulandu]

So, it seems like this could be attainable? Generally, I think having lemmas for facts like Expo \sim -log(U), Beta(a,1) \sim U^{1/a}, and similar could be very nice.

[Thomas Zhu]

I'm not sure how easy the proof for relating conv withconvolution is. By the way, we don't have the Beta distribution yet, but it should be very doable

[Rémy Degenne]

Alvan has an open PR for the Beta distribution: #16773. It is currently waiting for #17176, which has label awaiting-author.

[Alvan Arulandu]

I just finished midterms, so hopefully we'll be able to close ^ shortly!

[Josha Dekker]

I added convolution of measures a while back, but the API I added was very rudimentary! Please feel free to add API