The index under finite-rank perturbations of Fredholm operators

That a finite-rank perturbation of a Fredholm operator is again Fredholm is Mathlib's ContinuousLinearMap.IsFredholm.add_hasFiniteRange. This file records the corresponding index statement, which follows by restricting both operators to the kernel of the perturbation.

Finiteness of the rank is spelled with Mathlib's LinearMap.HasFiniteRange, matching the hypothesis of ContinuousLinearMap.IsFredholm.add_hasFiniteRange.

Main declarations

• ContinuousLinearMap.index_add_of_hasFiniteRange: over a complete nontrivially normed field, adding an operator of finite rank preserves the Fredholm index.

theorem ContinuousLinearMap.index_add_of_hasFiniteRange {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T K : E →L[𝕜] F} (hT : T.IsFredholm) (hK : (↑K).HasFiniteRange) : (T + K).index = T.index

Over a complete nontrivially normed field, perturbing a Fredholm operator by an operator of finite rank leaves its index unchanged: both operators restrict to the same map on the closed, finite-codimensional subspace ker K, and additivity of the index cancels the index shift of that restriction.