mathlib3

a07493af - feat(analysis/convolution): the predicate `convolution_exists` (#13541)

feat(analysis/convolution): the predicate `convolution_exists` (#13541) * This PR defines the predicate that a convolution exists. * This is not that interesting by itself, but it is a preparation for #13540 * I'm using the full module doc for the convolution file, even though not everything promised in the module doc is in this PR. * From the sphere eversion project