mathlib

50092e4a - feat(analysis/convolution): integral of a convolution over positive reals (#18353)

feat(analysis/convolution): integral of a convolution over positive reals (#18353) This PR generalises `integral_convolution` to consider convolutions of functions on the positive real line. (This will be used in a follow-up PR to relate the gamma and beta functions).