mathlib3

9d81ef7e - feat(analysis/convolution): regularity of convolution for functions depending on a parameter (#17626)

feat(analysis/convolution): regularity of convolution for functions depending on a parameter (#17626) Show that the convolution of `f` and `g` is smooth when `g` is. A version of this statement is already in mathlib, but in this PR we prove the version where `g` depends on a parameter. Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>