Localization of distributions and the augmentation

Let Ω be an open subset of a finite-dimensional real normed space E. Mathlib's dsupport T of a map T on test functions is the complement of the union of the open sets on which T vanishes. For an additive map on test functions, such as a distribution or a current, the localization principle says that T vanishes on that union, so on the complement of its support. Consequently T φ depends only on the germ of φ along dsupport T, T vanishes exactly when its support is empty, and the support of a sum lies in the union of the supports.

When dsupport T is a compact subset of Ω, a test χ equal to one near dsupport T exists, and T (χ • c) is independent of that cutoff for every vector c. This value is the augmentation augmentation T c: the pairing of a compactly supported distribution with the constant function c. For degree-zero currents and c the unit 0-form it is the augmentation of the current, the total coefficient of a finite sum of point masses. No constant test function is inserted into the domain of T: when the support of T is not a compact subset of Ω, no such cutoff exists and augmentation T c is the junk value zero. The augmentation of an additive map is additive in c, and that of a linear map is homogeneous in c. The augmentation is homogeneous in the map, and on maps whose supports are compact subsets of Ω it is also additive in the map. It sends the point evaluation φ ↦ ℓ (φ x) to ℓ c, and it vanishes on the boundary T ∘ d of a current, because the exterior derivative of a cutoff equal to one vanishes near the support.

Main declarations

• Distribution.isVanishingOn_compl_dsupport: an additive map on test functions vanishes on the complement of its support; Distribution.isVanishingOn_iff_disjoint_dsupport is the resulting characterization of the open sets on which it vanishes.
• Distribution.map_eq_map_of_eventuallyEq: tests that agree near the support have equal values.
• Distribution.dsupport_eq_empty_iff: an additive map on test functions vanishes exactly when its support is empty.
• Distribution.dsupport_comp_smulLeftCLM_subset: a smooth multiple T ∘ (g ·) is supported in the supports of both g and T.
• Distribution.augmentation: the pairing T (χ • c) with a cutoff χ equal to one near the support; Distribution.augmentation_eq is its independence of the cutoff.
• Distribution.augmentation_comp_extDerivCLM: the augmentation of a boundary is zero.

References

• L. Hörmander, The Analysis of Linear Partial Differential Operators I, §2.2 (localization and support) and §2.3 (distributions with compact support).
• H. Federer, Geometric Measure Theory, §4.1.7 (support of a current).

