Fredholm

Results named in Tau Ceti's TauCeti.Analysis.Fredholm modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremAtkinson's theorem#

an operator between Banach spaces is Fredholm if and only if it is invertible modulo compact operators.

TauCeti.isFredholm_iff_exists_isCompactOperator_comp_sub_one.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {T : E →L[𝕜] F} :
  T.IsFredholm ↔ ∃ S, IsCompactOperator ⇑(S ∘SL T - 1) ∧ IsCompactOperator ⇑(T ∘SL S - 1)

Lean

Formalized in Tau Ceti as TauCeti.isFredholm_iff_exists_isCompactOperator_comp_sub_one.

Other forms

Atkinson's theorem, parametrix direction. Formalized in Tau Ceti as ContinuousLinearMap.IsFredholm.of_isCompactOperator_comp_sub_one.

ContinuousLinearMap.IsFredholm.of_isCompactOperator_comp_sub_one.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {T : E →L[𝕜] F} {S : F →L[𝕜] E}
  (hST : IsCompactOperator ⇑(S ∘SL T - 1)) (hTS : IsCompactOperator ⇑(T ∘SL S - 1)) : T.IsFredholm

Sources

• Tau Ceti documentation: TauCeti.isFredholm_iff_exists_isCompactOperator_comp_sub_one
• Source of TauCeti.isFredholm_iff_exists_isCompactOperator_comp_sub_one in TauCeti/Analysis/Fredholm/CompactPerturbation.lean

LeanTauCeti.isFredholm_iff_exists_isCompactOperator_comp_sub_one · ContinuousLinearMap.IsFredholm.of_isCompactOperator_comp_sub_one

Uses 1

Proof usesRiesz--Schauder

TheoremRiesz--Schauder#

Riesz--Schauder, in the form in which compact perturbations of the identity arise below.

TauCeti.isFredholm_one_add.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜]
  [IsRCLikeNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [CompleteSpace E] {K : E →L[𝕜] E} (hK : IsCompactOperator ⇑K) : (1 + K).IsFredholm

Lean

Formalized in Tau Ceti as TauCeti.isFredholm_one_add.

Other forms

Riesz--Schauder. Formalized in Tau Ceti as TauCeti.isFredholm_one_sub.

TauCeti.isFredholm_one_sub.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜]
  [IsRCLikeNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [CompleteSpace E] {K : E →L[𝕜] E} (hK : IsCompactOperator ⇑K) : (1 - K).IsFredholm

Sources

• Tau Ceti documentation: TauCeti.isFredholm_one_add
• Source of TauCeti.isFredholm_one_add in TauCeti/Analysis/Fredholm/CompactPerturbation.lean

LeanTauCeti.isFredholm_one_add · TauCeti.isFredholm_one_sub

Uses 1 · Used by 1

Proof usesRiesz's lemma, translated form

Used byAtkinson's theorem

TheoremSchwartz's lemma#

A compact perturbation of a surjection between real or complex Banach spaces has finite-dimensional cokernel, without any hypothesis on its kernel.

ContinuousLinearMap.cofg_range_add_of_surjective_of_isCompactOperator.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (T K : E →L[𝕜] F)
  (hT : Function.Surjective ⇑T) (hK : IsCompactOperator ⇑K) : (↑(T + K)).range.CoFG

Lean

Formalized in Tau Ceti as ContinuousLinearMap.cofg_range_add_of_surjective_of_isCompactOperator.

Sources

• Tau Ceti documentation: ContinuousLinearMap.cofg_range_add_of_surjective_of_isCompactOperator
• Source of ContinuousLinearMap.cofg_range_add_of_surjective_of_isCompactOperator in TauCeti/Analysis/Fredholm/Schwartz.lean

LeanContinuousLinearMap.cofg_range_add_of_surjective_of_isCompactOperator

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.