The diagonal measure of a normal operator

Let a be a normal bounded operator on a complex Hilbert space H and let ξ ∈ H. The functional f ↦ ⟪ξ, f(a) ξ⟫ on continuous functions on spectrum ℂ a is positive, because the continuous functional calculus sends nonnegative functions to positive operators. By the Riesz–Markov–Kakutani theorem it is integration against a unique finite Borel measure μ_ξ on the spectrum:

⟪ξ, f(a) ξ⟫ = ∫ f dμ_ξ.

This measure is the scalar spectral measure of a at ξ. Its total mass is ‖ξ‖², and it computes ‖f(a) ξ‖² as the squared L²(μ_ξ) norm of f. Polarizing these diagonal measures gives the matrix elements of the bounded Borel functional calculus, which extends the continuous calculus from continuous to bounded Borel symbols.

The diagonal measure and its integration identities specialize StarAlgHom.representationDiagMeasure to the continuous functional calculus cfcHom.

LinearMap.exists_isFiniteMeasure_integral_characterSpace_eq gives the analogous representation on the character space of a commutative C⋆-algebra, as an existence statement. Here the measure lives on the spectrum itself and is a named definition, so later constructions can refer to it.

Main declarations

• ContinuousLinearMap.diagMeasure a ξ: the diagonal measure of a normal operator a at ξ, a finite measure on spectrum ℂ a.
• ContinuousLinearMap.integral_diagMeasure_eq_inner_cfcHom, ContinuousLinearMap.integral_diagMeasure_eq_inner_cfc: ∫ f dμ_ξ = ⟪ξ, f(a) ξ⟫.
• ContinuousLinearMap.eq_diagMeasure_iff: μ_ξ is the only finite measure with this property.
• ContinuousLinearMap.diagMeasure_univ: the total mass of μ_ξ is ‖ξ‖².
• ContinuousLinearMap.integral_norm_sq_diagMeasure: ∫ |f|² dμ_ξ = ‖f(a) ξ‖².

References

• M. Reed, B. Simon, Methods of Modern Mathematical Physics I: Functional Analysis, rev. ed., Academic Press (1980), §VII.2.
• J. B. Conway, A Course in Functional Analysis, 2nd ed., Springer (1990), §IX.2.

noncomputable def ContinuousLinearMap.diagMeasure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] (ξ : H) : MeasureTheory.Measure ↑(spectrum ℂ a)

The diagonal measure μ_ξ of a normal operator a at a vector ξ: the diagonal Riesz measure for its unital continuous functional calculus, characterized by the identity ∫ f dμ_ξ = ⟪ξ, f(a) ξ⟫.

instance ContinuousLinearMap.instIsFiniteMeasureElemComplexSpectrumIdDiagMeasure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] (ξ : H) : MeasureTheory.IsFiniteMeasure (a.diagMeasure ξ)

theorem ContinuousLinearMap.integral_diagMeasure_eq_inner_cfcHom {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] (ξ : H) (f : C(↑(spectrum ℂ a), ℂ)) : ∫ (x : ↑(spectrum ℂ a)), f x ∂a.diagMeasure ξ = inner ℂ ξ (((cfcHom inst✝) f) ξ)

Integration against the diagonal measure μ_ξ computes the diagonal matrix element of the continuous functional calculus: ∫ f dμ_ξ = ⟪ξ, f(a) ξ⟫.

theorem ContinuousLinearMap.integral_diagMeasure_eq_inner_cfc {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] (ξ : H) (f : ℂ → ℂ) (hf : ContinuousOn f (spectrum ℂ a) := by cfc_cont_tac) : ∫ (x : ↑(spectrum ℂ a)), f ↑x ∂a.diagMeasure ξ = inner ℂ ξ ((cfc f a) ξ)

The cfc form of integral_diagMeasure_eq_inner_cfcHom: for f continuous on the spectrum of a normal operator a, ∫ f dμ_ξ = ⟪ξ, cfc f a ξ⟫.

theorem ContinuousLinearMap.eq_diagMeasure_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] (ξ : H) (μ : MeasureTheory.Measure ↑(spectrum ℂ a)) [MeasureTheory.IsFiniteMeasure μ] : μ = a.diagMeasure ξ ↔ ∀ (f : C(↑(spectrum ℂ a), ℂ)), ∫ (x : ↑(spectrum ℂ a)), f x ∂μ = inner ℂ ξ (((cfcHom inst✝) f) ξ)

The diagonal measure μ_ξ is the unique finite measure on the spectrum of a normal operator a that represents f ↦ ⟪ξ, f(a) ξ⟫ on continuous functions.

@[simp]

theorem ContinuousLinearMap.diagMeasure_real_univ {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] (ξ : H) : (a.diagMeasure ξ).real Set.univ = ‖ξ‖ ^ 2

The total mass of the diagonal measure μ_ξ, as a real number, is ‖ξ‖².

@[simp]

theorem ContinuousLinearMap.diagMeasure_univ {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] (ξ : H) : (a.diagMeasure ξ) Set.univ = ‖ξ‖ₑ ^ 2

The total mass of the diagonal measure μ_ξ is ‖ξ‖².

theorem ContinuousLinearMap.integral_norm_sq_diagMeasure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] (ξ : H) (f : C(↑(spectrum ℂ a), ℂ)) : ∫ (x : ↑(spectrum ℂ a)), ‖f x‖ ^ 2 ∂a.diagMeasure ξ = ‖((cfcHom inst✝) f) ξ‖ ^ 2

The diagonal measure μ_ξ computes ‖f(a) ξ‖² as the squared L²(μ_ξ) norm of f: ∫ |f|² dμ_ξ = ‖f(a) ξ‖².