Spectral theory

Spectra and spectral theorems: self-adjoint, normal and compact self-adjoint spectral theorems, approximate and essential spectrum, numerical range and radius, Cayley transform, spectra of finite-rank and rank-one operators, almost Mathieu operator.

• Almost Mathieu operator
• Approximate point spectrum
• Cayley transform
• Ground-state energy of dilute Bose gases
• Numerical range and numerical radius
• Spectral theorem for bounded self-adjoint operators
• Spectral theorem for compact self-adjoint operators
• Spectrum of finite-rank operators
• Spectrum of rank-one operators
• Spectrum of self-adjoint operators

TheoremKrein–Rutman theorem for \(C(K)\)#✓fully proved

Let \(K\) be a compact Hausdorff space and let \(T\) be a compact bounded linear operator on the real Banach space \(C(K, \mathbb{R})\) of continuous real functions on \(K\) that is positive: \(Tf \ge 0\) pointwise whenever \(f \ge 0\) pointwise. Let \(r(T)\) be the spectral radius of \(T\), the supremum of \(|\lambda|\) over the real spectrum of \(T\). If \(r(T) > 0\), then there is a nonzero \(f \in C(K, \mathbb{R})\) with \(f \ge 0\) pointwise and \(Tf = r(T) f\).

theorem krein_rutman
    {K : Type*} [TopologicalSpace K] [CompactSpace K] [T2Space K]
    (T : C(K, ℝ) →L[ℝ] C(K, ℝ))
    (hT_compact : IsCompactOperator T)
    (hT_pos : ∀ f : C(K, ℝ), (∀ x, 0 ≤ f x) → ∀ x, 0 ≤ (T f) x)
    (hr : (0 : ℝ≥0∞) < spectralRadius ℝ T) :
    ∃ f : C(K, ℝ), f ≠ 0 ∧ (∀ x, 0 ≤ f x) ∧ T f = (spectralRadius ℝ T).toReal • f

Sources

• M. G. Krein and M. A. Rutman, Linear operators leaving invariant a cone in a Banach space, Uspekhi Mat. Nauk 3 (1948), 1–95, positive compact operator principal eigenvalue; Deimling, Nonlinear Functional Analysis; Lean states C(K, ℝ) compact positive case with spectralRadius eigenvector and nonnegativity.

TheoremSpectral theorem for compact normal operators#✓fully proved

Let \(E\) be a complex Hilbert space and \(T\) a compact normal operator on \(E\). Then there are a Hilbert basis \((b_i)_{i \in I}\) of \(E\) and complex numbers \((\mu_i)_{i \in I}\) such that \(T b_i = \mu_i b_i\) for every \(i\), and the eigenvalues vanish at infinity: for every \(\varepsilon > 0\) the set of \(i\) with \(|\mu_i| \ge \varepsilon\) is finite.

theorem compactNormal_hilbertBasis
    {E : Type uE} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]
    (T : E →L[ℂ] E) (hT_compact : IsCompactOperator T)
    (hT_normal : IsStarNormal T) :
    ∃ (ι : Type uE) (b : HilbertBasis ι ℂ E) (μ : ι → ℂ),
      (∀ ε > (0 : ℝ), Set.Finite { i | ε ≤ ‖μ i‖ }) ∧
      (∀ i, T (b i) = μ i • b i)

Sources

• Compact normal spectral theorem, Hilbert-Schmidt and Riesz 1910s; Reed-Simon I; Rudin Functional Analysis; Lean states complex Hilbert compact IsStarNormal case with same finite-level-set vanishing condition and same-universe index.

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.