The set of Fredholm operators is open, and the index is locally constant

In this file, we show two closely related results about Fredholm operators between two Banach spaces:

• isOpen_setOfPred_isFredholm: the set of Fredholm operators is open (for the operator norm) in the space of continuous linear maps;
• index_continuousOn_isFredholm: the integer-valued map T ↦ T.index is continuous (i.e locally constant) on this open subset.

TODO

With a bit more work, we could also show that, for any choice of a quasi-inverse S₀ to a Fredholm operator T₀, there is a function φ : (E →L[𝕜] F) → (F →L[𝕜] E) which is analytic on a neighborhood of T₀, such that φ(T₀) = S₀ and φ(T) is a quasi-inverse of T for every T in a neighborhood of T₀.

theorem ContinuousLinearMap.FredholmPackage.eventually_nhds_isInvertible {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] [CompleteSpace E] {T₀ : E →L[𝕜] F} (pkg : T₀.FredholmPackage) : ∀ᶠ (T : E →L[𝕜] F) in nhds T₀, (pkg.decCodom.proj ∘SL T ∘SL pkg.decDom.X₁.subtypeL).IsInvertible

Let T₀ : E → F be a Fredholm operator between two Banach spaces, and choose a FredholmPackage for T₀; that is, fix topological decompositions E = E₁ ⊕ E₀ and F = F₁ ⊕ F₀, where E₀ and F₀ are finite dimensional, and such that in these decompositions we have $T₀ = \begin{pmatrix} α₀ & 0 \cr 0 & 0 \end{pmatrix}$ with α₀ invertible.

Then, for $T = \begin{pmatrix} α & β \cr γ & δ \end{pmatrix}$ close enough to T₀ (in operator norm), we have that α is invertible.

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

If T₀ is a Fredholm operator between two Banach spaces, then every operator T close enough to T₀ (in operator norm) is also Fredholm.

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

The set of Fredholm operators between two Banach spaces is open (for the operator norm) in the space of continuous linear maps.

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

If T₀ is a Fredholm operator between two Banach spaces, then every operator T close enough to T₀ (in operator norm) has the same index as T₀.

theorem ContinuousLinearMap.IsFredholm.index_continuousAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] [CompleteSpace E] [CompleteSpace 𝕜] {T₀ : E →L[𝕜] F} (hT₀ : T₀.IsFredholm) : ContinuousAt (fun (T : E →L[𝕜] F) => (↑T).index) T₀

If T₀ is a Fredholm operator between two Banach spaces, then the integer-valued map T ↦ T.index is continuous at T₀.

theorem ContinuousLinearMap.index_continuousOn_isFredholm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] [CompleteSpace E] [CompleteSpace 𝕜] : ContinuousOn (fun (T : E →L[𝕜] F) => (↑T).index) {T : E →L[𝕜] F | T.IsFredholm}

The integer-valued map T ↦ T.index is continuous (i.e locally constant) on the set of Fredholm operators between two Banach spaces..