Smooth bump functions in inner product spaces #

In this file we prove that a real inner product space has smooth bump functions, see hasContDiffBump_of_innerProductSpace.

Keywords #

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.

Instances For

    Any inner product space has smooth bump functions.