Put convolution in a namespace?

Stream: mathlib4

[Michael Stoll]

Right now, docs#convolution lives in the root namespace, but it is a rather specialized concept from Measure Theory. As there are a number of other "convolutions" around in math, I would strongly suggest to move it (and the related declarations) to a namespace, e.g., MeasureTheory.

[Michael Stoll]

:ping_pong: anyone? In #11634 I have to disambiguate, because there are convolution and convolution_def in the root namespace...

[Kevin Buzzard]

I agree that if the concepts have the same name (as indeed they do) they should both be namespaced.

[Michael Stoll]

Can someone fluent in the measure theory part of Mathlib look at this? I wouldn't want to try to move things around there...

[Floris van Doorn]

Yes, moving everything about convolution to the MeasureTheory namespace sounds good to me. My apologies for putting it in the root namespace in the first place. I don't know if I have time soon to do this myself...

[Michael Stoll]

I have to prepare my talk today (see here), but maybe I can do it in the evening (CET).

[Floris van Doorn]

Done in #12376

[Michael Stoll]

Thanks! It seems I got distracted...