Global and local Lᵖ approximation by mollification

The three results below separate translation continuity, the normalized-kernel estimate, and the compact-localization step used for interior convergence.

theorem CKN.tendsto_eLpNorm_sub_zero_mollify {p : ENNReal} (hp : 1 ≤ p) (hp_top : p ≠ ⊤) {g : Vec 3 → ℝ} (hg : MeasureTheory.MemLp g p MeasureTheory.volume) {ε : ℕ → ℝ} (hε : Filter.Tendsto ε Filter.atTop (nhds 0)) (hε_pos : ∀ (n : ℕ), 0 < ε n) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec 3) => mollify g (ε n) ⋯ x - g x) p MeasureTheory.volume) Filter.atTop (nhds 0)

theorem CKN.mollify_eq_on_compact_of_eq_on_thickening {d : ℕ} {K : Set (Vec d)} {u g : Vec d → ℝ} {ε₀ ε : ℝ} (hε : 0 < ε) (hεlt : ε ≤ ε₀) (h_eq : ∀ y ∈ K + Metric.closedBall 0 ε₀, u y = g y) {x : Vec d} (hx : x ∈ K) : mollify u ε hε x = mollify g ε hε x

theorem CKN.tendsto_eLpNorm_restrict_mollify_sub_zero {U K : Set (Vec 3)} (hK : IsCompact K) {ε₀ : ℝ} (hε₀ : 0 < ε₀) (hKε₀ : ∀ x ∈ K, Metric.closedBall x ε₀ ⊆ U) {p : ENNReal} (hp : 1 ≤ p) (hp_top : p ≠ ⊤) {u : Vec 3 → ℝ} (hu : MeasureTheory.MemLp u p (MeasureTheory.volume.restrict U)) {ε : ℕ → ℝ} (hε : Filter.Tendsto ε Filter.atTop (nhds 0)) (hε_pos : ∀ (n : ℕ), 0 < ε n) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec 3) => mollify ((K + Metric.closedBall 0 ε₀).indicator u) (ε n) ⋯ x - u x) p (MeasureTheory.volume.restrict K)) Filter.atTop (nhds 0)