Normed bump function #

In this file we define ContDiffBump.normed f μ to be the bump function f normalized so that ∫ x, f.normed μ x ∂μ = 1 and prove some properties of this function.

A bump function normed so that ∫ x, f.normed μ x ∂μ = 1.

Instances For
    theorem ContDiffBump.normed_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [HasContDiffBump E] [MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E} (x : E) :
    ContDiffBump.normed f μ x = f x / ∫ (x : E), f xμ