Coarse-graining support: Support.Sobolev.W1p.InwardMollificationLp

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Global L^p convergence of inward mollification

This file combines the global approximate-identity theorem with strong continuity under the outward affine expansion. The result is independent of domain geometry and boundary conditions.

theorem HCPolySupport.tendsto_eLpNorm_inwardMollification_sub_zero {d : ℕ} {ρ g : Vec d → ℝ} {p : ENNReal} (hρ : IsConvexApproxKernel ρ) (hp1 : 1 ≤ p) (hp : p ≠ ⊤) (hg : MeasureTheory.MemLp g p MeasureTheory.volume) (x0 : Vec d) {r : ℝ} (hr : 0 < r) {ε : ℕ → ℝ} (hε : Filter.Tendsto ε Filter.atTop (nhds 0)) (hε_nonneg : ∀ (n : ℕ), 0 ≤ ε n) (hε_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < ε n) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (inwardMollification ρ g x0 r (ε n) - g) p MeasureTheory.volume) Filter.atTop (nhds 0)

Inward mollification converges strongly to its input in every finite L^p, 1 ≤ p < ∞, on the whole Euclidean space.

theorem HCPolySupport.tendsto_eLpNorm_one_add_mul_inwardMollification_sub_zero {d : ℕ} {ρ g : Vec d → ℝ} {p : ENNReal} (hρ : IsConvexApproxKernel ρ) (hp1 : 1 ≤ p) (hp : p ≠ ⊤) (hg : MeasureTheory.MemLp g p MeasureTheory.volume) (x0 : Vec d) {r : ℝ} (hr : 0 < r) {ε : ℕ → ℝ} (hε : Filter.Tendsto ε Filter.atTop (nhds 0)) (hε_nonneg : ∀ (n : ℕ), 0 ≤ ε n) (hε_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < ε n) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => (1 + ε n) * inwardMollification ρ g x0 r (ε n) x - g x) p MeasureTheory.volume) Filter.atTop (nhds 0)

The scalar factor produced by differentiating the affine pullback does not alter strong finite-L^p convergence of inward mollification.