Finite-dimensional eigenspaces of compact operators

This file develops Riesz--Schauder input used for compact perturbations of Fredholm operators. A compact operator on a normed space has a finite-dimensional eigenspace at every nonzero scalar. More generally, every finite stage of the corresponding generalized eigenspace is finite dimensional.

The eigenspace proof restricts the compact operator to its eigenspace, where it is a nonzero scalar multiple of the identity. Compactness of that identity forces finite dimensionality. The generalized statement then uses the filtration by kernels of (T - μ)^n: the difference operator maps stage n + 1 into stage n, and its kernel embeds into the ordinary eigenspace.

Mathlib proves the eigenspace result as ContinuousLinearMap.finite_dimensional_eigenspace in the setting of complete inner-product spaces over RCLike fields. The argument used there needs neither an inner product nor completeness of the ambient space; the declarations below record it over arbitrary complete nontrivially normed fields, the generality required by Fredholm theory.

Main declarations

• IsCompactOperator.finiteDimensional_eigenspace: a nonzero eigenspace of a compact operator is finite dimensional.
• IsCompactOperator.finiteDimensional_genEigenspace_nat: every finite-order generalized eigenspace at a nonzero scalar is finite dimensional.

The mathematical argument is the finite-dimensional eigenspace step in the Riesz--Schauder theory; see, for example, Conway, A Course in Functional Analysis, Chapter VI, Section 5.

theorem IsCompactOperator.finiteDimensional_eigenspace {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {T : E →L[𝕜] E} {μ : 𝕜} (hT : IsCompactOperator ⇑T) (hμ : μ ≠ 0) : FiniteDimensional 𝕜 ↥(Module.End.eigenspace (↑T) μ)

A nonzero eigenspace of a compact operator on a normed space is finite dimensional.

Unlike Mathlib's ContinuousLinearMap.finite_dimensional_eigenspace, this needs no inner product and works over any complete nontrivially normed field.

theorem IsCompactOperator.finiteDimensional_genEigenspace_nat {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {T : E →L[𝕜] E} {μ : 𝕜} (hT : IsCompactOperator ⇑T) (hμ : μ ≠ 0) (n : ℕ) : FiniteDimensional 𝕜 ↥((Module.End.genEigenspace (↑T) μ) ↑n)

Every finite stage of the generalized eigenspace of a compact operator at a nonzero scalar is finite dimensional. In particular, compact operators have no infinite-dimensional finite-order Jordan block at a nonzero eigenvalue.