The Borel functional calculus of a normal operator

Let a be a normal bounded operator on a complex Hilbert space H. Its continuous functional calculus cfcHom : C(spectrum ℂ a, ℂ) →⋆ₐ[ℂ] (H →L[ℂ] H) is a unital star representation of the continuous functions on the compact spectrum, so it has a projection-valued measure ProjValMeasure.ofRepresentation (cfcHom _). This is the spectral measure P of a, and integration against it is the Borel functional calculus

f ↦ f(a) = ∫ f dP,

a unital star algebra homomorphism from the bounded Borel functions on the spectrum to the bounded operators on H which extends the continuous functional calculus. Its value on the indicator of a Borel set B is the spectral projection P(B), and the coordinate function recovers a itself: this is the spectral theorem for bounded normal operators in its projection-valued form.

The spectral measure is the only projection-valued measure on the spectrum that recovers the continuous functional calculus (finite measures on the compact metrizable spectrum are regular, so no regularity hypothesis is needed), and it charges every nonempty relatively open subset of the spectrum. By the Fuglede–Putnam–Rosenblum theorem, an operator commutes with a iff it commutes with every spectral projection, equivalently with every value of the Borel calculus.

Main declarations

• ContinuousLinearMap.spectralPVM a: the spectral measure of a normal operator a.
• ContinuousLinearMap.borelCalculus a: the Borel functional calculus of a, the integral against a.spectralPVM.
• ContinuousLinearMap.borelCalculus_ofContinuousMap: the Borel calculus extends cfcHom.
• ContinuousLinearMap.borelCalculus_restrict_id: the coordinate function recovers a.
• ContinuousLinearMap.borelCalculus_indicator: indicators give the spectral projections.
• ContinuousLinearMap.eq_spectralPVM_iff: uniqueness of the spectral measure.
• ContinuousLinearMap.spectralPVM_proj_eq_zero_iff: the spectral measure has full support.
• ContinuousLinearMap.forall_commute_borelCalculus_iff, ContinuousLinearMap.forall_commute_spectralPVM_proj_iff: the spectral commutant.

References

• J. B. Conway, A Course in Functional Analysis, 2nd ed., Springer (1990), §IX.2.
• W. Rudin, Functional Analysis, 2nd ed., McGraw–Hill (1991), Theorems 12.23 and 12.24.

noncomputable def ContinuousLinearMap.spectralPVM {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] : TauCeti.ProjValMeasure (↑(spectrum ℂ a)) H

The spectral measure of a normal operator a: the projection-valued measure on its spectrum of the continuous functional calculus cfcHom.

noncomputable def ContinuousLinearMap.borelCalculus {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] : TauCeti.BoundedBorelFunction ↑(spectrum ℂ a) →⋆ₐ[ℂ] H →L[ℂ] H

The Borel functional calculus f ↦ f(a) of a normal operator a: integration of bounded Borel functions on the spectrum against the spectral measure of a.

@[simp]

theorem ContinuousLinearMap.integral_spectralPVM {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] : a.spectralPVM.integral = a.borelCalculus

Integration against the spectral measure is the Borel functional calculus.

theorem ContinuousLinearMap.spectralPVM_eq_ofRepresentation {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] : a.spectralPVM = TauCeti.ProjValMeasure.ofRepresentation (cfcHom inst✝)

The spectral measure is the projection-valued measure of cfcHom.

@[simp]

theorem ContinuousLinearMap.borelCalculus_ofContinuousMap {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] (f : C(↑(spectrum ℂ a), ℂ)) : a.borelCalculus (TauCeti.BoundedBorelFunction.ofContinuousMap f) = (cfcHom inst✝) f

The Borel calculus extends the continuous calculus. On a continuous function on the spectrum, the Borel functional calculus agrees with cfcHom.

@[simp]

theorem ContinuousLinearMap.spectralPVM_diag {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] (ξ : H) : a.spectralPVM.diag ξ = a.diagMeasure ξ

The diagonal measures of the spectral measure are the diagonal measures μ_ξ of a.

theorem ContinuousLinearMap.borelCalculus_ofContinuousMap_domRestrict {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] (f : ℂ → ℂ) (hf : ContinuousOn f (spectrum ℂ a) := by cfc_cont_tac) : a.borelCalculus (TauCeti.BoundedBorelFunction.ofContinuousMap { toFun := (spectrum ℂ a).domRestrict f, continuous_toFun := ⋯ }) = cfc f a

The cfc form of borelCalculus_ofContinuousMap: for f continuous on the spectrum, the Borel calculus of the restriction of f to the spectrum is cfc f a.

theorem ContinuousLinearMap.borelCalculus_restrict_id {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] : a.borelCalculus (TauCeti.BoundedBorelFunction.ofContinuousMap (ContinuousMap.restrict (spectrum ℂ a) (ContinuousMap.id ℂ))) = a

Spectral theorem for normal operators. The Borel calculus of the coordinate function on the spectrum is a itself, that is, a = ∫ z dP(z).

@[simp]

theorem ContinuousLinearMap.borelCalculus_indicator {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] {B : Set ↑(spectrum ℂ a)} (hB : MeasurableSet B) : a.borelCalculus ((TauCeti.BoundedBorelFunction.indicator B hB) 1) = a.spectralPVM.proj B hB

