Commit 2023-02-01 20:47 b3607518
View on Github →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.