Commit 2023-02-08 10:26 b018406a

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).