Matrix coefficients of strongly continuous unitary representations

Let π be a strongly continuous unitary representation of a locally compact abelian group G on a complex Hilbert space H, and let ξ ∈ H. The diagonal matrix coefficient g ↦ ⟪ξ, π(g) ξ⟫ is the Fourier–Stieltjes transform of a finite inner regular positive measure on the Pontryagin dual of G. This is the cyclic form of the Stone–Naimark–Ambrose–Godement spectral theorem.

The operators π(g) are only strongly continuous, so the spectral measure is built from the integrated operators π(f), f ∈ L¹(G), taken with respect to a Haar measure. They generate a unital commutative C⋆-algebra A, and the vector functional a ↦ ⟪ξ, a ξ⟫ is integration against a finite measure ν on the character space of A. A character ω that does not vanish on every integrated operator determines a continuous group character χ_ω with ω(π(g) π(f)) = χ_ω(g) ω(π(f)); this assignment is continuous on the open set of such characters, and the image of ν under it is the required measure. The characters annihilating every integrated operator do not contribute: since π(f) ξ approximates ξ, the identity ∫ |ω(π(f)) - 1|² dν = ‖π(f) ξ - ξ‖² forces their measure to be zero. Compact approximation inside the open set of non-annihilating characters then proves that the pushforward measure is inner regular.

No second countability of G and no separability of H is needed: the integrated form is defined for the Haar measure through its inner regularity for compact sets.

Main declarations

• ContRepresentation.exists_pontryaginMeasureTransform_eq_inner: a diagonal matrix coefficient of a strongly continuous unitary representation of a locally compact abelian group is the Fourier–Stieltjes transform of a finite inner regular measure on the dual group.

References

• G. B. Folland, A Course in Abstract Harmonic Analysis, 2nd ed., CRC Press (2016), §§3.2, 4.4 and Theorem 4.44.

theorem ContRepresentation.exists_pontryaginMeasureTransform_eq_inner {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] [MeasurableSpace (PontryaginDual (Multiplicative G))] [BorelSpace (PontryaginDual (Multiplicative G))] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : ContRepresentation ℂ (Multiplicative G) H) (hcont : ∀ (v : H), Continuous fun (g : G) => (π (Multiplicative.ofAdd g)) v) (hπ : π.IsUnitary) (ξ : H) : ∃ (μ : MeasureTheory.FiniteMeasure (PontryaginDual (Multiplicative G))), (↑μ).InnerRegular ∧ ∀ (g : G), μ.pontryaginMeasureTransform g = inner ℂ ξ ((π (Multiplicative.ofAdd g)) ξ)

Spectral theorem for strongly continuous unitary representations, cyclic form. For a strongly continuous unitary representation π of a locally compact abelian group G on a Hilbert space H and a vector ξ, the matrix coefficient g ↦ ⟪ξ, π(g) ξ⟫ is the Fourier–Stieltjes transform of a finite inner regular measure on the Pontryagin dual of G.