Compactly supported functions are dense in Schwartz space

This file shows that the compactly supported Schwartz functions are dense in 𝓢(E, F), by multiplying a Schwartz function by a rescaled smooth cutoff.

Main statements

• SchwartzMap.tendsto_smulLeftCLM_comp_smul: if φ is smooth, compactly supported, and equal to 1 near the origin, then (fun x ↦ φ (ε • x)) • f → f in the Schwartz topology as ε → 0.
• SchwartzMap.dense_hasCompactSupport: compactly supported Schwartz functions are dense.

theorem SchwartzMap.tendsto_seminorm_smulLeftCLM_comp_smul_sub {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {φ : E → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (hφ1 : φ =ᶠ[nhds 0] 1) (f : SchwartzMap E F) (k n : ℕ) : Filter.Tendsto (fun (ε : ℝ) => (SchwartzMap.seminorm ℝ k n) ((smulLeftCLM F fun (x : E) => φ (ε • x)) f - f)) (nhds 0) (nhds 0)

Multiplying a Schwartz function f by the rescaled cutoff fun x ↦ φ (ε • x) converges to f in each Schwartz seminorm as ε → 0, when φ is smooth, compactly supported, and equal to 1 near the origin.

theorem SchwartzMap.tendsto_smulLeftCLM_comp_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {φ : E → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (hφ1 : φ =ᶠ[nhds 0] 1) (f : SchwartzMap E F) : Filter.Tendsto (fun (ε : ℝ) => (smulLeftCLM F fun (x : E) => φ (ε • x)) f) (nhds 0) (nhds f)

As ε → 0, multiplying f by the rescaled cutoff fun x ↦ φ (ε • x) converges to f in the Schwartz topology, for any smooth, compactly supported φ equal to 1 near the origin.

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

Compactly supported Schwartz functions are dense in 𝓢(E, F).