Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-07 09:01 50092e4a

View on Github →

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).

Estimated changes