Maps on vector-valued tests as operator-valued distributions

Let F be a finite-dimensional real normed space, V a real normed space and Ω an open subset of a real normed space E. A continuous linear map T from the F-valued test functions 𝓓^{n}(Ω, F) to V determines the F →L[ℝ] V-valued distribution

ψ ↦ (v ↦ T (ψ • v))

on the real test functions 𝓓^{n}(Ω, ℝ). Conversely, writing an F-valued test function componentwise in a basis (bᵢ) of F, as φ = ∑ᵢ (bᵢ* ∘ φ) • bᵢ, an F →L[ℝ] V-valued distribution S determines the map φ ↦ ∑ᵢ S (bᵢ* ∘ φ) bᵢ, independently of the basis. These two constructions are mutually inverse, and both are continuous for the topologies of uniform convergence on compact sets of tests (TestFunction.dualEquivDistribution).

For V = ℝ, this identifies functionals on vector-valued tests, such as currents in a Euclidean chart (where the tests are the differential forms, valued in alternating maps), with Mathlib's dual-valued distributions 𝓓'^{n}(Ω, F →L[ℝ] ℝ). Statements about distributions, for instance a constancy criterion for distributions all of whose derivatives vanish, thereby transfer componentwise to functionals on vector-valued tests. The equivalence intertwines the derivatives on both sides (TestFunction.dualEquivDistribution_lineDeriv) and sends integration against a locally integrable field G : E → F →L[ℝ] V to the distribution of G (TestFunction.dualEquivDistribution_integralAgainstBilinCLM).

Main declarations

• TestFunction.dualEquivDistribution: the continuous linear equivalence between 𝓓^{n}(Ω, F) →L_c[ℝ] V and 𝓓'^{n}(Ω, F →L[ℝ] V).
• TestFunction.dualEquivDistribution_apply_apply and TestFunction.dualEquivDistribution_symm_apply_eq_sum: its formula, and the formula of its inverse in an arbitrary basis of F.
• TestFunction.dualEquivDistribution_lineDeriv: compatibility with directional derivatives, and TestFunction.lineDeriv_dualEquivDistribution_eq_zero: a functional annihilating all derivatives ∂_v φ gives a distribution with vanishing derivative along v.
• TestFunction.dualEquivDistribution_integralAgainstBilinCLM and TestFunction.dualEquivDistribution_symm_ofFun: compatibility with integration against a locally integrable function.

References

• L. Schwartz, Théorie des distributions à valeurs vectorielles I, Ann. Inst. Fourier 7 (1957).

noncomputable def TestFunction.dualEquivDistribution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] {n : ℕ∞} : CompactConvergenceCLM (RingHom.id ℝ) (TestFunction Ω F n) V ≃L[ℝ] Distribution Ω (F →L[ℝ] V) n

Maps on vector-valued tests are operator-valued distributions. For a finite-dimensional real normed space F and a real normed space V, the continuous linear maps from the F-valued test functions on Ω to V correspond to the F →L[ℝ] V-valued distributions on Ω: a map T corresponds to the distribution ψ ↦ (v ↦ T (ψ • v)). Both spaces carry the topology of uniform convergence on compact sets, and the correspondence is a homeomorphism for these topologies.

@[simp]

theorem TestFunction.dualEquivDistribution_apply_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] {n : ℕ∞} (T : CompactConvergenceCLM (RingHom.id ℝ) (TestFunction Ω F n) V) (ψ : TestFunction Ω ℝ n) (v : F) : ((dualEquivDistribution T) ψ) v = T ((postcompCLM (ContinuousLinearMap.toSpanSingleton ℝ v)) ψ)

The distribution attached to a continuous linear map T on F-valued tests evaluates a real test function ψ at v : F as T (ψ • v).

@[simp]

theorem TestFunction.dualEquivDistribution_symm_apply_postcompCLM {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] {n : ℕ∞} (S : Distribution Ω (F →L[ℝ] V) n) (ψ : TestFunction Ω ℝ n) (v : F) : (dualEquivDistribution.symm S) ((postcompCLM (ContinuousLinearMap.toSpanSingleton ℝ v)) ψ) = (S ψ) v

The map on F-valued tests attached to an F →L[ℝ] V-valued distribution S evaluates the test function ψ • v as S ψ v.

theorem TestFunction.dualEquivDistribution_symm_apply_eq_sum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] {n : ℕ∞} {ι : Type u_4} [Fintype ι] (b : Module.Basis ι ℝ F) (S : Distribution Ω (F →L[ℝ] V) n) (φ : TestFunction Ω F n) : (dualEquivDistribution.symm S) φ = ∑ i : ι, (S ((postcompCLM (LinearMap.toContinuousLinearMap (b.coord i))) φ)) (b i)

The map on F-valued tests attached to an F →L[ℝ] V-valued distribution S, in an arbitrary basis b of F: it sends φ to ∑ i, S (bᵢ* ∘ φ) bᵢ, where bᵢ* are the coordinate functionals of b.

theorem TestFunction.dualEquivDistribution_lineDeriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] {n k : ℕ∞} (T : CompactConvergenceCLM (RingHom.id ℝ) (TestFunction Ω F k) V) (v : E) : dualEquivDistribution (-(ContinuousLinearMap.precompCompactConvergenceCLM V (lineDerivCLM ℝ v)) T) = (Distribution.lineDerivCLM v) (dualEquivDistribution T)

dualEquivDistribution intertwines the derivatives: the derivative -T (∂_v ·) of a continuous linear map T on F-valued tests corresponds to the distributional derivative of the distribution attached to T.

theorem TestFunction.lineDeriv_dualEquivDistribution_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] {n k : ℕ∞} {T : CompactConvergenceCLM (RingHom.id ℝ) (TestFunction Ω F k) V} {v : E} (hT : ∀ (φ : TestFunction Ω F n), T ((lineDerivCLM ℝ v) φ) = 0) : (Distribution.lineDerivCLM v) (dualEquivDistribution T) = 0

If a continuous linear map T on F-valued tests annihilates every derivative ∂_v φ of a test function, then the distribution attached to T has vanishing derivative along v.

theorem TestFunction.dualEquivDistribution_integralAgainstBilinCLM {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] {n : ℕ∞} [MeasurableSpace E] [OpensMeasurableSpace E] (G : E → F →L[ℝ] V) (μ : MeasureTheory.Measure E) : dualEquivDistribution ((ContinuousLinearMap.toUniformConvergenceCLM (RingHom.id ℝ) V {S : Set (TestFunction Ω F n) | IsCompact S}) (integralAgainstBilinCLM (ContinuousLinearMap.apply ℝ V) μ G)) = Distribution.ofFun Ω G μ n

dualEquivDistribution sends integration against a field G : E → F →L[ℝ] V, the map φ ↦ ∫ x, G x (φ x) ∂μ, to the distribution Distribution.ofFun Ω G μ n of G. Both sides vanish when G is not locally integrable on Ω.

theorem TestFunction.dualEquivDistribution_symm_ofFun {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] {n : ℕ∞} [MeasurableSpace E] [OpensMeasurableSpace E] (G : E → F →L[ℝ] V) (μ : MeasureTheory.Measure E) : dualEquivDistribution.symm (Distribution.ofFun Ω G μ n) = (ContinuousLinearMap.toUniformConvergenceCLM (RingHom.id ℝ) V {S : Set (TestFunction Ω F n) | IsCompact S}) (integralAgainstBilinCLM (ContinuousLinearMap.apply ℝ V) μ G)

The map on F-valued tests attached to the distribution of a field G : E → F →L[ℝ] V is integration against G.