mathlib

b3607518 - feat(analysis/calculus/bump_function_findim): construct good bump functions on finite-dimensional spaces (#18095)

feat(analysis/calculus/bump_function_findim): construct good bump functions on finite-dimensional spaces (#18095) On any finite-dimensional real vector space, we construct a smooth family of smooth functions indexed by `R > 1` which are equal to `1` on the ball `B 0 1`, and with support exactly `B 0 R`. This is the main ingredient to construct nice bump functions.