Documentation

Mathlib.Analysis.Calculus.BumpFunction.InnerProduct

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.

Equations
Instances For
    @[instance 100]

    Any inner product space has smooth bump functions.

    Equations
    • =