A range of finite codimension stays closed and of finite codimension under compact perturbations

Proved

FredholmBanach.compact_perturbation_coker

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 $F/\operatorname{Im}u$ is finite-dimensional and $h$ is compact (it maps some neighbourhood of $0$ into a compact set). Then $F/\operatorname{Im}(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 2 (TS III.73), for Banach spaces:
if the range of `u` has finite codimension and `h` is compact, then the range of `u + h` is
closed and of finite codimension. -/
theorem compact_perturbation_coker {𝕜 E F : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
    [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F]
    {u h : E →L[𝕜] F} (hc : FiniteDimensional 𝕜 (F ⧸ u.range)) (hh : IsCompactOperator h) :
    FiniteDimensional 𝕜 (F ⧸ (u + h).range) ∧ 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 2, p. TS III.73 (stated there for Fréchet spaces)

Read-back

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

Read-back: `FredholmBanach.compact_perturbation_coker`

Setting. $\mathbb{K}$ is $\mathbb{R}$ or $\mathbb{C}$ (RCLike). $E$ , $F$ are Banach spaces over $\mathbb{K}$ . $u, h : E \to F$ are bounded linear maps; $u+h$ is their sum.

Definitions used.

u.range $= u(E)$ , a linear subspace of $F$ . F ⧸ u.range is the algebraic quotient vector space $F/u(E)$ (no topology is involved in the finiteness hypothesis). FiniteDimensional 𝕜 (F ⧸ u.range) means $u(E)$ has finite codimension in $F$ .
IsCompactOperator h: some neighbourhood of $0$ in $E$ is mapped by $h$ into a compact subset of $F$ (the standard compact operator notion).
IsClosed ((u+h).range : Set F): the range of $u+h$ is a closed subset of $F$ .

Assertion. Assume

$F/u(E)$ is finite-dimensional (algebraic codimension of $u(E)$ finite),
$h$ is compact.

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

Note that closedness of $u(E)$ is not assumed, while closedness of $(u+h)(E)$ is concluded. (For bounded maps between Banach spaces, finite algebraic codimension of the range already forces the range to be closed, so the conclusion is consistent with the hypothesis, and the theorem in particular contains this fact for the case $h=0$ .)

No hypothesis on $\ker u$ ; this is the "lower semi-Fredholm" stability statement.

Degenerate cases / remarks.

If $F$ is finite-dimensional, the hypothesis is automatic and the conclusions are trivial.
If $E = 0$ then $u = h = 0$ and the hypothesis says $F$ is finite-dimensional.
With $h = 0$ the statement asserts: a bounded operator between Banach spaces whose range has finite algebraic codimension has closed range. This is a genuine (true) content, not a typo.
index is not used.

No mis-formalization detected.

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

A range of finite codimension stays closed and of finite codimension under compact perturbations

Read-back: FredholmBanach.compact_perturbation_coker

Read-back: `FredholmBanach.compact_perturbation_coker`