theorem Distribution.dsupport_apply_apply_subset {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [AddZeroClass V] {x : E} (ℓ : F →+ V) : (dsupport fun (φ : TestFunction Ω F n) => ℓ (φ x)) ⊆ {x}

The support of a point evaluation followed by an additive map lies in that singleton.

theorem Distribution.isVanishingOn_iUnion {E : Type u_1} {F : Type u_2} {V : Type u_3} {𝓕 : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [FiniteDimensional ℝ E] [AddCommMonoid V] [FunLike 𝓕 (TestFunction Ω F n) V] [AddMonoidHomClass 𝓕 (TestFunction Ω F n) V] (T : 𝓕) {ι : Type u_6} {U : ι → Set E} (hU : ∀ (i : ι), IsOpen (U i)) (hT : ∀ (i : ι), IsVanishingOn (⇑T) (U i)) : IsVanishingOn (⇑T) (⋃ (i : ι), U i)

Localization principle. An additive map on test functions that vanishes on each member of a family of open sets vanishes on their union.

theorem Distribution.isVanishingOn_sUnion {E : Type u_1} {F : Type u_2} {V : Type u_3} {𝓕 : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [FiniteDimensional ℝ E] [AddCommMonoid V] [FunLike 𝓕 (TestFunction Ω F n) V] [AddMonoidHomClass 𝓕 (TestFunction Ω F n) V] (T : 𝓕) {S : Set (Set E)} (hS : ∀ s ∈ S, IsOpen s ∧ IsVanishingOn (⇑T) s) : IsVanishingOn (⇑T) (⋃₀ S)

An additive map on test functions that vanishes on each member of a set of open sets vanishes on their union.

theorem Distribution.isVanishingOn_compl_dsupport {E : Type u_1} {F : Type u_2} {V : Type u_3} {𝓕 : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [FiniteDimensional ℝ E] [AddCommMonoid V] [FunLike 𝓕 (TestFunction Ω F n) V] [AddMonoidHomClass 𝓕 (TestFunction Ω F n) V] (T : 𝓕) : IsVanishingOn (⇑T) (dsupport ⇑T)ᶜ

An additive map on test functions vanishes on the complement of its support.

theorem Distribution.isVanishingOn_iff_disjoint_dsupport {E : Type u_1} {F : Type u_2} {V : Type u_3} {𝓕 : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [FiniteDimensional ℝ E] [AddCommMonoid V] [FunLike 𝓕 (TestFunction Ω F n) V] [AddMonoidHomClass 𝓕 (TestFunction Ω F n) V] (T : 𝓕) {s : Set E} (hs : IsOpen s) : IsVanishingOn (⇑T) s ↔ Disjoint s (dsupport ⇑T)

An additive map on test functions vanishes on an open set exactly when that set is disjoint from its support.

theorem Distribution.map_eq_zero_of_disjoint_dsupport {E : Type u_1} {F : Type u_2} {V : Type u_3} {𝓕 : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [FiniteDimensional ℝ E] [AddCommMonoid V] [FunLike 𝓕 (TestFunction Ω F n) V] [AddMonoidHomClass 𝓕 (TestFunction Ω F n) V] (T : 𝓕) {φ : TestFunction Ω F n} (h : Disjoint (tsupport ⇑φ) (dsupport ⇑T)) : T φ = 0

An additive map on test functions vanishes on every test whose support is disjoint from its support.

theorem Distribution.dsupport_eq_empty_iff {E : Type u_1} {F : Type u_2} {V : Type u_3} {𝓕 : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [FiniteDimensional ℝ E] [AddCommMonoid V] [FunLike 𝓕 (TestFunction Ω F n) V] [AddMonoidHomClass 𝓕 (TestFunction Ω F n) V] (T : 𝓕) : dsupport ⇑T = ∅ ↔ ⇑T = 0

An additive map on test functions vanishes exactly when its support is empty.

theorem Distribution.dsupport_add_subset {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [AddZeroClass V] (f g : TestFunction Ω F n → V) : dsupport (f + g) ⊆ dsupport f ∪ dsupport g

The support of a sum of maps on test functions lies in the union of their supports.

theorem Distribution.map_eq_map_of_eventuallyEq {E : Type u_1} {F : Type u_2} {V : Type u_3} {𝓕 : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [FiniteDimensional ℝ E] [AddCommGroup V] [FunLike 𝓕 (TestFunction Ω F n) V] [AddMonoidHomClass 𝓕 (TestFunction Ω F n) V] (T : 𝓕) {φ ψ : TestFunction Ω F n} (h : ⇑φ =ᶠ[nhdsSet (dsupport ⇑T)] ⇑ψ) : T φ = T ψ

The value of an additive map on test functions depends only on the germ of the test along the support of the map.

theorem Distribution.dsupport_comp_smulLeftCLM_subset {E : Type u_1} {F : Type u_2} {V : Type u_3} {𝓕 : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [Zero V] [FunLike 𝓕 (TestFunction Ω F n) V] [ZeroHomClass 𝓕 (TestFunction Ω F n) V] (T : 𝓕) {g : E → ℝ} (hg : ContDiff ℝ (↑n) g) : dsupport (⇑T ∘ ⇑(TestFunction.smulLeftCLM hg)) ⊆ tsupport g ∩ dsupport ⇑T

The support of a smooth multiple T ∘ (g ·) of a map on test functions lies both in the support of g and in the support of T. In particular, multiplying by a test function g produces a compactly supported map.

noncomputable def Distribution.augmentation {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [Zero V] (f : TestFunction Ω F n → V) (c : F) : V

The augmentation of a map f on test functions at a vector c: the value f (χ • c), where χ is a test function equal to one on a neighbourhood of the support of f. For an additive map it does not depend on the choice of χ (Distribution.augmentation_eq), and such a χ exists when the support is a compact subset of Ω. It is zero when no such χ exists.

@[simp]

theorem Distribution.augmentation_of_not_exists {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [Zero V] {f : TestFunction Ω F n → V} (h : ¬∃ (χ : TestFunction Ω ℝ n), ∀ᶠ (x : E) in nhdsSet (dsupport f), χ x = 1) (c : F) : augmentation f c = 0

The augmentation is zero when no test function is equal to one on a neighbourhood of the support.

theorem Distribution.dsupport_comp_extDerivCLM_subset {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} [Zero V] {k : ℕ} (f : TestFunction Ω (E [⋀^Fin (k + 1)]→L[ℝ] F) ⊤ → V) : dsupport (f ∘ ⇑TestFunction.extDerivCLM) ⊆ dsupport f

The support of a boundary T ∘ d lies in the support of T.

@[simp]

theorem Distribution.augmentation_zero_right {E : Type u_1} {F : Type u_2} {V : Type u_3} {𝓕 : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [Zero V] [FunLike 𝓕 (TestFunction Ω F n) V] [ZeroHomClass 𝓕 (TestFunction Ω F n) V] (T : 𝓕) : augmentation (⇑T) 0 = 0

The augmentation of a map vanishing at zero is zero at the zero vector.

theorem Distribution.augmentation_add_right {E : Type u_1} {F : Type u_2} {V : Type u_3} {𝓕 : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [AddZeroClass V] [FunLike 𝓕 (TestFunction Ω F n) V] [AddMonoidHomClass 𝓕 (TestFunction Ω F n) V] (T : 𝓕) (c d : F) : augmentation (⇑T) (c + d) = augmentation (⇑T) c + augmentation (⇑T) d

The augmentation of an additive map is additive in the vector.

theorem Distribution.augmentation_smul_right {E : Type u_1} {F : Type u_2} {V : Type u_3} {𝓕 : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [AddCommMonoid V] [Module ℝ V] [FunLike 𝓕 (TestFunction Ω F n) V] [LinearMapClass 𝓕 ℝ (TestFunction Ω F n) V] (T : 𝓕) (a : ℝ) (c : F) : augmentation (⇑T) (a • c) = a • augmentation (⇑T) c

The augmentation of a linear map is homogeneous in the vector.

theorem Distribution.augmentation_eq {E : Type u_1} {F : Type u_2} {V : Type u_3} {𝓕 : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [FiniteDimensional ℝ E] [AddCommGroup V] [FunLike 𝓕 (TestFunction Ω F n) V] [AddMonoidHomClass 𝓕 (TestFunction Ω F n) V] (T : 𝓕) {χ : TestFunction Ω ℝ n} (hχ : ∀ᶠ (x : E) in nhdsSet (dsupport ⇑T), χ x = 1) (c : F) : augmentation (⇑T) c = T ((TestFunction.postcompCLM (ContinuousLinearMap.toSpanSingleton ℝ c)) χ)

Independence of the cutoff. The augmentation of an additive map on test functions is its value on χ • c for any test function χ equal to one on a neighbourhood of its support.

theorem Distribution.augmentation_add {E : Type u_1} {F : Type u_2} {V : Type u_3} {𝓕 : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [FiniteDimensional ℝ E] [AddCommGroup V] [FunLike 𝓕 (TestFunction Ω F n) V] [AddMonoidHomClass 𝓕 (TestFunction Ω F n) V] (T : 𝓕) {𝓖 : Type u_5} [FunLike 𝓖 (TestFunction Ω F n) V] [AddMonoidHomClass 𝓖 (TestFunction Ω F n) V] (S : 𝓖) (hT : IsCompact (dsupport ⇑T)) (hTΩ : dsupport ⇑T ⊆ ↑Ω) (hS : IsCompact (dsupport ⇑S)) (hSΩ : dsupport ⇑S ⊆ ↑Ω) (c : F) : augmentation (⇑T + ⇑S) c = augmentation (⇑T) c + augmentation (⇑S) c

The augmentation is additive on additive maps whose supports are compact subsets of Ω.

theorem Distribution.augmentation_sub {E : Type u_1} {F : Type u_2} {V : Type u_3} {𝓕 : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [FiniteDimensional ℝ E] [AddCommGroup V] [FunLike 𝓕 (TestFunction Ω F n) V] [AddMonoidHomClass 𝓕 (TestFunction Ω F n) V] (T : 𝓕) {𝓖 : Type u_5} [FunLike 𝓖 (TestFunction Ω F n) V] [AddMonoidHomClass 𝓖 (TestFunction Ω F n) V] (S : 𝓖) (hT : IsCompact (dsupport ⇑T)) (hTΩ : dsupport ⇑T ⊆ ↑Ω) (hS : IsCompact (dsupport ⇑S)) (hSΩ : dsupport ⇑S ⊆ ↑Ω) (c : F) : augmentation (⇑T - ⇑S) c = augmentation (⇑T) c - augmentation (⇑S) c

The augmentation of a difference is the difference of the augmentations.

theorem Distribution.augmentation_apply_apply {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [FiniteDimensional ℝ E] [AddCommGroup V] {x : E} (hx : x ∈ Ω) (ℓ : F →+ V) (c : F) : augmentation (fun (φ : TestFunction Ω F n) => ℓ (φ x)) c = ℓ c

The augmentation of a point evaluation. For x ∈ Ω and an additive map ℓ, the evaluation φ ↦ ℓ (φ x) has augmentation ℓ c at c. For the degree-zero point current and the unit 0-form it is one.

@[simp]

theorem Distribution.augmentation_delta {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [FiniteDimensional ℝ E] {x : E} (hx : x ∈ Ω) (c : ℝ) : augmentation (⇑(delta x)) c = c

The Dirac distribution at a point of Ω has augmentation c at c.

theorem Distribution.augmentation_smul {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {𝕜 : Type u_5} [DivisionRing 𝕜] [AddCommMonoid V] [Module 𝕜 V] (f : TestFunction Ω F n → V) (a : 𝕜) (c : F) : augmentation (a • f) c = a • augmentation f c

The augmentation is homogeneous.

theorem Distribution.augmentation_comp_extDerivCLM {E : Type u_1} {F : Type u_2} {V : Type u_3} {𝓕 : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} [FiniteDimensional ℝ E] [AddCommGroup V] {k : ℕ} [FunLike 𝓕 (TestFunction Ω (E [⋀^Fin (k + 1)]→L[ℝ] F) ⊤) V] [AddMonoidHomClass 𝓕 (TestFunction Ω (E [⋀^Fin (k + 1)]→L[ℝ] F) ⊤) V] (T : 𝓕) (hT : IsCompact (dsupport ⇑T)) (hTΩ : dsupport ⇑T ⊆ ↑Ω) (c : E [⋀^Fin k]→L[ℝ] F) : augmentation (⇑T ∘ ⇑TestFunction.extDerivCLM) c = 0

The augmentation of a boundary vanishes. If the support of T is a compact subset of Ω, then the boundary T ∘ d has augmentation zero at every constant k-form: the exterior derivative of a cutoff equal to one near the support vanishes there.