Coarse-graining support: Support.Sobolev.W1p.GlobalMollifierLp #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Global L^p convergence of the scaled mollifier #
This file proves the global approximate-identity statement for the convex kernel family. It is deliberately independent of the affine inward mollification and of bounded-domain Sobolev theory.
theorem
HCPolySupport.tendsto_eLpNorm_sub_zero_convolution_scaledConvexApproxKernel
{d : ℕ}
{ρ g : Vec d → ℝ}
{p : ENNReal}
(hρ : IsConvexApproxKernel ρ)
(hp1 : 1 ≤ p)
(hp : p ≠ ⊤)
(hg : MeasureTheory.MemLp g p MeasureTheory.volume)
{r : ℝ}
(hr : 0 < r)
{ε : ℕ → ℝ}
(hε : Filter.Tendsto ε Filter.atTop (nhds 0))
(hε_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < ε n)
:
Filter.Tendsto
(fun (n : ℕ) =>
MeasureTheory.eLpNorm
(fun (x : Vec d) =>
MeasureTheory.convolution (scaledConvexApproxKernel ρ (ε n * r)) g (ContinuousLinearMap.lsmul ℝ ℝ)
MeasureTheory.volume x - g x)
p MeasureTheory.volume)
Filter.atTop (nhds 0)
Convolution by the scaled convex kernel is a global approximate identity
in every finite L^p, 1 ≤ p < ∞.