Commit 2025-04-23 07:25 0e302d35

feat(Analysis): add mlconvolution and lconvolution, Convolution with the Lebesgue integral (#23299) Create LConvolution.lean which defines convolution using the Lebesgue integral. I plan to add more API but wanted to make sure the definition/notation are satisfactory. The main intended application of this is to prove that the pdf of a product (sum) of independent random variables is given by the convolution of their pdfs.