mathlib3

845654a1 - feat(analysis/calculus): define a smooth bump function (#4458)

feat(analysis/calculus): define a smooth bump function (#4458) Define an infinitely smooth function which is `1` on the closed ball of radius `1` and is `0` outside of the open ball of radius `2`.