Stability of Fredholm operators under small perturbations

This file proves that Fredholm operators from a Banach space to a normed space form an open set in the operator norm topology and that their index is locally constant. Equivalently, every Fredholm operator T has an ε > 0 such that any operator S with ‖S - T‖ < ε is Fredholm and has the same index.

The proof uses Mathlib's ContinuousLinearMap.FredholmPackage. In the resulting block decomposition, the corner between the essential domain and codomain summands is an equivalence for T, and remains an equivalence in a neighbourhood of T because continuous linear equivalences form an open subset of the operator space. Elementary block elimination then reduces a nearby operator to the product of that invertible corner with a map between the two finite-dimensional summands. The openness input is Mathlib's ContinuousLinearEquiv.isOpen; no implementation is vendored.

Main declarations

• ContinuousLinearMap.IsFredholm.eventually_isFredholm_and_index_eq: Fredholmness and the index are stable in a neighbourhood of a Fredholm operator.
• ContinuousLinearMap.IsFredholm.exists_pos_isFredholm_and_index_eq_of_norm_sub_lt: the corresponding operator-norm ε statement.
• TauCeti.isOpen_setOf_isFredholm: Fredholm operators form an open set.
• TauCeti.isOpen_setOf_isFredholm_index_eq: Fredholm operators of a fixed index form an open set.

The argument follows McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Appendix A.1, and supplies the small-perturbation stability target in Lane F0 of the analytic Heegaard Floer roadmap.

theorem ContinuousLinearMap.IsFredholm.eventually_isFredholm_and_index_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (hT : T.IsFredholm) : ∀ᶠ (S : E →L[𝕜] F) in nhds T, S.IsFredholm ∧ S.index = T.index

Fredholmness and the Fredholm index are stable in a neighbourhood of a Fredholm operator.

theorem ContinuousLinearMap.IsFredholm.exists_pos_isFredholm_and_index_eq_of_norm_sub_lt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (hT : T.IsFredholm) : ∃ ε > 0, ∀ (S : E →L[𝕜] F), ‖S - T‖ < ε → S.IsFredholm ∧ S.index = T.index

A sufficiently small operator-norm perturbation of a Fredholm operator is Fredholm with the same index.

theorem TauCeti.isOpen_setOf_isFredholm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] : IsOpen {T : E →L[𝕜] F | T.IsFredholm}

The set of Fredholm operators from a Banach space to a normed space is open in the operator norm topology.

theorem TauCeti.isOpen_setOf_isFredholm_index_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℤ) : IsOpen {T : E →L[𝕜] F | T.IsFredholm ∧ T.index = n}

For every integer n, the set of Fredholm operators of index n is open in the operator norm topology.