Convergence of test functions with a common compact support

Mathlib's LF topology on the test functions 𝓓^{n}(Ω, F) is the finest locally convex topology making every inclusion 𝓓^{n}_{K}(E, F) → 𝓓^{n}(Ω, F) of the tests supported in a compact K ⊆ Ω continuous, and the topology of 𝓓^{n}_{K}(E, F) is that of uniform convergence of all derivatives of order at most n. Consequently a family of test functions supported in one fixed compact subset of Ω converges as soon as each of its derivatives of order at most n converges uniformly. This is the usual way to prove convergence in 𝓓^{n}(Ω, F) concretely, for instance for approximations by mollification or by truncated Fourier series.

Main declarations

• TestFunction.tendsto_of_tendstoUniformly_iteratedFDeriv: test functions supported in a common compact subset of Ω whose derivatives of order at most n converge uniformly converge in 𝓓^{n}(Ω, F).

References

• L. Hörmander, The Analysis of Linear Partial Differential Operators I, §2.1 (the topology of test functions).

theorem TestFunction.tendsto_of_tendstoUniformly_iteratedFDeriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {ι : Type u_3} {l : Filter ι} {φ : ι → TestFunction Ω F n} {ψ : TestFunction Ω F n} {K : Set E} (hK : IsCompact K) (hKΩ : K ⊆ ↑Ω) (hφK : ∀ (i : ι), tsupport ⇑(φ i) ⊆ K) (h : ∀ (k : ℕ), ↑k ≤ n → TendstoUniformly (fun (i : ι) => iteratedFDeriv ℝ k ⇑(φ i)) (iteratedFDeriv ℝ k ⇑ψ) l) : Filter.Tendsto φ l (nhds ψ)

Convergence of test functions with a common compact support. If the test functions φ i on Ω are all supported in a fixed compact subset K of Ω, and for every order k ≤ n the k-th derivatives of the φ i converge uniformly to that of ψ, then φ i → ψ in the LF topology of 𝓓^{n}(Ω, F).