Local finite order of distributions

A distribution has finite order on each compact set: for a compact K ⊆ Ω its value on a test function supported in K is bounded by a constant times a bound on the derivatives of the test function up to some fixed order N.

Main declarations

• Distribution.exists_norm_apply_le: a distribution has finite order on each compact set.
• Distribution.isLittleO_apply_of_norm_iteratedFDeriv_le: a map with such a finite-order bound sends a family of test functions whose derivatives up to that order are o(‖h‖) to an o(‖h‖) family.

References

• [L. Hörmander, The Analysis of Linear Partial Differential Operators I][hormander2003], §2.1.

theorem Distribution.exists_norm_apply_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} (T : Distribution Ω F ⊤) {K : TopologicalSpace.Compacts E} (hK : ↑K ⊆ ↑Ω) : ∃ (N : ℕ) (C : ℝ), 0 ≤ C ∧ ∀ (φ : TestFunction Ω ℝ ⊤), tsupport ⇑φ ⊆ ↑K → ∀ (M : ℝ), 0 ≤ M → (∀ i ≤ N, ∀ (x : E), ‖iteratedFDeriv ℝ i (⇑φ) x‖ ≤ M) → ‖T φ‖ ≤ C * M

A distribution has finite order on each compact set. For a compact K ⊆ Ω there are an order N and a constant C such that ‖T φ‖ ≤ C * M for every test function φ supported in K whose derivatives of order at most N are all bounded by M.

theorem Distribution.isLittleO_apply_of_norm_iteratedFDeriv_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {X : Type u_3} {F' : Type u_4} {G : Type u_5} [NormedAddCommGroup X] [NormedAddCommGroup F'] [NormedSpace ℝ F'] [NormedAddCommGroup G] {K : Set E} {N : ℕ} {C : ℝ} {P : TestFunction Ω F' ⊤ → G} (hC : 0 ≤ C) (hP : ∀ (φ : TestFunction Ω F' ⊤), tsupport ⇑φ ⊆ K → ∀ (M : ℝ), 0 ≤ M → (∀ i ≤ N, ∀ (x : E), ‖iteratedFDeriv ℝ i (⇑φ) x‖ ≤ M) → ‖P φ‖ ≤ C * M) {R : X → TestFunction Ω F' ⊤} (hRK : ∀ᶠ (h : X) in nhds 0, tsupport ⇑(R h) ⊆ K) (hR : ∀ i ≤ N, ∀ ε > 0, ∀ᶠ (h : X) in nhds 0, ∀ (x : E), ‖iteratedFDeriv ℝ i (⇑(R h)) x‖ ≤ ε * ‖h‖) : (fun (h : X) => P (R h)) =o[nhds 0] fun (h : X) => h

Finite order turns o(‖h‖) derivative bounds into o(‖h‖) values. Let P satisfy a finite-order bound of order N on K, as in Distribution.exists_norm_apply_le. If near 0 the test functions R h are supported in K and their derivatives of order at most N are eventually bounded by ε * ‖h‖ for every ε > 0, then P (R h) = o(‖h‖). This is the step that differentiates a pairing of a distribution with a smooth family of test functions.