Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-28 04:58 c7a2d670

View on Github →

refactor(analysis/calculus/specific_functions): add params to smooth_bump_function (#6467) In the construction of a partition of unity we need a smooth bump function that vanishes outside of ball x R and equals one on closed_ball x r with arbitrary 0 < r < R.

Estimated changes