Prove2Me

Compact perturbations preserve the Fredholm property and the index

Proved
FredholmBanach.isFredholm_add_compact

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

banach-spacescompact-operatorsfredholm-operatorsfunctional-analysisoperator-theory

Let K\mathbb{K} be R\mathbb{R} or C\mathbb{C} and let EE, FF be Banach spaces over K\mathbb{K}. Let u:E→Fu:E\to F be a Fredholm operator and let h:E→Fh:E\to F be a compact operator (it maps some neighbourhood of 00 into a compact set). Then u+hu+h is a Fredholm operator and ind⁡(u+h)=ind⁡u\operatorname{ind}(u+h)=\operatorname{ind}u, where ind⁡u=dim⁡Ker⁡u−dim⁡(F/Im⁡u)\operatorname{ind}u=\dim\operatorname{Ker}u-\dim(F/\operatorname{Im}u).

Preamble
import Definitions.Def_FredholmBanach_Setting
Formal statement
namespace FredholmBanach

open Topology

/-- Bourbaki, *Théories spectrales*, III, § 5, n° 3, Théorème 3 (TS III.73), for Banach spaces:
if `u` is Fredholm and `h` is compact, then `u + h` is Fredholm and `ind (u + h) = ind u`. -/
theorem isFredholm_add_compact {𝕜 E F : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
    [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F]
    {u h : E →L[𝕜] F} (hu : u.IsFredholm) (hh : IsCompactOperator h) :
    (u + h).IsFredholm ∧ index (u + h) = index u := 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° 3, Théorème 3, p. TS III.73
Read-back

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

Read-back: FredholmBanach.isFredholm_add_compact

Setting. K\mathbb{K} is R\mathbb{R} or C\mathbb{C} (RCLike). EE, FF are Banach spaces over K\mathbb{K}. u,h:E→Fu, h : E \to F are bounded linear maps.

Definitions used.

  • u.IsFredholm (Mathlib structure, five fields): (i) uu is a strict map: the corestriction E→u(E)E \to u(E) is a topological quotient map; (ii) u(E)u(E) is closed; (iii) ker⁡u\ker u is finite-dimensional; (iv) the algebraic quotient F/u(E)F/u(E) is finite-dimensional (CoFG: finitely generated quotient); (v) ker⁡u\ker u admits a continuous linear projection E→ker⁡uE \to \ker u restricting to the identity on ker⁡u\ker u.
  • IsCompactOperator h: hh maps some neighbourhood of 00 into a compact set.
  • index u =dim⁡ker⁡u−dim⁡(F/u(E))= \dim \ker u - \dim(F/u(E)) as an integer, with finrank =0=0 on infinite-dimensional spaces (kernel minus cokernel; opposite sign to Bourbaki).

Assertion. If uu is Fredholm and hh is compact, then

  1. u+hu + h is Fredholm, and
  2. ind⁡(u+h)=ind⁡(u)\operatorname{ind}(u+h) = \operatorname{ind}(u).

Degenerate cases / remarks.

  • Both indices in (2) are of Fredholm maps (by (1)), so the junk value of index on non-Fredholm maps is never involved.
  • h=0h = 0: trivial. Finite-dimensional EE, FF: every map is Fredholm and both indices equal dim⁡E−dim⁡F\dim E - \dim F.
  • The sign convention does not matter for an equality of indices.
  • Every finite-rank bounded operator is compact, so this covers finite-rank perturbations too.

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