Cutting off a Schwartz function

Let χ : E → ℝ be a smooth compactly supported function that equals 1 near the origin. For a Schwartz function f, the truncations x ↦ χ (R⁻¹ • x) • f x are smooth and compactly supported, and they converge to f in the Schwartz topology as R → ∞. Consequently the smooth compactly supported functions are dense in 𝓢(E, F) when E is finite-dimensional.

This is how a statement proved for smooth compactly supported test functions is passed to Schwartz test functions: any quantity controlled by finitely many Schwartz seminorms (for instance a weighted sup norm of the Fourier transform) is approximated by its values on the truncations.

The estimate is explicit. Suppose χ = 1 on the ball of radius r and R ≥ 1. The difference f - χ (R⁻¹ • ·) • f is (1 - χ (R⁻¹ • ·)) • f, which vanishes on the ball of radius r R. Expand its n-th derivative by the Leibniz rule. The term in which no derivative falls on the cutoff is supported where ‖x‖ ≥ r R, so trading one power of ‖x‖ against (r R)⁻¹ bounds it by the (k + 1, n) seminorm of f divided by r R. Every other term carries a derivative of χ (R⁻¹ • ·) of order i ≥ 1, which is R⁻ⁱ times a derivative of χ and hence O(R⁻¹). Altogether the (k, n) seminorm of the difference is O(R⁻¹).

Main results

• SchwartzMap.seminorm_sub_smulLeftCLM_comp_inv_smul_le: the explicit bound seminorm k n (f - χ (R⁻¹ • ·) • f) ≤ K / R for R ≥ 1.
• SchwartzMap.tendsto_smulLeftCLM_comp_inv_smul_atTop: the truncations converge to f in 𝓢(E, F).
• SchwartzMap.hasCompactSupport_smulLeftCLM_comp_inv_smul: the truncations are compactly supported.
• SchwartzMap.dense_hasCompactSupport: compactly supported functions are dense in 𝓢(E, F) for finite-dimensional E.

References

• L. Hörmander, The Analysis of Linear Partial Differential Operators I, Section 7.1.

@[simp]

theorem SchwartzMap.smulLeftCLM_comp_inv_smul_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {χ : E → ℝ} (hχ : Function.HasTemperateGrowth χ) (R : ℝ) (f : SchwartzMap E F) (x : E) : ((smulLeftCLM F fun (y : E) => χ (R⁻¹ • y)) f) x = χ (R⁻¹ • x) • f x

The truncation χ (R⁻¹ • ·) • f of a Schwartz function by a cutoff of temperate growth, evaluated pointwise.

theorem SchwartzMap.hasCompactSupport_smulLeftCLM_comp_inv_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {χ : E → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hsupp : HasCompactSupport χ) {R : ℝ} (hR : R ≠ 0) (f : SchwartzMap E F) : HasCompactSupport ⇑((smulLeftCLM F fun (y : E) => χ (R⁻¹ • y)) f)

A truncation of a Schwartz function by a compactly supported cutoff is compactly supported.

theorem SchwartzMap.seminorm_sub_smulLeftCLM_comp_inv_smul_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {χ : E → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) {B : ℕ → ℝ} (hB : ∀ (i : ℕ) (x : E), ‖iteratedFDeriv ℝ i χ x‖ ≤ B i) {r : ℝ} (hr : 0 < r) (hχ1 : ∀ (y : E), ‖y‖ < r → χ y = 1) (f : SchwartzMap E F) (k n : ℕ) {R : ℝ} (hR : 1 ≤ R) : (SchwartzMap.seminorm ℝ k n) (f - (smulLeftCLM F fun (y : E) => χ (R⁻¹ • y)) f) ≤ (∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * (1 + B i) * ((SchwartzMap.seminorm ℝ k (n - i)) f + (SchwartzMap.seminorm ℝ (k + 1) (n - i)) f / r)) / R

The truncation estimate. Let χ be smooth with ‖D^i χ‖ ≤ B i for every i, and equal to 1 on the ball of radius r > 0. For R ≥ 1 the (k, n) seminorm of f - χ (R⁻¹ • ·) • f is at most K / R, where K depends on χ, f, k and n but not on R.

theorem SchwartzMap.tendsto_smulLeftCLM_comp_inv_smul_atTop {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {χ : E → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hbdd : ∀ (i : ℕ), ∃ (B : ℝ), ∀ (x : E), ‖iteratedFDeriv ℝ i χ x‖ ≤ B) (hχ1 : χ =ᶠ[nhds 0] 1) (f : SchwartzMap E F) : Filter.Tendsto (fun (R : ℝ) => (smulLeftCLM F fun (y : E) => χ (R⁻¹ • y)) f) Filter.atTop (nhds f)

Truncations converge in the Schwartz topology. If χ is smooth with every derivative bounded (for instance, if χ is compactly supported) and equal to 1 near the origin, then χ (R⁻¹ • ·) • f → f in 𝓢(E, F) as R → ∞.

theorem SchwartzMap.dense_hasCompactSupport {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] : Dense {f : SchwartzMap E F | HasCompactSupport ⇑f}

Compactly supported functions are dense in Schwartz space.