Riesz theory for compact perturbations of the identity

Let K be a compact operator on a Banach space X and write A = 1 - K. This file proves the three finiteness facts that make A a Fredholm operator: its kernel is finite dimensional, its range is closed, and its cokernel is finite dimensional. Together they are the operator-theoretic half of the Riesz--Schauder theory, and they are what upgrades Mathlib's spectral Fredholm alternative for compact operators to a statement about Fredholm operators.

Compactness enters the three arguments in different forms: the kernel argument uses the existing finite-dimensional eigenspace theorem, the range argument extracts a convergent subsequence with IsCompactOperator.exists_subseq_tendsto, and the cokernel argument uses the separation consequence IsCompactOperator.exists_dist_lt_of_norm_le.

• The kernel is the 1-eigenspace of K, already known to be finite dimensional.
• For the range, split off a closed complement M of ker A, which exists because ker A is finite dimensional. On M the operator A is bounded below: otherwise a sequence in a fixed norm shell with A xₙ → 0 would, along a subsequence on which K converges, converge to a nonzero element of ker A ⊓ M. A bounded-below map on a complete space has closed range.
• For the cokernel, run the classical Riesz argument on the decreasing chain of ranges range A ⊇ range A² ⊇ ⋯. Each Aⁿ is again 1 minus a compact operator, so each of these ranges is closed, and Riesz's lemma would otherwise produce a separated bounded sequence. Once the chain stabilises at p, the finite-dimensional ker (A ^ p) and range (A ^ p) ≤ range A together span X, so ker (A ^ p) surjects onto the cokernel.

Main declarations

• IsCompactOperator.exists_pos_mul_norm_le_of_disjoint_ker: 1 - K is bounded below on any closed subspace meeting its kernel trivially.
• IsCompactOperator.finiteDimensional_ker_one_sub: ker (1 - K) is finite dimensional.
• IsCompactOperator.isClosed_range_one_sub: range (1 - K) is closed.
• IsCompactOperator.isCompactOperator_one_sub_pow: 1 - (1 - K) ^ n is compact, so every power of 1 - K is again a compact perturbation of the identity. This holds for any continuous endomorphism of a topological module.
• IsCompactOperator.finiteDimensional_quotient_range_one_sub: X ⧸ range (1 - K) is finite dimensional.

The argument is the classical Riesz theory of compact operators; see, for example, Conway, A Course in Functional Analysis, Chapter VI, Section 5, or Rudin, Functional Analysis, Chapter 4.

theorem IsCompactOperator.isCompactOperator_one_sub_pow {R : Type u_1} {M : Type u_2} [Ring R] [TopologicalSpace M] [AddCommGroup M] [IsTopologicalAddGroup M] [Module R M] {K : M →L[R] M} (hK : IsCompactOperator ⇑K) (n : ℕ) : IsCompactOperator ⇑(1 - (1 - K) ^ n)

Every power of a compact perturbation of the identity is again a compact perturbation of the identity.

theorem IsCompactOperator.exists_pos_mul_norm_le_of_disjoint_ker {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {K : X →L[𝕜] X} (hK : IsCompactOperator ⇑K) {M : Submodule 𝕜 X} (hM : IsClosed ↑M) (hdisj : Disjoint (↑(1 - K)).ker M) : ∃ (c : ℝ), 0 < c ∧ ∀ x ∈ M, c * ‖x‖ ≤ ‖(1 - K) x‖

On a closed subspace M meeting ker (1 - K) only in 0, the operator 1 - K is bounded below.

theorem IsCompactOperator.finiteDimensional_ker_one_sub {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {K : X →L[𝕜] X} [CompleteSpace 𝕜] (hK : IsCompactOperator ⇑K) : FiniteDimensional 𝕜 ↥(↑(1 - K)).ker

The kernel of a compact perturbation of the identity is finite dimensional.

theorem IsCompactOperator.isClosed_range_one_sub {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {K : X →L[𝕜] X} [CompleteSpace 𝕜] [IsRCLikeNormedField 𝕜] [CompleteSpace X] (hK : IsCompactOperator ⇑K) : IsClosed ↑(↑(1 - K)).range

The range of a compact perturbation of the identity is closed.

theorem IsCompactOperator.finiteDimensional_quotient_range_one_sub {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {K : X →L[𝕜] X} [CompleteSpace 𝕜] [IsRCLikeNormedField 𝕜] [CompleteSpace X] (hK : IsCompactOperator ⇑K) : FiniteDimensional 𝕜 (X ⧸ (↑(1 - K)).range)

The cokernel of a compact perturbation of the identity is finite dimensional.