[Merged by Bors] - feat(analysis/convolution): integral of a convolution over positive reals

[loefflerd]

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

---

[sgouezel]

For usability, can you also record a lemma saying that, under your assumptions, x -> (∫ t:ℝ in 0..x, L (f t) (g (x - t)) ∂ν) is integrable on Ioi 0 (or even on the whole space, for what it's worth)? Maybe this will require splitting off a few lemmas from your proof to avoid too much code duplication, I'm not sure.

[loefflerd]

For usability, can you also record a lemma saying that, under your assumptions, x -> (∫ t:ℝ in 0..x, L (f t) (g (x - t)) ∂ν) is integrable on Ioi 0 (or even on the whole space, for what it's worth)? Maybe this will require splitting off a few lemmas from your proof to avoid too much code duplication, I'm not sure.

Do you have a suggestion what to call this function? Maybe "convolution_forward" or "convolution
_pos"?

[sgouezel]

Rather pos_convolution: otherwise, one may confuse it with the statement that some convolution is positive. (This will be solved by Lean 4 naming convention, but we're not there yet).

[loefflerd]

Rather pos_convolution

OK, here it is then

[sgouezel]

bors r+
Thanks!

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests