Adding mgf's, cgf's, charFun's to distributions

Stream: mathlib4

[Anirudh Rao]

Hi! I was interested in trying to add moment-generating functions, cumulant-generating functions, and characteristic functions of distributions to Mathlib. It could also be used to add expected value and variance for distributions too (though idk if having those proofs rely on mgf is necessarily good for perf?). I've done a little bit of work already formalizing those for the binomial distribution. I wanted to check in to see if this is useful for Mathlib (pretty sure but just in case) and to ask about any broader context of developing Probability/MeasureTheory along with any Mathlib-specific guidelines that I should know about. Thanks!

[David Ledvinka]

Yes this would definitely be desirable.