Spectrum of compact operators

TheoremEigenvectors for distinct eigenvalues are not in the span of earlier ones#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \(T\) be a bounded linear operator on \(E\), let \((\lambda_n)_{n \in \mathbb{N}}\) be pairwise distinct scalars in \(\mathbb{K}\), and let \((u_n)_{n \in \mathbb{N}}\) be nonzero vectors in \(E\) with \(T u_n = \lambda_n u_n\) for every \(n\). Then for every \(n\), the vector \(u_n\) does not lie in the linear span of \(\{u_i : i < n\}\).

This is the non-orthogonal replacement for the orthogonality of eigenspaces used in the self-adjoint case: it follows from the fact that the eigenspaces of a linear operator form an independent family.

theorem eigenvector_not_mem_span_prefix {T : E →L[𝕜] E} {lam : ℕ → 𝕜}
    (hinj : Function.Injective lam) {u : ℕ → E}
    (hu : ∀ n, T (u n) = lam n • u n) (hu_ne : ∀ n, u n ≠ 0) (n : ℕ) :
    u n ∉ Submodule.span 𝕜 (u '' Set.Iio n)

Used by 1

Used byFiniteness of eigenvalues of a compact operator bounded away from zero

TheoremAn operator acts as a scalar on a span of eigenvectors modulo a smaller span#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \(T\) be a bounded linear operator on \(E\), let \((\lambda_n)_{n \in \mathbb{N}}\) in \(\mathbb{K}\) and \((u_n)_{n \in \mathbb{N}}\) in \(E\) satisfy \(T u_n = \lambda_n u_n\) for every \(n\), and for each \(n\) let \(V_n\) be the linear span of \(\{u_i : i < n\}\). Then for every \(n\) and every \(y \in V_{n+1}\), we have \(T y - \lambda_n y \in V_n\).

The proof is induction on the span: each generator \(u_i\) with \(i < n\) contributes \((\lambda_i - \lambda_n) u_i\) and the generator \(u_n\) contributes \(0\).

theorem sub_mem_span_prefix {T : E →L[𝕜] E} {lam : ℕ → 𝕜} {u : ℕ → E}
    (hu : ∀ n, T (u n) = lam n • u n) {n : ℕ} {y : E}
    (hy : y ∈ Submodule.span 𝕜 (u '' Set.Iio (n + 1))) :
    T y - lam n • y ∈ Submodule.span 𝕜 (u '' Set.Iio n)

Used by 1

Used byFiniteness of eigenvalues of a compact operator bounded away from zero

TheoremInvariance of spans of eigenvectors#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \(T\) be a bounded linear operator on \(E\), and let \((\lambda_n)_{n \in \mathbb{N}}\) in \(\mathbb{K}\) and \((u_n)_{n \in \mathbb{N}}\) in \(E\) satisfy \(T u_n = \lambda_n u_n\) for every \(n\). Then for every \(n\) and every \(y\) in the linear span of \(\{u_i : i \le n\}\), the vector \(T y\) also lies in that span.

theorem map_mem_span_prefix {T : E →L[𝕜] E} {lam : ℕ → 𝕜} {u : ℕ → E}
    (hu : ∀ n, T (u n) = lam n • u n) {n : ℕ} {y : E}
    (hy : y ∈ Submodule.span 𝕜 (u '' Set.Iio (n + 1))) :
    T y ∈ Submodule.span 𝕜 (u '' Set.Iio (n + 1))

Used by 1

Used byFiniteness of eigenvalues of a compact operator bounded away from zero

TheoremRiesz separation for nested spans#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \((u_n)_{n \in \mathbb{N}}\) be vectors in \(E\), and for each \(n\) let \(V_n\) be the linear span of \(\{u_i : i < n\}\). Suppose \(u_n \notin V_n\) for every \(n\). Then for every \(n\) there is a vector \(y \in V_{n+1}\) with \(\|y\| = 1\) and \(\|y - z\| \ge 1/2\) for every \(z \in V_n\).

This is Riesz's lemma for the finite-dimensional, hence closed, subspace \(V_n\): one takes \(y\) to be the normalization of \(u_n - z\) for a \(z \in V_n\) almost realizing the distance \(d > 0\) from \(u_n\) to \(V_n\).

theorem exists_unit_vector_far {u : ℕ → E}
    (hnotmem : ∀ n, u n ∉ Submodule.span 𝕜 (u '' Set.Iio n)) (n : ℕ) :
    ∃ y : E, ‖y‖ = 1 ∧ y ∈ Submodule.span 𝕜 (u '' Set.Iio (n + 1)) ∧
      ∀ z ∈ Submodule.span 𝕜 (u '' Set.Iio n), (1 / 2 : ℝ) ≤ ‖y - z‖

Used by 1

