Transport of test functions along continuous linear equivalences

A continuous linear equivalence e : E ≃L[ℝ] E' carries a test function φ on an open set V of E to the test function φ ∘ e.symm on any open set Ω of E' containing e '' V. This transport is continuous for the LF topologies, so precomposing with it transports distributions along e. Its derivative is the derivative of φ precomposed with e.symm. A test vector field is transported by also applying e to its values, y ↦ e (φ (e.symm y)); its divergence is then the transported divergence of φ, because the trace is invariant under conjugation.

These formulas transport the test-field pairings that define distributional derivatives, variation and perimeter along linear changes of variables, in particular along rotations and reflections.

Main declarations

• ContinuousLinearEquiv.transportSupportedIn: transport of tests supported in a compact K to tests supported in e '' K, as a continuous linear map.
• ContinuousLinearEquiv.transportTestFunction: transport of test functions along a continuous linear equivalence, changing their domain, as a continuous linear map.
• ContinuousLinearEquiv.transportTestFunction_apply: evaluation of a transported test function.
• ContinuousLinearEquiv.transportTestFunction_trans, ContinuousLinearEquiv.transportTestFunction_transportTestFunction_symm: functoriality.
• ContinuousLinearEquiv.transportTestFunction_postcompCLM: transport commutes with postcomposition by a continuous linear map.
• ContinuousLinearEquiv.fderiv_transportTestFunction: the Fréchet derivative of a transported test function.
• ContinuousLinearEquiv.divergenceCLM_postcompCLM_transportTestFunction: the divergence of a transported test vector field is the transported divergence.

Implementation notes

Both transports work at every order of smoothness n. Continuity of transportTestFunction is checked on each space of tests supported in a fixed compact K ⊆ V, whose transports are supported in e '' K (transportSupportedIn); there the i-th derivative of φ ∘ e.symm is bounded by ‖e.symm‖ ^ i times that of φ.

def ContinuousLinearEquiv.transportSupportedIn {E : Type u_1} {E' : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (e : E ≃L[ℝ] E') (K : TopologicalSpace.Compacts E) : ContDiffMapSupportedIn E F n K →L[ℝ] ContDiffMapSupportedIn E' F n (TopologicalSpace.Compacts.map ⇑e ⋯ K)

Transport along e of tests supported in a compact K, which are supported in e '' K, as a continuous linear map. Its i-th seminorm is at most ‖e.symm‖ ^ i times that of the original test.

@[simp]

theorem ContinuousLinearEquiv.transportSupportedIn_apply {E : Type u_1} {E' : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (e : E ≃L[ℝ] E') (K : TopologicalSpace.Compacts E) (φ : ContDiffMapSupportedIn E F n K) (y : E') : ((e.transportSupportedIn K) φ) y = φ (e.symm y)

A transported test supported in K is evaluated at the inversely transported point.

noncomputable def ContinuousLinearEquiv.transportTestFunction {E : Type u_1} {E' : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] {V : TopologicalSpace.Opens E} {Ω : TopologicalSpace.Opens E'} {n : ℕ∞} (e : E ≃L[ℝ] E') (hVO : Set.MapsTo ⇑e ↑V ↑Ω) : TestFunction V F n →L[ℝ] TestFunction Ω F n

Transport test functions on V along a continuous linear equivalence e, regarding the result φ ∘ e.symm as a test function on an open set Ω containing e '' V. This is a continuous linear map for the LF topologies.

@[simp]

theorem ContinuousLinearEquiv.transportTestFunction_apply {E : Type u_1} {E' : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] {V : TopologicalSpace.Opens E} {Ω : TopologicalSpace.Opens E'} {n : ℕ∞} (e : E ≃L[ℝ] E') (hVO : Set.MapsTo ⇑e ↑V ↑Ω) (φ : TestFunction V F n) (y : E') : ((e.transportTestFunction hVO) φ) y = φ (e.symm y)

A transported test function is evaluated at the inversely transported point.

theorem ContinuousLinearEquiv.transportTestFunction_trans {E : Type u_1} {E' : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] {V : TopologicalSpace.Opens E} {Ω : TopologicalSpace.Opens E'} {n : ℕ∞} {E'' : Type u_4} [NormedAddCommGroup E''] [NormedSpace ℝ E''] {W : TopologicalSpace.Opens E''} (e₁ : E ≃L[ℝ] E') (e₂ : E' ≃L[ℝ] E'') (h₁ : Set.MapsTo ⇑e₁ ↑V ↑Ω) (h₂ : Set.MapsTo ⇑e₂ ↑Ω ↑W) (h : Set.MapsTo ⇑(e₁.trans e₂) ↑V ↑W) (φ : TestFunction V F n) : ((e₁.trans e₂).transportTestFunction h) φ = (e₂.transportTestFunction h₂) ((e₁.transportTestFunction h₁) φ)

Transporting along a composite of continuous linear equivalences is transporting along each in turn.

@[simp]

theorem ContinuousLinearEquiv.transportTestFunction_transportTestFunction_symm {E : Type u_1} {E' : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] {V : TopologicalSpace.Opens E} {Ω : TopologicalSpace.Opens E'} {n : ℕ∞} (e : E ≃L[ℝ] E') (hVO : Set.MapsTo ⇑e ↑V ↑Ω) (hOV : Set.MapsTo ⇑e.symm ↑Ω ↑V) (φ : TestFunction Ω F n) : (e.transportTestFunction hVO) ((e.symm.transportTestFunction hOV) φ) = φ

Transporting along e.symm and then along e gives back the original test function.

theorem ContinuousLinearEquiv.transportTestFunction_postcompCLM {E : Type u_1} {E' : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] {V : TopologicalSpace.Opens E} {Ω : TopologicalSpace.Opens E'} {n : ℕ∞} {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] (e : E ≃L[ℝ] E') (hVO : Set.MapsTo ⇑e ↑V ↑Ω) (L : F →L[ℝ] G) (φ : TestFunction V F n) : (e.transportTestFunction hVO) ((TestFunction.postcompCLM L) φ) = (TestFunction.postcompCLM L) ((e.transportTestFunction hVO) φ)

Transport commutes with postcomposition by a continuous linear map.

@[simp]

theorem ContinuousLinearEquiv.fderiv_transportTestFunction {E : Type u_1} {E' : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] {V : TopologicalSpace.Opens E} {Ω : TopologicalSpace.Opens E'} (e : E ≃L[ℝ] E') (hVO : Set.MapsTo ⇑e ↑V ↑Ω) (φ : TestFunction V F ⊤) (y : E') : fderiv ℝ (⇑((e.transportTestFunction hVO) φ)) y = fderiv ℝ (⇑φ) (e.symm y) ∘SL ↑e.symm

The Fréchet derivative of a transported test function is the transported derivative, precomposed with e.symm.

@[simp]

theorem ContinuousLinearEquiv.divergenceCLM_postcompCLM_transportTestFunction {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] {V : TopologicalSpace.Opens E} {Ω : TopologicalSpace.Opens E'} [FiniteDimensional ℝ E] [FiniteDimensional ℝ E'] (e : E ≃L[ℝ] E') (hVO : Set.MapsTo ⇑e ↑V ↑Ω) (φ : TestFunction V E ⊤) : TestFunction.divergenceCLM ((TestFunction.postcompCLM ↑e) ((e.transportTestFunction hVO) φ)) = (e.transportTestFunction hVO) (TestFunction.divergenceCLM φ)

The divergence of a transported test vector field y ↦ e (φ (e.symm y)) is the transported divergence of φ.