Theorems · Theorem · operator theory

IsCompactOperator.antilipschitz_of_not_hasEigenvalue

∀ {𝕜 : Type u_1} {X : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {T : X →L[𝕜] X} {μ : 𝕜},
  IsCompactOperator ⇑T → μ ≠ 0 → ¬Module.End.HasEigenvalue (↑T) μ → ∃ K, AntilipschitzWith K ⇑(T - μ • 1)

If T : X →L[𝕜] X is a compact operator on a Banach space X, and μ ≠ 0 is not an eigenvalue of T, then T - μ • 1 is antilipschitz with positive constant. That is, T - μ • 1 is bounded below as an operator. This is a useful step in the proof of the Fredholm alternative for compact operators.

Defined in

Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative

Cited by

1 results in Mathlib

Foundations

Depth 180 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace