Laplace transform

Stream: maths

[Jason KY.]

I would like to define moment generating functions and I think a natural way to do so is through Laplace transforms. Is anyone working on this?

I have played around with a few definitions but I'm not sure whether my definition is the correct generality for mathlib. Would an expert mind taking a look at it here: https://github.com/JasonKYi/probability_theory/blob/main/src/laplace.lean#L17