Used byFiniteness of eigenvalues of a compact operator bounded away from zero

TheoremFiniteness of eigenvalues of a compact operator bounded away from zero#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \(T\) be a compact bounded linear operator on \(E\), and let \(\varepsilon > 0\) be real. Then the set of eigenvalues \(\mu \in \mathbb{K}\) of \(T\) with \(|\mu| \ge \varepsilon\) is finite.

If it were infinite, distinct eigenvalues \(\lambda_n\) with eigenvectors \(u_n\) would give, by Riesz separation for the spans of the \(u_n\), unit vectors \(y_n\) whose images \(T y_n\) are pairwise at distance at least \(\varepsilon / 2\), contradicting compactness of \(T\). No self-adjointness, inner product or completeness is needed.

theorem finite_eigenvalues_of_ge {T : E →L[𝕜] E}
    (hc : IsCompactOperator (T : E → E)) {ε : ℝ} (hε : 0 < ε) :
    Set.Finite {μ : 𝕜 | Module.End.HasEigenvalue (T.toLinearMap) μ ∧ ε ≤ ‖μ‖}

Uses 4 · Used by 1

Proof usesEigenvectors for distinct eigenvalues are not in the span of earlier ones · Riesz separation for nested spans · Invariance of spans of eigenvectors · An operator acts as a scalar on a span of eigenvectors modulo a smaller span

Used byEigenvalues of a compact operator tend to zero along any injective sequence

TheoremEigenvalues of a compact operator tend to zero along any injective sequence#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\) and let \(T\) be a compact bounded linear operator on \(E\). If \((\lambda_n)_{n \in \mathbb{N}}\) is a sequence of pairwise distinct eigenvalues of \(T\), then \(\lambda_n \to 0\) as \(n \to \infty\).

Otherwise some \(\varepsilon > 0\) would satisfy \(|\lambda_n| \ge \varepsilon\) for infinitely many \(n\), giving infinitely many eigenvalues of modulus at least \(\varepsilon\), which contradicts the finiteness of eigenvalues of a compact operator bounded away from zero.

theorem tendsto_eigenvalue_of_injective {T : E →L[𝕜] E}
    (hc : IsCompactOperator (T : E → E)) {lam : ℕ → 𝕜}
    (hinj : Function.Injective lam)
    (hlam : ∀ n, Module.End.HasEigenvalue (T.toLinearMap) (lam n)) :
    Tendsto lam atTop (𝓝 0)

Uses 1

Proof usesFiniteness of eigenvalues of a compact operator bounded away from zero

TheoremA compact operator on an infinite-dimensional space is not a unit#✓fully proved

If T is compact and E is infinite-dimensional, then T has no two-sided inverse among bounded operators. (Completeness of E is not needed for this statement.)

theorem not_isUnit_of_isCompactOperator (hInf : ¬ FiniteDimensional 𝕜 E)
    (T : E →L[𝕜] E) (hT : IsCompactOperator (T : E → E)) : ¬ IsUnit T

Used by 2

Used byA compact operator on an infinite-dimensional Banach space is not bijective · Zero lies in the spectrum of a compact operator on an infinite-dimensional space

TheoremA compact operator on an infinite-dimensional Banach space is not bijective#✓fully proved

Let \(E\) be an infinite-dimensional Banach space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\) and let \(T\) be a compact bounded linear operator on \(E\). Then \(T\) is not bijective.

By the bounded inverse theorem, a bijective bounded operator on a Banach space has a bounded inverse, so this follows from the fact that a compact operator on an infinite-dimensional space has no bounded two-sided inverse.

theorem not_bijective_of_isCompactOperator [CompleteSpace E]
    (hInf : ¬ FiniteDimensional 𝕜 E) (T : E →L[𝕜] E)
    (hT : IsCompactOperator (T : E → E)) : ¬ Function.Bijective T

Uses 1

Proof usesA compact operator on an infinite-dimensional space is not a unit

TheoremZero lies in the spectrum of a compact operator on an infinite-dimensional space#✓fully proved

Let \(E\) be an infinite-dimensional normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\) and let \(T\) be a compact bounded linear operator on \(E\). Then \(0\) lies in the spectrum of \(T\) in the algebra of bounded linear operators on \(E\); that is, \(T\) has no bounded two-sided inverse.

theorem zero_mem_spectrum_of_isCompactOperator (hInf : ¬ FiniteDimensional 𝕜 E)
    (T : E →L[𝕜] E) (hT : IsCompactOperator (T : E → E)) :
    (0 : 𝕜) ∈ spectrum 𝕜 T

Uses 1 · Used by 1

Proof usesA compact operator on an infinite-dimensional space is not a unit

Used bySpectrum of a finite-rank operator on an infinite-dimensional space

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.