Finite-dimensional kernel and closed range survive compact perturbations

Proved

FredholmBanach.compact_perturbation_ker_range

by Mazecto · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

banach-spacescompact-operatorsfredholm-operatorsfunctional-analysisoperator-theory

Let $\mathbb{K}$ be $\mathbb{R}$ or $\mathbb{C}$ and let $E$ , $F$ be Banach spaces over $\mathbb{K}$ . Let $u,h:E\to F$ be bounded linear maps. Assume $\operatorname{Ker}u$ is finite-dimensional, $\operatorname{Im}u$ is closed in $F$ , and $h$ is compact (it maps some neighbourhood of $0$ into a compact set). Then $\operatorname{Ker}(u+h)$ is finite-dimensional and $\operatorname{Im}(u+h)$ is closed in $F$ .

Preamble

import Definitions.Def_FredholmBanach_Setting

Formal statement

namespace FredholmBanach

open Topology

/-- Bourbaki, *Théories spectrales*, III, § 5, n° 2, Théorème 1 (TS III.72), for Banach spaces:
if `u` has finite-dimensional kernel and closed range and `h` is compact, then `u + h` has
finite-dimensional kernel and closed range. -/
theorem compact_perturbation_ker_range {𝕜 E F : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
    [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F]
    {u h : E →L[𝕜] F} (hk : FiniteDimensional 𝕜 u.ker) (hr : IsClosed (u.range : Set F))
    (hh : IsCompactOperator h) :
    FiniteDimensional 𝕜 (u + h).ker ∧ IsClosed ((u + h).range : Set F) := by sorry

end FredholmBanach

Source

N. Bourbaki, Théories spectrales, Chapitres III à V, Springer (2023), https://doi.org/10.1007/978-3-031-19505-1, Chapitre III, § 5, n° 2, Théorème 1, p. TS III.72 (stated there for separated locally convex spaces and strict maps)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Read-back: `FredholmBanach.compact_perturbation_ker_range`

Setting. $\mathbb{K}$ is $\mathbb{R}$ or $\mathbb{C}$ (RCLike). $E$ , $F$ are Banach spaces over $\mathbb{K}$ (normed, complete). $u, h : E \to F$ are bounded linear maps (E →L[𝕜] F); $u + h$ is the pointwise sum.

Definitions used.

u.ker $=\{x \in E : u x = 0\}$ , u.range $= u(E)$ , as $\mathbb{K}$ -linear subspaces; FiniteDimensional 𝕜 u.ker means $\dim_{\mathbb{K}} \ker u < \infty$ .
IsClosed (u.range : Set F): $u(E)$ is a closed subset of $F$ .
IsCompactOperator h (Mathlib): there is a compact $K \subseteq F$ such that $h^{-1}(K)$ is a neighbourhood of $0$ in $E$ ; i.e. $h$ maps some neighbourhood of $0$ (equivalently, for a normed space, the unit ball) into a relatively compact set. This is the usual notion of compact operator.

Assertion. Assume

$\ker u$ is finite-dimensional,
$u(E)$ is closed in $F$ ,
$h$ is a compact operator.

Then $\ker(u+h)$ is finite-dimensional and $(u+h)(E)$ is closed in $F$ .

No assumption on the cokernel $F/u(E)$ and no Fredholm hypothesis; this is the "upper semi-Fredholm" stability statement.

Degenerate cases / remarks.

If $E$ is finite-dimensional, both conclusions are automatic (every subspace of finite dimension in a normed space is closed). If $F=0$ then $\ker u = E$ , so the hypothesis forces $E$ finite-dimensional.
If $h=0$ the statement is the hypothesis itself.
Completeness of $E$ and $F$ is assumed; the statement does not claim anything for incomplete spaces.
index is not used.

No mis-formalization detected; the statement matches the classical result that compact perturbations preserve "finite-dimensional kernel and closed range" between Banach spaces.

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Mazecto · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Finite-dimensional kernel and closed range survive compact perturbations

Read-back: FredholmBanach.compact_perturbation_ker_range

Read-back: `FredholmBanach.compact_perturbation_ker_range`