theorem SchwartzMap.compactlySupportedDense {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] : Dense {φ : SchwartzMap E ℂ | HasCompactSupport ⇑φ}

The compactly-supported Schwartz functions form a dense subset of the Schwartz space 𝓢(E, ℂ). The proof multiplies a Schwartz function f by a sequence of bump cutoffs and uses that the Schwartz seminorms of bumpCutoffMul m f - f tend to zero as m → ∞.

theorem TemperedDistribution.compactly_supported_dense_in_schwartz {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [FiniteDimensional ℝ E] (u : TemperedDistribution E F) (ψ : SchwartzMap E ℂ) (h : ∀ (φ : SchwartzMap E ℂ), HasCompactSupport ⇑φ → u φ = 0) : u ψ = 0

If a tempered distribution u vanishes on every compactly-supported Schwartz function, then it vanishes on every Schwartz function. This is the density argument bridging local information about u to its global behaviour.

theorem TemperedDistribution.eq_zero_of_dsupport_eq_empty {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [FiniteDimensional ℝ E] (u : TemperedDistribution E F) (hu : Distribution.dsupport ⇑u = ∅) : u = 0

Proposition 8.9 of Melrose: a tempered distribution u with empty distributional support is the zero distribution. The proof covers E by open sets on which u vanishes, applies a Schwartz partition of unity to deduce that u vanishes on every compactly-supported Schwartz function, and then extends this to all Schwartz functions by density.