Compactly supported approximation of smooth Sobolev functions

A smooth function whose classical derivatives through order k belong to Lᵖ can be approximated by smooth compactly supported functions, simultaneously in the Lᵖ seminorm of every derivative through order k, for 0 < p < ∞. The domain is a finite-dimensional real normed space, the codomain is a real normed space, and the measure is arbitrary.

The approximations are χ ((n + 1)⁻¹ • x) • f x, with a fixed smooth compactly supported cutoff χ equal to one near zero. The Leibniz estimate gives an integrable envelope consisting of a finite sum of norms of derivatives of f. At each point the approximation eventually agrees with f on a neighborhood, so all its derivatives eventually agree there as well. This is the cutoff step used after smoothing in whole-space Sobolev density arguments. The statements here concern classical derivatives; no identification with a bundled weak Sobolev space is asserted.

References

L. C. Evans, Partial Differential Equations, §5.3.1. The derivative estimate uses Mathlib's norm_iteratedFDeriv_smul_le and iteratedFDeriv_comp_const_smul.

The expanding-cutoff construction and the compactly supported bump's derivative bounds are adapted from SchwartzMap.dense_hasCompactSupport and SchwartzMap.tendsto_smulLeftCLM_comp_inv_smul_atTop in TauCeti/Analysis/Distribution/SchwartzSpace/Cutoff.lean. Their positive-order derivative scaling estimate is shared via TauCeti.norm_iteratedFDeriv_comp_inv_smul_sub_const_le.

theorem TauCeti.tendsto_eLpNorm_iteratedFDeriv_cutoff_sub {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopology E] {μ : MeasureTheory.Measure E} {p : ENNReal} (hp0 : p ≠ 0) (hp : p ≠ ⊤) {χ : E → ℝ} {f : E → F} {k : ℕ} (hχ : ContDiff ℝ (↑k) χ) (hχ1 : χ =ᶠ[nhds 0] 1) {B : ℕ → ℝ} (hB : ∀ i ≤ k, ∀ (x : E), ‖iteratedFDeriv ℝ i χ x‖ ≤ B i) (hf : ContDiff ℝ (↑k) f) (hmem : ∀ i ≤ k, MeasureTheory.MemLp (iteratedFDeriv ℝ i f) p μ) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm ((iteratedFDeriv ℝ k fun (x : E) => χ ((↑n + 1)⁻¹ • x) • f x) - iteratedFDeriv ℝ k f) p μ) Filter.atTop (nhds 0)

Expanding cutoffs approximate the k-th classical derivative of a Cᵏ function in Lᵖ. Only the derivatives up to the requested order need to be integrable; the measure need not be translation invariant.

theorem TauCeti.memLp_iteratedFDeriv_smul_of_bounded {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopology E] {μ : MeasureTheory.Measure E} {p : ENNReal} {χ : E → ℝ} {f : E → F} {k : ℕ} (hχ : ContDiff ℝ (↑k) χ) {B : ℕ → ℝ} (hB : ∀ i ≤ k, ∀ (x : E), ‖iteratedFDeriv ℝ i χ x‖ ≤ B i) (hf : ContDiff ℝ (↑k) f) (hmem : ∀ i ≤ k, MeasureTheory.MemLp (iteratedFDeriv ℝ i f) p μ) : MeasureTheory.MemLp (iteratedFDeriv ℝ k fun (x : E) => χ x • f x) p μ

Multiplication by a Cᵏ scalar function with bounded derivatives preserves Lᵖ integrability of the k-th classical derivative, provided every derivative of the second factor through order k belongs to Lᵖ.

theorem TauCeti.exists_contDiff_hasCompactSupport_approximation {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E} {p : ENNReal} (hp0 : p ≠ 0) (hp : p ≠ ⊤) {f : E → F} (hf : ContDiff ℝ (↑⊤) f) (k : ℕ) (hmem : ∀ i ≤ k, MeasureTheory.MemLp (iteratedFDeriv ℝ i f) p μ) : ∃ (g : ℕ → E → F), (∀ (n : ℕ), ContDiff ℝ (↑⊤) (g n) ∧ HasCompactSupport (g n)) ∧ (∀ (n i : ℕ), i ≤ k → MeasureTheory.MemLp (iteratedFDeriv ℝ i (g n)) p μ) ∧ ∀ i ≤ k, Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (iteratedFDeriv ℝ i (g n) - iteratedFDeriv ℝ i f) p μ) Filter.atTop (nhds 0)

A smooth function with Lᵖ classical derivatives through order k admits smooth compactly supported approximations converging in the Lᵖ seminorm of every such derivative. The same approximation sequence works for all orders through k.