Convolution of Poisson PMFs

Stream: mathlib4

[blfang]

Hi all, this is my first attempt at contributing to mathlib4: https://github.com/leanprover-community/mathlib4/pull/12748/commits/ca5eee3439c47051a6603ae1393d7c2034af21c9

I am struggling to resolve some of the sorrys. Specifically,

• How to convert HasSum f 1 into ∑ k ∈ K, f k = 1.
• Issues with using simp and ring with ↑ coercions (between Nat and Finset.range (n + 1), between ℝ≥0, ℝ≥0∞, and ℝ, etc.).
• General feeling that I am doing things the "hard way" and am missing some slicker ways to write this proof.

I've left comments in the file to point out where I am having trouble, but would appreciate general advice about how to streamline this proof. I think my lack of familiarity with certain lean concepts is making this much harder than it should be. Thanks in advance!

To @Josha Dekker: Github suggested you as a reviewer, let me know if I should assign someone else.

[Josha Dekker]

I’m happy to take a look at some point, but I’m a bit busy right now, so can’t guarantee it will be particularly quick. Once you get the PR to pass CI, it should automatically be on the queue, which means reviewers that can merge the PR will at some point give some feedback! You can phrase individual questions that you have as a question (e.g. in the new members stream), if you reduce them to #mwe. For example, your questions about finsets or coercions can also go there!

[Josha Dekker]

(deleted)

[Josha Dekker]

I've taken another brief look. I think that it would be good to split up the proof a bit more: the crucial aspect that you want to show is about docs#expSeries (a certain sum over expSeries terms is again an expSeries term with different parameters), so it would be reasonable to prove this result first (see the proof above your result in the Poisson file to see where I used this expSeries before). Then, the actual result would simply involve unfolding poissonPMF, where summability of a poissonPMF has already been established in another result in that file.

[Josha Dekker]

(I don’t have time to review the Lean proof in detail the coming week, but I would give this recommendation anyway, so I thought it’d be efficient to give it now!)

[Ruben Van de Velde]

I looked at it, but it was really painful. I hope Josha's suggestion will help, but the coercions really do get in the way

[Josha Dekker]

I'm afraid I also can't comment on whether using Finset.range is the best choice of index for the sum, as I don't know that aspect of Mathlib sufficiently well.

[Josha Dekker]

Ruben Van de Velde said:

I looked at it, but it was really painful. I hope Josha's suggestion will help, but the coercions really do get in the way

Yes, so I hope breaking it up in very small bits hopefully limits the number of coercions one needs to deal with at the same time.

[Josha Dekker]

@blfang , I think it would make your life easier if you work with the Binomial theorem directly (add_pow, https://github.com/leanprover-community/mathlib4/blob/8666bd82efec40b8b3a5abca02dc9b24bbdf2652/Mathlib/Data/Nat/Choose/Sum.lean#L83), rather than the PMF for the binomial distribution (both to reduce imports and to simplify assumptions).

[blfang]

Thank you both! Will look into your suggestions and try to rewrite this in a cleaner way.