Mollification Convergence for $L^2$ Functions

This establishes $L^2$ convergence of mollifications for arbitrary $L^2$ functions.

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

If $f:V\to E$ satisfies MemLp f 2 m, then

This is an $L^2$-approximation theorem for mollification and uses the extended norm convention of eLpNorm.

Original Lean declaration header

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

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

Module navigation

Module: Analysis/Mollification/Basic.

Supporting theorems: lintegral_enorm_convolution_sq_le, tendsto_eLpNorm_convolution_sub_of_continuous.

Previous: tendsto_eLpNorm_convolution_sub_of_continuous · Next: integral_inner_convolution_eq.

Source excerpt, lines 238–241 · Frozen source 408915f.