Chapter 16: Spectral Theory of Bounded Operators

This file formalizes Propositions 16.1, 16.2, and 16.3 from Chapter 16 on the spectral theory of bounded linear operators on Hilbert spaces.

Main results

• prop_16_1 — Proposition 16.1 (Goal 110): The spectrum of a bounded linear operator on a Hilbert space is a compact subset of {|z| ≤ ‖T‖}.
• prop_16_2 — Proposition 16.2 (Goal 111): For a bounded self-adjoint operator A with m = inf_{‖φ‖=1}⟨Aφ, φ⟩ and M = sup_{‖φ‖=1}⟨Aφ, φ⟩, {m, M} ⊆ spec(A) ⊆ [m, M].
• prop_16_3 — Proposition 16.3 (Goal 112): For a bounded self-adjoint operator A and a real polynomial p, ‖p(A)‖ ≤ sup_{t ∈ [m,M]} |p(t)|.

References

These results are standard in the spectral theory of bounded operators on Hilbert spaces; see e.g. Reed and Simon, Methods of Modern Mathematical Physics I: Functional Analysis, Chapter VII.

Numerical range infrastructure

def innerQuadForm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : H →L[ℂ] H) (φ : H) : ℝ

The quadratic form φ ↦ Re⟨Aφ, φ⟩ for a bounded linear operator A on a complex Hilbert space H. For a self-adjoint operator, the imaginary part vanishes and this equals ⟨Aφ, φ⟩ viewed as a real number.

noncomputable def numericalRangeInf {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : H →L[ℂ] H) : ℝ

m(A) = inf_{‖φ‖=1} Re⟨Aφ, φ⟩, the infimum of the numerical range restricted to the unit sphere. For a self-adjoint operator, this is the bottom of the spectrum.

noncomputable def numericalRangeSup {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : H →L[ℂ] H) : ℝ

M(A) = sup_{‖φ‖=1} Re⟨Aφ, φ⟩, the supremum of the numerical range restricted to the unit sphere. For a self-adjoint operator, this is the top of the spectrum.

Proposition 16.1 (Goal 110)

theorem prop_16_1_isCompact {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (T : H →L[ℂ] H) : IsCompact (spectrum ℂ T)

The spectrum of a bounded linear operator on a Hilbert space is compact. This is the first part of Proposition 16.1.

theorem prop_16_1_subset_closedBall {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (T : H →L[ℂ] H) : spectrum ℂ T ⊆ Metric.closedBall 0 ‖T‖

The spectrum of a bounded linear operator is contained in the closed ball of radius ‖T‖. This is the second part of Proposition 16.1.

theorem prop_16_1 {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (T : H →L[ℂ] H) : IsCompact (spectrum ℂ T) ∧ spectrum ℂ T ⊆ Metric.closedBall 0 ‖T‖

Goal 110: Proposition 16.1: For any bounded linear operator T on a Hilbert space H, the spectrum σ(T) ⊂ ℂ is a compact subset of the closed ball {z : ℂ | ‖z‖ ≤ ‖T‖}.

Proposition 16.2 (Goal 111)

theorem prop_16_2 {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (A : H →L[ℂ] H) (hA : IsSelfAdjoint A) : have m := numericalRangeInf A; have M := numericalRangeSup A; {↑m, ↑M} ⊆ spectrum ℂ A ∧ spectrum ℂ A ⊆ Complex.ofReal '' Set.Icc m M

Goal 111: Proposition 16.2: If A is a bounded self-adjoint operator on a Hilbert space H, then with m = inf_{‖φ‖=1} ⟨Aφ, φ⟩ and M = sup_{‖φ‖=1} ⟨Aφ, φ⟩, the spectrum satisfies {m, M} ⊆ σ(A) ⊆ [m, M] (where [m, M] is embedded in ℂ via the canonical inclusion ℝ ↪ ℂ). The proof is not given in the text.

Proposition 16.3 (Goal 112)

theorem prop_16_3 {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (A : H →L[ℂ] H) (hA : IsSelfAdjoint A) (p : Polynomial ℝ) (hp : p ≠ 0) : have m := numericalRangeInf A; have M := numericalRangeSup A; ‖(Polynomial.aeval A) p‖ ≤ sSup ((fun (t : ℝ) => |Polynomial.eval t p|) '' Set.Icc m M)

Goal 112: Proposition 16.3: If A is a bounded self-adjoint operator on a Hilbert space and p is a nonzero real polynomial, then p(A) = Σᵢ cᵢ Aⁱ satisfies ‖p(A)‖ ≤ sup_{t ∈ [m, M]} |p(t)|, where m and M are as in Proposition 16.2. The proof is not given in the text.