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

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

• ContDiffBumpBase.ofInnerProductSpace E = { toFun := fun (R : ℝ) (x : E) => Real.smoothTransition ((R - ‖x‖) / (R - 1)), mem_Icc := ⋯, symmetric := ⋯, smooth := ⋯, eq_one := ⋯, support := ⋯ }

instance hasContDiffBump_of_innerProductSpace (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] : HasContDiffBump E

Any inner product space has smooth bump functions.

Equations

• ⋯ = ⋯