The Borel calculus of the indicator of a Borel set B is the spectral projection P(B).

theorem ContinuousLinearMap.inner_borelCalculus_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] (f : TauCeti.BoundedBorelFunction ↑(spectrum ℂ a)) (ξ : H) : inner ℂ ξ ((a.borelCalculus f) ξ) = ∫ (x : ↑(spectrum ℂ a)), f x ∂a.diagMeasure ξ

Diagonal matrix elements of the Borel calculus are integrals against the diagonal measures: ⟪ξ, f(a) ξ⟫ = ∫ f dμ_ξ.

theorem ContinuousLinearMap.norm_sq_borelCalculus_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] (f : TauCeti.BoundedBorelFunction ↑(spectrum ℂ a)) (ξ : H) : ‖(a.borelCalculus f) ξ‖ ^ 2 = ∫ (x : ↑(spectrum ℂ a)), ‖f x‖ ^ 2 ∂a.diagMeasure ξ

Vector norm identity for the Borel calculus: ‖f(a) ξ‖² = ∫ |f|² dμ_ξ.

theorem ContinuousLinearMap.norm_borelCalculus_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] {f : TauCeti.BoundedBorelFunction ↑(spectrum ℂ a)} {M : ℝ} (hM : 0 ≤ M) (hf : ∀ (x : ↑(spectrum ℂ a)), ‖f x‖ ≤ M) : ‖a.borelCalculus f‖ ≤ M

A bound ‖f x‖ ≤ M on the spectrum bounds the operator norm of f(a) by M.

theorem ContinuousLinearMap.norm_borelCalculus_apply_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] {f : TauCeti.BoundedBorelFunction ↑(spectrum ℂ a)} {M : ℝ} (hM : 0 ≤ M) (hf : ∀ (x : ↑(spectrum ℂ a)), ‖f x‖ ≤ M) (ξ : H) : ‖(a.borelCalculus f) ξ‖ ≤ M * ‖ξ‖

A bound ‖f x‖ ≤ M on the spectrum gives ‖f(a) ξ‖ ≤ M ‖ξ‖ for every vector ξ.

theorem ContinuousLinearMap.borelCalculus_congr_ae {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] {f g : TauCeti.BoundedBorelFunction ↑(spectrum ℂ a)} (h : ∀ (ξ : H), ⇑f =ᵐ[a.diagMeasure ξ] ⇑g) : a.borelCalculus f = a.borelCalculus g

Almost-everywhere invariance. Bounded Borel functions that agree almost everywhere for every diagonal measure μ_ξ of a have the same Borel calculus.

theorem ContinuousLinearMap.commute_borelCalculus_borelCalculus {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] (f g : TauCeti.BoundedBorelFunction ↑(spectrum ℂ a)) : Commute (a.borelCalculus f) (a.borelCalculus g)

Any two values of the Borel calculus of a commute.

theorem ContinuousLinearMap.forall_commute_spectralPVM_proj_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] (b : H →L[ℂ] H) : (∀ (B : Set ↑(spectrum ℂ a)) (hB : MeasurableSet B), Commute b (a.spectralPVM.proj B hB)) ↔ Commute b a

Spectral commutant. An operator commutes with every spectral projection of a normal operator a iff it commutes with a. One direction is the Fuglede–Putnam–Rosenblum theorem: an operator commuting with a also commutes with star a, hence with the continuous functional calculus of a.

theorem ContinuousLinearMap.forall_commute_borelCalculus_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] (b : H →L[ℂ] H) : (∀ (f : TauCeti.BoundedBorelFunction ↑(spectrum ℂ a)), Commute b (a.borelCalculus f)) ↔ Commute b a

Spectral commutant. An operator commutes with every value of the Borel calculus of a normal operator a iff it commutes with a.

theorem ContinuousLinearMap.commute_borelCalculus {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] (f : TauCeti.BoundedBorelFunction ↑(spectrum ℂ a)) : Commute a (a.borelCalculus f)

Every value of the Borel calculus of a commutes with a.

theorem ContinuousLinearMap.eq_spectralPVM_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] (P : TauCeti.ProjValMeasure (↑(spectrum ℂ a)) H) : P = a.spectralPVM ↔ ∀ (f : C(↑(spectrum ℂ a), ℂ)), P.integral (TauCeti.BoundedBorelFunction.ofContinuousMap f) = (cfcHom inst✝) f

Uniqueness of the spectral measure. A projection-valued measure on the spectrum of a normal operator a is its spectral measure iff integrating continuous functions against it gives the continuous functional calculus of a.

theorem ContinuousLinearMap.spectralPVM_proj_ne_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] {U : Set ↑(spectrum ℂ a)} (hU : IsOpen U) (hne : U.Nonempty) : a.spectralPVM.proj U ⋯ ≠ 0

Full support of the spectral measure. The spectral projection of a nonempty relatively open subset of the spectrum of a normal operator is nonzero.

theorem ContinuousLinearMap.spectralPVM_proj_eq_zero_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] {U : Set ↑(spectrum ℂ a)} (hU : IsOpen U) : a.spectralPVM.proj U ⋯ = 0 ↔ U = ∅

The spectral projection of a relatively open subset of the spectrum of a normal operator vanishes iff the subset is empty.