mathlib

0d77f29f - feat(analysis/calculus/specific_functions): define normed bump functions (#13463)

feat(analysis/calculus/specific_functions): define normed bump functions (#13463) * Normed bump functions have integral 1 w.r.t. the specified measure. * Also add a few more properties of bump functions, including its smoothness in all arguments (including midpoint and the two radii). * From the sphere eversion project * Required for convolutions