Mollification Convergence for Compactly Supported Continuous Functions

This establishes $L^2$ convergence of mollifications in the continuous compactly supported case.

Let $V$ be a finite-dimensional real inner-product space with an additive Haar measure $m$, let $E$ be a complete normed real vector space, and let $(\varphi_n)_{n\in\mathbb{N}}$ be smooth bumps centered at $0$. Assume their outer radii satisfy

For every continuous compactly supported function $f:V\to E$,

The convergence is in the extended $L^2$ norm, whose values lie in $[0,\infty]$. This is the basic approximation result used to extend mollification convergence from regular functions to general $L^2$ functions.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis.Mollification. Shown in its original module context. Proof omitted.

theorem tendsto_eLpNorm_convolution_sub_of_continuous {φ : ℕ → ContDiffBump (0 : V)}
    (hφ : Tendsto (fun n => (φ n).rOut) atTop (𝓝 0)) {f : V → E} (hf : Continuous f)
    (hfc : HasCompactSupport f) :
    Tendsto (fun n => eLpNorm ((φ n).normed m ⋆[ContinuousLinearMap.lsmul ℝ ℝ, m] f - f) 2 m)
      atTop (𝓝 0)

Module navigation

Module: Analysis/Mollification/Basic.

Previous: lintegral_enorm_convolution_sq_le · Next: tendsto_eLpNorm_convolution_sub.

Source excerpt, lines 188–192 · Frozen source 408915f.