Positive functionals on commutative C⋆-algebras are measures on the character space

Let A be a unital commutative C⋆-algebra, with character space Δ = characterSpace ℂ A. A linear functional f : A → ℂ that is nonnegative on every star a * a is integration against a finite inner regular positive measure on Δ:

f a = ∫ ω, ω a ∂μ.

The Gelfand transform identifies A with C(Δ, ℂ), and under this identification star a * a runs through the nonnegative functions, so f becomes a positive linear functional on C(Δ, ℝ). The compact space Δ then carries its Riesz–Markov–Kakutani measure.

This is the commutative case of the passage from positive functionals to spectral data; it turns a cyclic commuting family of operators, such as a unitary representation of an abelian group, into a measure on the joint spectrum.

Main declarations

• LinearMap.exists_isFiniteMeasure_integral_characterSpace_eq: a functional nonnegative on star a * a is integration against a finite inner regular measure on the character space.
• WeakDual.CharacterSpace.integral_apply_star_mul_self: integrating ω ↦ ω (star a * a) gives the squared L² norm of ω ↦ ω a, so a measure representing a functional f computes f (star a * a).
• StarSubalgebra.exists_isFiniteMeasure_integral_characterSpace_eq_inner: for a closed commutative star algebra of operators on a Hilbert space, each positive vector functional a ↦ ⟪ξ, a ξ⟫ is integration against a finite inner regular measure on the character space.
• StarSubalgebra.integral_norm_sq_eq_norm_apply_sq: a measure representing such a functional computes ‖a ξ‖² as the squared L² norm of ω ↦ ω a.

References

• W. Rudin, Functional Analysis, 2nd ed., McGraw–Hill (1991), Theorem 11.18 and §12.
• G. J. Murphy, C⋆-Algebras and Operator Theory, Academic Press (1990), §2.1.

theorem LinearMap.exists_isFiniteMeasure_integral_characterSpace_eq {A : Type u_1} [CommCStarAlgebra A] [MeasurableSpace ↑(WeakDual.characterSpace ℂ A)] [BorelSpace ↑(WeakDual.characterSpace ℂ A)] (f : A →ₗ[ℂ] ℂ) (hf : ∀ (a : A), 0 ≤ f (star a * a)) : ∃ (μ : MeasureTheory.Measure ↑(WeakDual.characterSpace ℂ A)), MeasureTheory.IsFiniteMeasure μ ∧ μ.InnerRegular ∧ ∀ (a : A), f a = ∫ (ω : ↑(WeakDual.characterSpace ℂ A)), ω a ∂μ

Positive functionals on a commutative C⋆-algebra are measures on its character space. A linear functional on a unital commutative C⋆-algebra that is nonnegative on every star a * a is integration against a finite inner regular positive measure μ on the character space: f a = ∫ ω, ω a ∂μ.

theorem WeakDual.CharacterSpace.integral_apply_star_mul_self {E : Type u_2} [CStarAlgebra E] [MeasurableSpace ↑(characterSpace ℂ E)] (μ : MeasureTheory.Measure ↑(characterSpace ℂ E)) (a : E) : ∫ (ω : ↑(characterSpace ℂ E)), ω (star a * a) ∂μ = ↑(∫ (ω : ↑(characterSpace ℂ E)), ‖ω a‖ ^ 2 ∂μ)

For a measure μ on the character space of a unital C⋆-algebra, integrating ω ↦ ω (star a * a) = |ω a|² gives the squared L² norm of ω ↦ ω a. Hence if μ represents a functional f, as in LinearMap.exists_isFiniteMeasure_integral_characterSpace_eq, then f (star a * a) = ∫ |ω a|² dμ(ω).

theorem StarSubalgebra.integral_norm_sq_eq_norm_apply_sq {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (B : StarSubalgebra ℂ (H →L[ℂ] H)) [IsClosed ↑B] [MeasurableSpace ↑(WeakDual.characterSpace ℂ ↥B)] {μ : MeasureTheory.Measure ↑(WeakDual.characterSpace ℂ ↥B)} {ξ : H} (hμ : ∀ (a : ↥B), inner ℂ ξ (↑a ξ) = ∫ (ω : ↑(WeakDual.characterSpace ℂ ↥B)), ω a ∂μ) (a : ↥B) : ∫ (ω : ↑(WeakDual.characterSpace ℂ ↥B)), ‖ω a‖ ^ 2 ∂μ = ‖↑a ξ‖ ^ 2

For a closed star algebra B of operators, if a measure μ on the character space represents the positive vector functional of ξ, then ∫ |ω a|² dμ(ω) = ‖a ξ‖² for every a ∈ B.

theorem StarSubalgebra.exists_isFiniteMeasure_integral_characterSpace_eq_inner {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (B : StarSubalgebra ℂ (H →L[ℂ] H)) [IsClosed ↑B] [MeasurableSpace ↑(WeakDual.characterSpace ℂ ↥B)] [IsMulCommutative ↥B] [BorelSpace ↑(WeakDual.characterSpace ℂ ↥B)] (ξ : H) : ∃ (μ : MeasureTheory.Measure ↑(WeakDual.characterSpace ℂ ↥B)), MeasureTheory.IsFiniteMeasure μ ∧ μ.InnerRegular ∧ ∀ (a : ↥B), inner ℂ ξ (↑a ξ) = ∫ (ω : ↑(WeakDual.characterSpace ℂ ↥B)), ω a ∂μ

Positive vector functionals are measures on the character space. For a closed commutative star algebra B of operators on a complex Hilbert space and a vector ξ, the positive vector functional a ↦ ⟪ξ, a ξ⟫ is integration against a finite inner regular positive measure on the character space of B.