Diagonal Riesz measures for continuous-function representations

Let π : C(K, ℂ) →⋆ₐ[ℂ] (H →L[ℂ] H) be a unital star representation on a complex Hilbert space, with K compact Hausdorff. For each ξ : H, the positive functional f ↦ ⟪ξ, π(f) ξ⟫ determines a finite regular Borel measure on K.

The measure is determined by the identity ∫ f dμ_ξ = ⟪ξ, π f ξ⟫ for each continuous f. Its total mass is ‖ξ‖², and ∫ ‖f‖² dμ_ξ = ‖π f ξ‖². The continuous functional calculus of a normal operator specializes this construction: ContinuousLinearMap.diagMeasure is the StarAlgHom.representationDiagMeasure of cfcHom.

Main results

• StarAlgHom.representationDiagMeasure: the finite regular Riesz measure at a vector.
• StarAlgHom.integral_representationDiagMeasure: the continuous scalar integral identity.
• StarAlgHom.eq_representationDiagMeasure_iff: characterization among regular measures.
• StarAlgHom.representationDiagMeasure_real_univ and StarAlgHom.representationDiagMeasure_univ: total mass ‖ξ‖².
• StarAlgHom.integral_norm_sq_representationDiagMeasure: the squared L² identity.
• StarAlgHom.representationDiagMeasure_smul: scaling the vector by c scales the measure by ‖c‖².

The final identity uses StarAlgHom.norm_sq_apply_eq_re_inner_star_mul, a quadratic identity for arbitrary star-algebra representations.

noncomputable def StarAlgHom.representationDiagMeasure {K : Type u_1} [TopologicalSpace K] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : C(K, ℂ) →⋆ₐ[ℂ] H →L[ℂ] H) [CompactSpace K] [T2Space K] [MeasurableSpace K] [BorelSpace K] (ξ : H) : MeasureTheory.Measure K

The finite regular Riesz measure of the positive functional f ↦ ⟪ξ, π f ξ⟫. For continuous f, it satisfies ∫ f dμ_ξ = ⟪ξ, π f ξ⟫ and is unique among regular Borel measures.

instance StarAlgHom.isFiniteMeasure_representationDiagMeasure {K : Type u_1} [TopologicalSpace K] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : C(K, ℂ) →⋆ₐ[ℂ] H →L[ℂ] H) [CompactSpace K] [T2Space K] [MeasurableSpace K] [BorelSpace K] (ξ : H) : MeasureTheory.IsFiniteMeasure (π.representationDiagMeasure ξ)

instance StarAlgHom.regular_representationDiagMeasure {K : Type u_1} [TopologicalSpace K] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : C(K, ℂ) →⋆ₐ[ℂ] H →L[ℂ] H) [CompactSpace K] [T2Space K] [MeasurableSpace K] [BorelSpace K] (ξ : H) : (π.representationDiagMeasure ξ).Regular

theorem StarAlgHom.integral_representationDiagMeasure {K : Type u_1} [TopologicalSpace K] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : C(K, ℂ) →⋆ₐ[ℂ] H →L[ℂ] H) [CompactSpace K] [T2Space K] [MeasurableSpace K] [BorelSpace K] (ξ : H) (f : C(K, ℂ)) : ∫ (x : K), f x ∂π.representationDiagMeasure ξ = inner ℂ ξ ((π f) ξ)

Integrating a continuous function against the diagonal measure gives the scalar matrix coefficient ⟪ξ, π f ξ⟫ for the fixed vector ξ.

theorem StarAlgHom.eq_representationDiagMeasure_iff {K : Type u_1} [TopologicalSpace K] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : C(K, ℂ) →⋆ₐ[ℂ] H →L[ℂ] H) [CompactSpace K] [T2Space K] [MeasurableSpace K] [BorelSpace K] (ξ : H) (μ : MeasureTheory.Measure K) [μ.Regular] : μ = π.representationDiagMeasure ξ ↔ ∀ (f : C(K, ℂ)), ∫ (x : K), f x ∂μ = inner ℂ ξ ((π f) ξ)

A regular measure μ equals the diagonal measure μ_ξ iff ∫ f dμ = ⟪ξ, π f ξ⟫ for every continuous complex-valued f.

@[simp]

theorem StarAlgHom.representationDiagMeasure_real_univ {K : Type u_1} [TopologicalSpace K] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : C(K, ℂ) →⋆ₐ[ℂ] H →L[ℂ] H) [CompactSpace K] [T2Space K] [MeasurableSpace K] [BorelSpace K] (ξ : H) : (π.representationDiagMeasure ξ).real Set.univ = ‖ξ‖ ^ 2

The mass of the representation diagonal measure is the squared vector norm.

@[simp]

theorem StarAlgHom.representationDiagMeasure_univ {K : Type u_1} [TopologicalSpace K] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : C(K, ℂ) →⋆ₐ[ℂ] H →L[ℂ] H) [CompactSpace K] [T2Space K] [MeasurableSpace K] [BorelSpace K] (ξ : H) : (π.representationDiagMeasure ξ) Set.univ = ‖ξ‖ₑ ^ 2

The total mass, in extended nonnegative reals.

theorem StarAlgHom.representationDiagMeasure_smul {K : Type u_1} [TopologicalSpace K] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : C(K, ℂ) →⋆ₐ[ℂ] H →L[ℂ] H) [CompactSpace K] [T2Space K] [MeasurableSpace K] [BorelSpace K] (c : ℂ) (ξ : H) : π.representationDiagMeasure (c • ξ) = ‖c‖₊ ^ 2 • π.representationDiagMeasure ξ

Scaling the vector by c scales the diagonal measure by ‖c‖².

theorem StarAlgHom.representationDiagMeasure_smul_of_norm_eq_one {K : Type u_1} [TopologicalSpace K] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : C(K, ℂ) →⋆ₐ[ℂ] H →L[ℂ] H) [CompactSpace K] [T2Space K] [MeasurableSpace K] [BorelSpace K] {c : ℂ} (hc : ‖c‖ = 1) (ξ : H) : π.representationDiagMeasure (c • ξ) = π.representationDiagMeasure ξ

Scaling the vector by a unit complex number does not change the diagonal measure.

@[simp]

theorem StarAlgHom.representationDiagMeasure_neg {K : Type u_1} [TopologicalSpace K] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : C(K, ℂ) →⋆ₐ[ℂ] H →L[ℂ] H) [CompactSpace K] [T2Space K] [MeasurableSpace K] [BorelSpace K] (ξ : H) : π.representationDiagMeasure (-ξ) = π.representationDiagMeasure ξ

Negating the vector does not change the diagonal measure.

theorem StarAlgHom.integral_norm_sq_representationDiagMeasure {K : Type u_1} [TopologicalSpace K] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : C(K, ℂ) →⋆ₐ[ℂ] H →L[ℂ] H) [CompactSpace K] [T2Space K] [MeasurableSpace K] [BorelSpace K] (ξ : H) (f : C(K, ℂ)) : ∫ (x : K), ‖f x‖ ^ 2 ∂π.representationDiagMeasure ξ = ‖(π f) ξ‖ ^ 2

For every continuous symbol f, the squared L²(μ_ξ) norm equals ‖π(f) ξ‖²: explicitly, ∫ ‖f‖² dμ_ξ = ‖π(f) ξ‖².