mathlib3

b018406a - feat(analysis/calculus/special_functions): refactor bump functions (#17453)

feat(analysis/calculus/special_functions): refactor bump functions (#17453) Currently, we have satisfactory bump functions on inner spaces (equal to 1 on `ball c r` and support equal to `ball c R`), and less satisfactory bump functions on general finite-dimensional normed spaces (equal to 1 on a neighborhood of `c`, with support a larger neighborhood of `c`), where the latter are obtained from the former by composing with an arbitrary linear equiv with an inner product space called `to_euclidean`. In particular, they have different names (`bump_function_of_inner` and `bump_function`) and whenever one wants to prove properties of `bump_function` one has to juggle with the `to_euclidean`. We refactor bump functions to get a coherent theory, which is uniform over all normed spaces. We remove completely `bump_function_of_inner`, and we make sure that `bump_function c r R` is a smooth function equal to `1` on `ball c r` and with support exactly `ball c R`, on all normed spaces. For this, we provide a typeclass `has_cont_diff_bump` saying that a space has nice bump functions, and we instantiate it both on inner product spaces (using the old approach with a function constructed from the norm and from `exp(-1/x^2)`), and on finite-dimensional normed spaces (where the bump functions have already been constructed by convolution in #18095).