Question about proving additivity of the Poisson distributio

Stream: mathlib4

[huaizhangchu]

Hi everyone, I’m a beginner using Lean, and I really hope to contribute to mathlib. My direction is probability and statistics. After organizing some materials, I found myself interested in the independent additivity of common distributions. The main reason is that in gaussianReal there is already a proof of independent additivity that can be used for reference, but for other distributions such as Poisson and Gamma, it seems they are not covered yet (please correct me if I’m wrong).

I started learning from the Poisson distribution. I found that Poisson is mainly defined from the PMF perspective. If I want to prove independent additivity using convolution like in the Gaussian case, I currently have two ideas:

1. directly compute the PMF convolution using the binomial theorem and combinatorial identities.
2. find a way to embed ℕ into the existing frameworks such as continuous convolution / charFun / mgf. I didn’t find support for discrete cases (maybe I searched incorrectly), so if there are related files or PRs, I would really appreciate pointers.

I would be very grateful for any suggestions about which direction might make more sense, or if there are better approaches. Thank you!

(English is not my first language, so I’m using AI to help translate my text. The technical ideas and questions are my own.)

[David Ledvinka]

I suspect the easiest way to do it will be to use charFun. Especially since we will also want to have the charFun in mathlib anyway and once you have that its very easy to prove the result you want. I have some examples of doing this with discrete distributions here: #mathlib4 > Discrete Probability Proposal (but none of this is in mathlib). I am not sure I would do things exactly like I do them in that thread but the main insights imo is that for "embedding" them into the existing framework the nicest thing to use is a linear combination of diracs (so the Poisson distribution on ℝwill be an (infinite) linear combination of diracs on the natural numbers with the coefficients being given by the "PMF" of the Poisson distribution).

[David Ledvinka]

If you also want the result for the measures on ℕ directly you can then use the fact that the pushforward of measures from ℕ to ℝ is injective to "pullback" the result.

[huaizhangchu]

David Ledvinka 說：

I suspect the easiest way to do it will be to use charFun. Especially since we will also want to have the charFun in mathlib anyway and once you have that its very easy to prove the result you want. I have some examples of doing this with discrete distributions here: #mathlib4 > Discrete Probability Proposal (but none of this is in mathlib). I am not sure I would do things exactly like I do them in that thread but the main insights imo is that for "embedding" them into the existing framework the nicest thing to use is a linear combination of diracs (so the Poisson distribution on ℝwill be an (infinite) linear combination of diracs on the natural numbers with the coefficients being given by the "PMF" of the Poisson distribution).

Got it! I just took a quick look at your proposal about discrete probability. I think I’ll need some more time to study it carefully. Thank you very much for your help!