Continuous functionals for the topology of pointwise convergence

Every linear functional on E →SLₚₜ[σ] F which is continuous for the topology of pointwise convergence (the strong operator topology) is a finite sum T ↦ ∑ x ∈ s, g x (T x) of continuous functionals of values (PointwiseConvergenceCLM.exists_finset_sum_eq). On a Hilbert space, writing each g x as an inner product gives the usual finite sums of matrix coefficients.

References

Kadison–Ringrose, Fundamentals of the Theory of Operator Algebras I, Theorem 5.1.2.

theorem PointwiseConvergenceCLM.exists_finset_sum_eq {𝕜₁ : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [NormedField 𝕜₁] [RCLike 𝕜] {σ : 𝕜₁ →+* 𝕜} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (φ : StrongDual 𝕜 (E →SLₚₜ[σ] F)) : ∃ (s : Finset E) (g : E → StrongDual 𝕜 F), ∀ (T : E →SLₚₜ[σ] F), φ T = ∑ x ∈ s, (g x) (T x)

Continuous functionals in the strong operator topology. A linear functional on operators which is continuous for the topology of pointwise convergence is a finite sum of functionals T ↦ g x (T x), each a continuous functional on F applied to the value at a vector x.