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

source
noncomputable def ContDiffBumpBase.ofInnerProductSpace (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] :
ContDiffBumpBase E

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
  • One or more equations did not get rendered due to their size.
Instances For
    source
    instance hasContDiffBump_of_innerProductSpace (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] :
    HasContDiffBump E

    Any inner product space has smooth bump functions.

    Equations