Spectral theory of compact operators

This file develops the spectral theory of compact operators on Banach spaces. The main result is the Fredholm alternative for compact operators.

Main results

• antilipschitz_of_not_hasEigenvalue: if T is a compact operator and μ ≠ 0 is not an eigenvalue, then T - μI is antilipschitz, i.e. bounded below.
• hasEigenvalue_or_mem_resolventSet: the Fredholm alternative for compact operators, which says that if T is a compact operator and μ ≠ 0, then either μ is an eigenvalue of T, or μ is in the resolvent set of T.
• hasEigenvalue_iff_mem_spectrum: if T is a compact operator, then the nonzero eigenvalues of T are exactly the nonzero points in the spectrum of T.

We follow the proof given in Section 2 of https://terrytao.wordpress.com/2011/04/10/a-proof-of-the-fredholm-alternative/ but adapt it to work in a more general setting of spaces over nontrivially normed fields, rather than just over ℝ or ℂ. The main technical hurdle is that we don't have the ability to rescale vectors to have norm exactly 1, so we have to work with vectors in a shell instead of on the unit sphere, and this makes some of the intermediate statements more complicated.

theorem IsCompactOperator.antilipschitz_of_not_hasEigenvalue {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {T : X →L[𝕜] X} {μ : 𝕜} (hT : IsCompactOperator ⇑T) (hμ : μ ≠ 0) (h : ¬Module.End.HasEigenvalue (↑T) μ) : ∃ (K : NNReal), AntilipschitzWith K ⇑(T - μ • 1)

If T : X →L[𝕜] X is a compact operator on a Banach space X, and μ ≠ 0 is not an eigenvalue of T, then T - μ • 1 is antilipschitz with positive constant. That is, T - μ • 1 is bounded below as an operator.

This is a useful step in the proof of the Fredholm alternative for compact operators.

theorem IsCompactOperator.hasEigenvalue_or_mem_resolventSet {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {T : X →L[𝕜] X} {μ : 𝕜} [CompleteSpace X] (hT : IsCompactOperator ⇑T) (hμ : μ ≠ 0) : Module.End.HasEigenvalue (↑T) μ ∨ μ ∈ resolventSet 𝕜 T

The Fredholm alternative for compact operators: if T is a compact operator and μ ≠ 0, then either μ is an eigenvalue of T, or μ is in the resolvent set of T. See also hasEigenvalue_iff_mem_spectrum, which says that the nonzero eigenvalues of a compact operator are exactly the nonzero points in the spectrum of the operator.

theorem IsCompactOperator.hasEigenvalue_iff_mem_spectrum {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {T : X →L[𝕜] X} {μ : 𝕜} [CompleteSpace X] (hT : IsCompactOperator ⇑T) (hμ : μ ≠ 0) : Module.End.HasEigenvalue (↑T) μ ↔ μ ∈ spectrum 𝕜 T

If T is a compact operator on a Banach space, then the nonzero eigenvalues of T are exactly the nonzero points in the spectrum of T. This is a consequence of the Fredholm alternative for compact operators.