Changing the coefficient space of test functions

A continuous linear equivalence of coefficient spaces induces a continuous linear equivalence of native test-function spaces. These maps preserve the exact support and commute with extension to a larger open domain. Continuity uses Mathlib's TestFunction.postcompCLM, hence the native locally convex inductive-limit topology.

noncomputable def TestFunction.postcompCLE {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [Algebra ℝ 𝕜] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace 𝕜 F] [NormedSpace 𝕜 G] [IsScalarTower ℝ 𝕜 F] [IsScalarTower ℝ 𝕜 G] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} (e : F ≃L[𝕜] G) : TestFunction Ω F n ≃L[𝕜] TestFunction Ω G n

A change of coefficient space acts on test functions by pointwise postcomposition.

@[simp]

theorem TestFunction.postcompCLE_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [Algebra ℝ 𝕜] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace 𝕜 F] [NormedSpace 𝕜 G] [IsScalarTower ℝ 𝕜 F] [IsScalarTower ℝ 𝕜 G] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} (e : F ≃L[𝕜] G) (φ : TestFunction Ω F n) (x : E) : ((postcompCLE e) φ) x = e (φ x)

@[simp]

theorem TestFunction.postcompCLE_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [Algebra ℝ 𝕜] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace 𝕜 F] [NormedSpace 𝕜 G] [IsScalarTower ℝ 𝕜 F] [IsScalarTower ℝ 𝕜 G] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} (e : F ≃L[𝕜] G) : (postcompCLE e).symm = postcompCLE e.symm

@[simp]

theorem TestFunction.coe_postcompCLE {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [Algebra ℝ 𝕜] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace 𝕜 F] [NormedSpace 𝕜 G] [IsScalarTower ℝ 𝕜 F] [IsScalarTower ℝ 𝕜 G] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} (e : F ≃L[𝕜] G) : ↑(postcompCLE e) = postcompCLM ↑e

The underlying continuous linear map is Mathlib's coefficient postcomposition map.

@[simp]

theorem TestFunction.postcompCLE_refl {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [Algebra ℝ 𝕜] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [IsScalarTower ℝ 𝕜 F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} : postcompCLE (ContinuousLinearEquiv.refl 𝕜 F) = ContinuousLinearEquiv.refl 𝕜 (TestFunction Ω F n)

The identity coefficient change acts as the identity on test functions.

theorem TestFunction.postcompCLE_trans {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [Algebra ℝ 𝕜] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace 𝕜 F] [NormedSpace 𝕜 G] [IsScalarTower ℝ 𝕜 F] [IsScalarTower ℝ 𝕜 G] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {H : Type u_5} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedSpace 𝕜 H] [IsScalarTower ℝ 𝕜 H] (e : F ≃L[𝕜] G) (e' : G ≃L[𝕜] H) : postcompCLE (e.trans e') = (postcompCLE e).trans (postcompCLE e')

Successive coefficient changes compose as continuous linear equivalences.

@[simp]

theorem TestFunction.tsupport_postcompCLE {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [Algebra ℝ 𝕜] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace 𝕜 F] [NormedSpace 𝕜 G] [IsScalarTower ℝ 𝕜 F] [IsScalarTower ℝ 𝕜 G] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} (e : F ≃L[𝕜] G) (φ : TestFunction Ω F n) : tsupport ⇑((postcompCLE e) φ) = tsupport ⇑φ

An invertible coefficient change preserves the topological support exactly.

theorem TestFunction.postcompCLE_monoCLM {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [Algebra ℝ 𝕜] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace 𝕜 F] [NormedSpace 𝕜 G] [IsScalarTower ℝ 𝕜 F] [IsScalarTower ℝ 𝕜 G] {Ω Ω' : TopologicalSpace.Opens E} {n : ℕ∞} (e : F ≃L[𝕜] G) {m : ℕ∞} (φ : TestFunction Ω F n) : (postcompCLE e) ((monoCLM 𝕜) φ) = (monoCLM 𝕜) ((postcompCLE e) φ)

Coefficient changes commute with extension and lowering regularity, including the zero-map case of monoCLM when the domains or orders are incompatible.