OAI/Analysis/LiebThirring/CompactAlternative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLiebThirring.OperatorProof.compact_perturbation_alternative line 13

   Source documentation

   The Fredholm alternative, transported through an arbitrary bounded isomorphism.

   lemma compact_perturbation_alternative {E : Type u190} [NormedAddCommGroup E]
       [NormedSpace ℂ E] [CompleteSpace E] (B : E ≃L[ℂ] E) (C : E →L[ℂ] E)
       (hC : IsCompactOperator C) :
       (∃ u : E, u ≠ 0 ∧ B u-C u = 0) ∨
         Function.Bijective (B.toContinuousLinearMap-C) := by
   …