Commit 2022-05-27 19:20 41ca6015

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.