Finite localization of test functions

A test function can be written as a finite sum of tests subordinate to any open cover of its support. Consequently, an additive map on test functions which vanishes locally vanishes globally; continuity of the additive map is not required. Every compact subset of the domain also has a cutoff test function equal to one on a neighbourhood of it, and every point of the domain has a test function with a prescribed value there, supported in a given neighbourhood of the point. In a finite-dimensional space, a compact set K in the interior of a compact set K' has a complex smooth cutoff supported in K' and equal to one on K (ContDiffMapSupportedIn.exists_eqOn_one_of_subset_interior).

Multiplication by a smooth function χ whose closed support meets Ω only inside an open set U sends tests on Ω to tests on U. This is TestFunction.cutoffCLM, a continuous linear map 𝓓^{n}(Ω, F) →L[ℝ] 𝓓^{n}(U, F) for the LF topologies; it is the localization step used to glue distributions and currents defined on the members of an open cover.

The decomposition uses Mathlib's SmoothPartitionOfUnity.exists_isSubordinate, applied to the compact support, and the cutoff packages IsCompact.exists_contDiff_cutoff as a test function. This is the partition-of-unity localization of distributions described in Hörmander, The Analysis of Linear Partial Differential Operators I, §2.2 (Localization).

noncomputable def TestFunction.cutoffCLM {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω U : TopologicalSpace.Opens E} {n : ℕ∞} {χ : E → ℝ} (hχ : ContDiff ℝ (↑n) χ) (hχU : tsupport χ ∩ ↑Ω ⊆ ↑U) : TestFunction Ω F n →L[ℝ] TestFunction U F n

Multiplication φ ↦ χ φ by a C^n function χ whose topological support meets Ω only inside U, as a continuous linear map from tests on Ω to tests on U. When U = Ω this is TestFunction.smulLeftCLM.

@[simp]

theorem TestFunction.cutoffCLM_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω U : TopologicalSpace.Opens E} {n : ℕ∞} {χ : E → ℝ} (hχ : ContDiff ℝ (↑n) χ) (hχU : tsupport χ ∩ ↑Ω ⊆ ↑U) (φ : TestFunction Ω F n) (x : E) : ((cutoffCLM hχ hχU) φ) x = χ x • φ x

theorem TestFunction.exists_sum_subordinate {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} (φ : TestFunction Ω F n) {ι : Type u_3} (U : ι → Set E) (hU : ∀ (i : ι), IsOpen (U i)) (hcover : tsupport ⇑φ ⊆ ⋃ (i : ι), U i) : ∃ (s : Finset ι) (ψ : ↥s → TestFunction Ω F n), (∀ (i : ↥s), tsupport ⇑(ψ i) ⊆ U ↑i) ∧ ∑ i : ↥s, ψ i = φ ∧ ∀ (i : ↥s) (x : E), ‖(ψ i) x‖ ≤ ‖φ x‖

A test function is a finite sum of test functions supported in members of an open cover of its topological support. The summands are pointwise no larger in norm than the test function itself.

theorem TestFunction.exists_cutoff_tsupport_subset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {K W : Set E} (hK : IsCompact K) (hW : IsOpen W) (hKW : K ⊆ W) (hWΩ : W ⊆ ↑Ω) : ∃ (χ : TestFunction Ω ℝ n), (∀ (x : E), χ x ∈ Set.Icc 0 1) ∧ (∀ᶠ (x : E) in nhdsSet K, χ x = 1) ∧ tsupport ⇑χ ⊆ W

A compact subset K of an open set W contained in the domain has a test function with values in [0, 1], equal to one on a neighbourhood of K, whose topological support lies in W.

theorem TestFunction.exists_eventually_eq_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {K : Set E} (hK : IsCompact K) (hKΩ : K ⊆ ↑Ω) : ∃ (χ : TestFunction Ω ℝ n), (∀ᶠ (x : E) in nhdsSet K, χ x = 1) ∧ ∀ (x : E), χ x ∈ Set.Icc 0 1

Every compact subset of the domain has a test function with values in [0, 1] that is equal to one on a neighbourhood of it.

theorem TestFunction.exists_tsupport_subset_apply_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {x : E} {s : Set E} (hs : s ∈ nhds x) (hsΩ : s ⊆ ↑Ω) (v : F) : ∃ (φ : TestFunction Ω F n), tsupport ⇑φ ⊆ s ∧ φ x = v

Every point of the domain has a test function taking a prescribed value at it and supported in a given neighbourhood of it.

theorem TestFunction.exists_norm_le_one_mul_eq_abs {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {s : Finset E} (a : E → ℝ) (hs : ↑s ⊆ ↑Ω) : ∃ (φ : TestFunction Ω ℝ n), (∀ (x : E), ‖φ x‖ ≤ 1) ∧ ∀ x ∈ s, a x * φ x = |a x|

A real test function bounded in norm by one can realize the signs of arbitrary coefficients on a finite subset of its domain.

theorem ContDiffMapSupportedIn.exists_eqOn_one_of_subset_interior {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {K K' : TopologicalSpace.Compacts E} (h : ↑K ⊆ interior ↑K') : ∃ (χ : ContDiffMapSupportedIn E ℂ ⊤ K'), Set.EqOn (⇑χ) 1 ↑K

A compact set K in the interior of a compact set K' of a finite-dimensional space has a smooth cutoff supported in K' and equal to one on K.

theorem AddMonoidHom.eq_zero_of_locally_vanishing {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [AddCommMonoid G] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} (T : TestFunction Ω F n →+ G) (h : ∀ x ∈ Ω, ∃ (U : Set E), IsOpen U ∧ x ∈ U ∧ ∀ (φ : TestFunction Ω F n), tsupport ⇑φ ⊆ U → T φ = 0) : T = 0

An additive map on test functions vanishes if every point of the domain has an open neighborhood on whose supported tests it vanishes.