mathlib

41ca6015 - feat(analysis/convolution): The convolution of two functions (#13540)

feat(analysis/convolution): The convolution of two functions (#13540) * Define the convolution of two functions. * Prove that when one of the functions has compact support and is `C^n` and the other function is locally integrable, the convolution is `C^n`. * Compute the total derivative of the convolution (when one of the functions has compact support). * Prove that when taking the convolution with functions that "tend to the Dirac delta function", the convolution tends to the original function. * From the sphere eversion project.