Smooth bump functions in inner product spaces #
In this file we prove that a real inner product space has smooth bump functions,
smooth function, bump function, inner product space
A base bump function in an inner product space. This construction works in any space with a norm smooth away from zero but we do not have a typeclass for this.