Mollification by a normalized smooth kernel

MathlibAnnex.Mollification.mollify

def

Defines convolution with a nonnegative smooth kernel of integral one.

Statement

Let and , with their coordinate sup norms and Lebesgue measure on . For a real parameter and a map , define , where is the normalized bump described below.

Definition

For , take the specified smooth bump centered at , with inner radius and outer radius . For , the definition instead uses radii and . Set The denominator is positive. This normalization followed by convolution is the complete definition. The fallback defines the operation at every real parameter; approximation uses only .

Assumptions

The definition accepts every , every real , and every function . It does not assume continuity, measurability, or integrability. Analytic properties of the convolution require their own hypotheses.

Conclusion

The output is the function . For locally integrable this is the ordinary convolution with the compactly supported continuous kernel. For arbitrary the displayed integral is understood with the source library’s total Bochner-integral convention (zero when Bochner integrability fails).

For , the same normalized bump satisfies In particular its topological support, , is contained in . The definition fixes these bumps; no formula identifying them as dilates of a single kernel is asserted. Smoothness of and convergence are separate results.

noncomputable def mollify {n N : ℕ} (ε : ℝ)
    (f : (Fin n → ℝ) → (Fin N → ℝ)) : (Fin n → ℝ) → (Fin N → ℝ) :=
  standardMollifier ε ⋆[ContinuousLinearMap.lsmul ℝ ℝ, volume] f

noncomputable section
open Set MeasureTheory Filter
open scoped Convolution Topology ENNReal NNReal Pointwise
namespace MathlibAnnex
namespace Mollification

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project