Morera's Theorem

Stream: mathlib4

[Alex Meiburg]

It's a nice fact that the Laplace transform is analytic anywhere its region of convergence (as an integral, its domain of absolute convergence is always exactly some half-plane). The proof is pretty straightforward given https://en.wikipedia.org/wiki/Morera%27s_theorem - Wikipedia gives an example for proving the analyticity of e.g. the Gamma function but the same Fubini trick works there too. I would quite like to use this fact, but I'm not familiar with much of the API around complex analysis and don't know how far it is from this.