Spectral theorem for bounded self-adjoint operators

TheoremScalar spectral measure of a vector#✓fully proved

Let \(E\) be a complex Hilbert space, \(T\) a bounded self-adjoint operator on \(E\) and \(v \in E\). There is a finite regular measure \(\mu\) on the spectrum \(\sigma(T) \subseteq \mathbb{C}\) of \(T\) such that for every continuous function \(f : \sigma(T) \to \mathbb{R}\), \(\int_{\sigma(T)} f \, d\mu = \operatorname{Re} \langle f(T) v, v \rangle\), where \(f(T)\) is the continuous functional calculus of \(T\) applied to \(f\) viewed as a complex-valued function.

The measure lives on the complex spectrum. Its support is real because the spectrum of a self-adjoint operator is real.

theorem IsSelfAdjoint.exists_spectralMeasure
    {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]
    (T : E →L[ℂ] E) (hT : IsSelfAdjoint T) (v : E) :
    ∃ μ : Measure (spectrum ℂ T), IsFiniteMeasure μ ∧ μ.Regular ∧
      ∀ f : C(spectrum ℂ T, ℝ),
        ∫ z, f z ∂μ = Complex.re (inner ℂ ((cfcHom hT.isStarNormal)
          (⟨fun z => (f z : ℂ), Complex.continuous_ofReal.comp f.continuous⟩ :
            C(spectrum ℂ T, ℂ)) v) v)

Used by 1

Used bySpectral theorem for bounded self-adjoint operators, multiplication form

TheoremSpectral theorem for bounded self-adjoint operators, multiplication form#✓fully proved

Let \(E\) be a complex Hilbert space and \(T\) a bounded self-adjoint operator on \(E\). Then there are a measure space \((X, \mu)\), a measurable function \(\varphi : X \to \mathbb{R}\) and a linear isometric isomorphism \(U\) of \(E\) onto \(L^2(X, \mu; \mathbb{C})\) such that for every \(x \in E\), \(U(Tx)(a) = \varphi(a)\,(Ux)(a)\) for \(\mu\)-almost every \(a \in X\).

Proof: Scalar measures from the continuous functional calculus identify each cyclic subspace with an \(L^2\) space. A maximal orthogonal family of cyclic subspaces is then assembled over a disjoint-union measure, where the spectral coordinate acts by multiplication.

theorem boundedSelfAdjoint_spectral_multiplication
    {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]
    (T : E →L[ℂ] E) (hT : IsSelfAdjoint T) :
    ∃ (X : Type u) (_ : MeasurableSpace X) (μ : Measure X) (φ : X → ℝ) (_ : Measurable φ)
      (U : E ≃ₗᵢ[ℂ] Lp ℂ 2 μ),
      ∀ x, ∀ᵐ a ∂μ, U (T x) a = (φ a : ℂ) * U x a

Sources

W. Rudin, Functional Analysis, 2nd ed., Ch. 12.

Uses 1

Proof usesScalar spectral measure of a vector

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.