Poisson Distribution

Stream: new members

[Gareth Ma]

Hi! I have just defined the Poisson distribution, or at least it's pdf. However, I feel like the proof can surely be shortened - it is currently 24 lines long, but the crucial part of the proof i.e. power series of exponential function is already there, just that the type casting is hell. Can someone help take a look at it? I think I will prove a few more results and translate more of my first year statistics module into Lean :)

[Gareth Ma]

Link: https://github.com/grhkm21/lean/blob/0f8333970e9cdfc3c98f8c928998a8e400ac7792/sketch/pmf.lean#L28