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.