Components of vector-valued test functions in a basis

Let F be a finite-dimensional real normed space with a basis (bᵢ). An F-valued test function φ has the real-valued components bᵢ* ∘ φ, obtained by postcomposition with the coordinate functionals of the basis, and is recovered from them as φ = ∑ᵢ (bᵢ* ∘ φ) • bᵢ. Conversely, for a real test function ψ and a vector v : F, any continuous linear functional f on F sends the test function ψ • v to the multiple f v • ψ; in particular the components of ψ • v are the multiples b.repr v i • ψ. These identities reduce statements about F-valued test functions to statements about real-valued ones.

Main declarations

• TestFunction.postcompCLM_postcompCLM: postcomposing with L₁ and then with L₂ is postcomposing with L₂ ∘L L₁.
• TestFunction.sum_postcompCLM_toSpanSingleton_coord: an F-valued test function is the sum of its components in a basis, times the basis vectors.
• TestFunction.postcompCLM_postcompCLM_toSpanSingleton: a continuous linear functional applied to ψ • v.

@[simp]

theorem TestFunction.toBoundedContinuousFunction_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (φ : TestFunction Ω F n) : { toFun := ⇑φ, continuous_toFun := ⋯, map_bounded' := ⋯ } = 0 ↔ φ = 0

A test function is zero as a bounded continuous function exactly when it is zero.

theorem TestFunction.postcompCLM_postcompCLM {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [Algebra ℝ 𝕜] [NormedSpace 𝕜 F] [IsScalarTower ℝ 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace 𝕜 G] [IsScalarTower ℝ 𝕜 G] {H : Type u_5} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedSpace 𝕜 H] [IsScalarTower ℝ 𝕜 H] (L₁ : F →L[𝕜] G) (L₂ : G →L[𝕜] H) (φ : TestFunction Ω F n) : (postcompCLM L₂) ((postcompCLM L₁) φ) = (postcompCLM (L₂ ∘SL L₁)) φ

Postcomposing a test function with L₁ and then with L₂ is postcomposing it with L₂ ∘L L₁. Unlike SchwartzMap.postcompCLM_postcompCLM, this is not a simp lemma: it would merge the factors of the basis expansion in sum_postcompCLM_toSpanSingleton_coord into composites such as toSpanSingleton ℝ (b i) ∘L b.coord i, which simp cannot evaluate further.

theorem TestFunction.sum_postcompCLM_toSpanSingleton_coord {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} [FiniteDimensional ℝ F] {ι : Type u_3} [Fintype ι] (b : Module.Basis ι ℝ F) (φ : TestFunction Ω F n) : ∑ i : ι, (postcompCLM (ContinuousLinearMap.toSpanSingleton ℝ (b i))) ((postcompCLM (LinearMap.toContinuousLinearMap (b.coord i))) φ) = φ

An F-valued test function φ is the sum of its components bᵢ* ∘ φ in a basis b of F, each multiplied by the corresponding basis vector bᵢ.

@[simp]

theorem TestFunction.postcompCLM_postcompCLM_toSpanSingleton {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (f : F →L[ℝ] ℝ) (ψ : TestFunction Ω ℝ n) (v : F) : (postcompCLM f) ((postcompCLM (ContinuousLinearMap.toSpanSingleton ℝ v)) ψ) = f v • ψ

A continuous linear functional f on F sends the test function ψ • v to f v • ψ.