Spectral theorem for compact self-adjoint operators

TheoremEigenvalues are bounded by the operator norm#✓fully proved

Let \(T\) be a bounded linear operator on an inner product space over \(\mathbb{R}\) or \(\mathbb{C}\). Every eigenvalue \(\mu\) of \(T\) satisfies \(|\mu| \le \|T\|\).

Indeed, if \(Tx = \mu x\) with \(x \neq 0\), then \(|\mu| \, \|x\| = \|Tx\| \le \|T\| \, \|x\|\).

theorem norm_hasEigenvalue_le {T : H →L[𝕜] H} {μ : 𝕜}
    (hμ : Module.End.HasEigenvalue (T : H →ₗ[𝕜] H) μ) : ‖μ‖ ≤ ‖T‖

TheoremFiniteness of large eigenvalues of a compact self-adjoint operator#✓fully proved

Let \(T\) be a compact self-adjoint operator on a Hilbert space over \(\mathbb{R}\) or \(\mathbb{C}\). For every \(\varepsilon > 0\), the set of eigenvalues \(\mu\) of \(T\) with \(\varepsilon \le |\mu|\) is finite.

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

Used by 3

Used byFinite-rank approximation of compact self-adjoint operators · Maximum principle for compact self-adjoint operators · Maximum principle as a sequence in infinite dimension

TheoremA nonzero compact self-adjoint operator has an eigenvalue of modulus equal to its norm#✓fully proved

Let \(T \neq 0\) be a compact self-adjoint operator on a Hilbert space \(H\) over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\). Then \(T\) has an eigenvalue \(\mu \in \mathbb{K}\) with \(\mu \neq 0\) and \(|\mu| = \|T\|\), where \(\|T\|\) is the operator norm of \(T\).

theorem exists_hasEigenvalue_norm_eq (T : H →L[𝕜] H) (hT : IsSelfAdjoint T)
    (hc : IsCompactOperator (T : H → H)) (hT0 : T ≠ 0) :
    ∃ μ : 𝕜, μ ≠ 0 ∧ ‖μ‖ = ‖T‖ ∧ Module.End.HasEigenvalue (T : Module.End 𝕜 H) μ

Used by 2

Used byFinite-rank approximation of compact self-adjoint operators · A nonzero compact self-adjoint operator has a real eigenvalue of modulus equal to its norm, with a unit eigenvector

TheoremA nonzero compact self-adjoint operator has a real eigenvalue of modulus equal to its norm, with a unit eigenvector#✓fully proved

A nonzero compact self-adjoint operator has a real eigenvalue of modulus equal to its norm, with a unit eigenvector. Let \(T \neq 0\) be a compact self-adjoint operator on a Hilbert space \(H\) over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\). Then there are a real number \(r\) and a unit vector \(u \in H\) with \(T u = r u\) and \(|r| = \|T\|\), where \(\|T\|\) is the operator norm of \(T\).

theorem exists_unit_eigenvector_real_eigenvalue (T : H →L[𝕜] H) (hT : IsSelfAdjoint T)
    (hc : IsCompactOperator (T : H → H)) (hT0 : T ≠ 0) :
    ∃ r : ℝ, ∃ u : H, ‖u‖ = 1 ∧ T u = (r : 𝕜) • u ∧ |r| = ‖T‖

Uses 1 · Used by 1

Proof usesA nonzero compact self-adjoint operator has an eigenvalue of modulus equal to its norm

Used byDeflation step

TheoremDeflation step#✓fully proved

Let \(T\) be a compact self-adjoint operator on a Hilbert space \(H\) over \(\mathbb{R}\) or \(\mathbb{C}\), let \(S\) be a linear subspace of \(H\) that admits an orthogonal projection \(P : H \to H\) onto \(S\) and satisfies \(T(S) \subseteq S\), and let \(T_1 = PTP\) be the compression of \(T\) to \(S\). If \(T_1 \neq 0\), then there are a real number \(r\) and a unit vector \(v \in S\) with \(Tv = rv\), \(|r| = \|T_1\|\) and \(|r| \le \|T\|\).

theorem exists_next_eigenvector_of_invariant {S : Submodule 𝕜 H} [S.HasOrthogonalProjection]
    {T : H →L[𝕜] H} (hT : IsSelfAdjoint T) (hc : IsCompactOperator (T : H → H))
    (hS : ∀ x ∈ S, T x ∈ S)
    (hT₁ : S.starProjection ∘L T ∘L S.starProjection ≠ 0) :
    ∃ r : ℝ, ∃ v : H, ‖v‖ = 1 ∧ v ∈ S ∧ T v = (r : 𝕜) • v ∧
      |r| = ‖S.starProjection ∘L T ∘L S.starProjection‖ ∧ |r| ≤ ‖T‖

Uses 1 · Used by 3

Proof usesA nonzero compact self-adjoint operator has a real eigenvalue of modulus equal to its norm, with a unit eigenvector

Used byNext eigenvalue after a finite family of eigenvectors · Maximum principle for compact self-adjoint operators · Maximum principle as a sequence in infinite dimension

TheoremNext eigenvalue after a finite family of eigenvectors#✓fully proved

Let \(T\) be a compact self-adjoint operator on a Hilbert space \(H\) over \(\mathbb{R}\) or \(\mathbb{C}\), let \(u_1, \dots, u_n \in H\) and scalars \(\mu_1, \dots, \mu_n\) satisfy \(T u_i = \mu_i u_i\) for every \(i\), and let \(S\) be the orthogonal complement of the span of \(u_1, \dots, u_n\). If \(Tz \neq 0\) for some \(z \in S\), then there are a real number \(r\) and a unit vector \(v\) with \(\langle v, u_i \rangle = 0\) for every \(i\), \(Tv = rv\) and \(\langle Tv, v \rangle = r\), such that \(|\langle Tx, x \rangle| \le |r|\) for every unit vector \(x \in S\). In particular \(v \in S\), so \(|r|\) is the maximum of \(|\langle Tx, x \rangle|\) over unit vectors \(x \in S\).

The vectors \(u_i\) need not be orthonormal, or even nonzero.

theorem exists_next_eigenvector_of_finite_eigenvectors
    {n : ℕ} {u : Fin n → H} {μ : Fin n → 𝕜} {T : H →L[𝕜] H}
    (hT : IsSelfAdjoint T) (hc : IsCompactOperator (T : H → H))
    (hμ : ∀ i, T (u i) = μ i • u i)
    (hne : ∃ z ∈ (Submodule.span 𝕜 (Set.range u))ᗮ, T z ≠ 0) :
    ∃ r : ℝ, ∃ v : H,
      ‖v‖ = 1 ∧
      (∀ i, ⟪v, u i⟫_𝕜 = 0) ∧
      T v = (r : 𝕜) • v ∧
      (∀ x ∈ (Submodule.span 𝕜 (Set.range u))ᗮ, ‖x‖ = 1 →
        ‖⟪T x, x⟫_𝕜‖ ≤ |r|) ∧
      ⟪T v, v⟫_𝕜 = (r : 𝕜)

Uses 1

Proof usesDeflation step

TheoremFinite-rank approximation of compact self-adjoint operators#✓fully proved

Let \(T\) be a compact self-adjoint operator on a Hilbert space \(H\) over \(\mathbb{R}\) or \(\mathbb{C}\). For every \(\varepsilon > 0\) there is a bounded self-adjoint operator \(F\) on \(H\) with finite-dimensional range such that \(\|T - F\| \le \varepsilon\).

theorem exists_finiteRank_approx {T : H →L[𝕜] H} (hT : IsSelfAdjoint T)
    (hc : IsCompactOperator (T : H → H)) {ε : ℝ} (hε : 0 < ε) :
    ∃ F : H →L[𝕜] H, IsSelfAdjoint F ∧
      FiniteDimensional 𝕜 ↥(LinearMap.range (F : H →ₗ[𝕜] H)) ∧ ‖T - F‖ ≤ ε

Uses 2

Proof usesFiniteness of large eigenvalues of a compact self-adjoint operator · A nonzero compact self-adjoint operator has an eigenvalue of modulus equal to its norm

TheoremMaximum principle for compact self-adjoint operators#✓fully proved

Let \(T\) be a compact self-adjoint operator on a Hilbert space \(H\) over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\). Then one of the following two alternatives holds.

Either there are \(N \in \mathbb{N}\) (possibly \(N = 0\), as for \(T = 0\)), nonzero real numbers \(s_0, \dots, s_{N-1}\) and an orthonormal family \(u_0, \dots, u_{N-1}\) in \(H\) such that \(T u_i = s_i u_i\) for every \(i < N\), \(|s_0| \ge |s_1| \ge \dots \ge |s_{N-1}|\), for every \(i < N\) every unit vector \(x \in H\) orthogonal to \(u_0, \dots, u_{i-1}\) satisfies \(|\langle T x, x \rangle| \le |s_i|\) while \(|\langle T u_i, u_i \rangle| = |s_i|\), and \(T x = 0\) for every \(x \in H\) orthogonal to all of \(u_0, \dots, u_{N-1}\).

Or there are nonzero real numbers \(s_0, s_1, s_2, \dots\) and an orthonormal sequence \(u_0, u_1, u_2, \dots\) in \(H\) such that \(T u_n = s_n u_n\) for every \(n\), the sequence \(|s_n|\) is nonincreasing and tends to \(0\) as \(n \to \infty\), for every \(n\) every unit vector \(x \in H\) orthogonal to \(u_0, \dots, u_{n-1}\) satisfies \(|\langle T x, x \rangle| \le |s_n|\) while \(|\langle T u_n, u_n \rangle| = |s_n|\), and \(T x = 0\) for every \(x \in H\) orthogonal to every \(u_n\).

MathlibExt.Analysis.InnerProductSpace.CompactSelfAdjointMaximumPrinciple.exists_nonzero_eigenvalue_enumeration · 15 lines

theorem exists_nonzero_eigenvalue_enumeration {T : H →L[𝕜] H}
    (hT : IsSelfAdjoint T) (hc : IsCompactOperator (T : H → H)) :
    (∃ (N : ℕ) (s : Fin N → ℝ) (u : Fin N → H),
      (∀ i, s i ≠ 0) ∧ (∀ i, T (u i) = (s i : 𝕜) • u i) ∧
      Orthonormal 𝕜 u ∧ Antitone (fun i => |s i|) ∧
      (∀ i, (∀ x : H, ‖x‖ = 1 → (∀ j < i, ⟪x, u j⟫_𝕜 = 0) →
        ‖⟪T x, x⟫_𝕜‖ ≤ |s i|) ∧ ‖⟪T (u i), u i⟫_𝕜‖ = |s i|) ∧
      ∀ x : H, (∀ i, ⟪x, u i⟫_𝕜 = 0) → T x = 0) ∨
    (∃ (s : ℕ → ℝ) (u : ℕ → H),
      (∀ n, s n ≠ 0) ∧ (∀ n, T (u n) = (s n : 𝕜) • u n) ∧
      Orthonormal 𝕜 u ∧ Antitone (fun n => |s n|) ∧
      Tendsto (fun n => |s n|) atTop (𝓝 0) ∧
      (∀ n, (∀ x : H, ‖x‖ = 1 → (∀ j < n, ⟪x, u j⟫_𝕜 = 0) →
        ‖⟪T x, x⟫_𝕜‖ ≤ |s n|) ∧ ‖⟪T (u n), u n⟫_𝕜‖ = |s n|) ∧
      ∀ x : H, (∀ n, ⟪x, u n⟫_𝕜 = 0) → T x = 0)

Uses 2 · Used by 1

Proof usesDeflation step · Finiteness of large eigenvalues of a compact self-adjoint operator

Used byMaximum principle for compact self-adjoint operators in finite dimension

TheoremMaximum principle for compact self-adjoint operators in finite dimension#✓fully proved

Let \(H\) be a finite-dimensional Hilbert space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\) and let \(T\) be a compact self-adjoint operator on \(H\). Then there are \(N \in \mathbb{N}\), nonzero real numbers \(s_0, \dots, s_{N-1}\) and an orthonormal family \(u_0, \dots, u_{N-1}\) in \(H\) such that \(T u_i = s_i u_i\) for every \(i < N\), \(|s_0| \ge |s_1| \ge \dots \ge |s_{N-1}|\), and for every \(i < N\) every unit vector \(x \in H\) orthogonal to \(u_0, \dots, u_{i-1}\) satisfies \(|\langle T x, x \rangle| \le |s_i|\), while \(|\langle T u_i, u_i \rangle| = |s_i|\). Moreover \(T x = 0\) for every \(x \in H\) orthogonal to all of \(u_0, \dots, u_{N-1}\).

theorem exists_finite_eigenvalue_enumeration [FiniteDimensional 𝕜 H]
    {T : H →L[𝕜] H} (hT : IsSelfAdjoint T) (hc : IsCompactOperator (T : H → H)) :
    ∃ (N : ℕ) (s : Fin N → ℝ) (u : Fin N → H),
      (∀ i, s i ≠ 0) ∧ (∀ i, T (u i) = (s i : 𝕜) • u i) ∧
      Orthonormal 𝕜 u ∧ Antitone (fun i => |s i|) ∧
      (∀ i, (∀ x : H, ‖x‖ = 1 → (∀ j < i, ⟪x, u j⟫_𝕜 = 0) →
        ‖⟪T x, x⟫_𝕜‖ ≤ |s i|) ∧ ‖⟪T (u i), u i⟫_𝕜‖ = |s i|) ∧
      ∀ x : H, (∀ i, ⟪x, u i⟫_𝕜 = 0) → T x = 0

Uses 1

Proof usesMaximum principle for compact self-adjoint operators

TheoremMaximum principle as a sequence in infinite dimension#✓fully proved

Let \(T\) be a compact self-adjoint operator on an infinite-dimensional Hilbert space \(H\) over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\). Then there are real numbers \(s_0, s_1, s_2, \dots\) and an orthonormal sequence \(u_0, u_1, u_2, \dots\) in \(H\) such that \(T u_n = s_n u_n\) and \(|s_{n+1}| \le |s_n|\) for every \(n\), \(|s_n| \to 0\) as \(n \to \infty\), and for every \(n\) every unit vector \(x \in H\) orthogonal to \(u_0, \dots, u_{n-1}\) satisfies \(|\langle T x, x \rangle| \le |s_n|\), while \(|\langle T u_n, u_n \rangle| = |s_n|\).

Unlike the maximum principle for compact self-adjoint operators, the \(s_n\) are not required to be nonzero, and no claim is made that \(T\) vanishes on the vectors orthogonal to every \(u_n\).

theorem exists_ordered_eigenvalue_sequence {T : H →L[𝕜] H} (hT : IsSelfAdjoint T)
    (hc : IsCompactOperator (T : H → H)) (hInf : ¬ FiniteDimensional 𝕜 H) :
    ∃ (s : ℕ → ℝ) (u : ℕ → H),
      (∀ n, T (u n) = (s n : 𝕜) • u n) ∧
      Orthonormal 𝕜 u ∧
      (∀ n, |s (n + 1)| ≤ |s n|) ∧
      Tendsto (fun n => |s n|) atTop (𝓝 0) ∧
      ∀ n, (∀ x : H, ‖x‖ = 1 → (∀ j < n, ⟪x, u j⟫_𝕜 = 0) → ‖⟪T x, x⟫_𝕜‖ ≤ |s n|) ∧
        ‖⟪T (u n), u n⟫_𝕜‖ = |s n|

Uses 2

Proof usesDeflation step · Finiteness of large eigenvalues of a compact self-adjoint operator

TheoremOrthogonal complement of the nonzero-eigenvalue eigenspaces#✓fully proved

Let \(H\) be a Hilbert space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\) and let \(T : H \to H\) be a compact self-adjoint bounded linear operator. Then the orthogonal complement of the subspace spanned by the eigenspaces \(\ker(T - \mu I)\) for all nonzero \(\mu \in \mathbb{K}\) equals the kernel of \(T\).

theorem orthogonal_iSup_eigenspaces_ne_zero_eq_ker {T : H →L[𝕜] H}
    (hT : IsSelfAdjoint T) (hc : IsCompactOperator (T : H → H)) :
    (⨆ (μ : 𝕜) (_ : μ ≠ 0), (eigenspace (T : End 𝕜 H) μ : Submodule 𝕜 H))ᗮ =
      LinearMap.ker T.toLinearMap

Used by 1

Used bySpectral theorem for compact self-adjoint operators (range decomposition form)

TheoremSpectral theorem for compact self-adjoint operators (range decomposition form)#✓fully proved

Spectral theorem for compact self-adjoint operators (range decomposition form). Let \(H\) be a Hilbert space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\) and let \(T : H \to H\) be a compact self-adjoint bounded linear operator. Then: (1) the closure of the subspace spanned by the eigenspaces \(\ker(T - \mu I)\) for all nonzero \(\mu \in \mathbb{K}\) equals the closure of the range of \(T\); (2) the closure of the range of \(T\) and the kernel of \(T\) are complementary subspaces: their intersection is \(\{0\}\) and their sum is \(H\); and (3) the eigenspaces \(\ker(T - \mu I)\), \(\mu \in \mathbb{K}\), are pairwise orthogonal for distinct values of \(\mu\).

theorem spectral_theorem_range_decomposition {T : H →L[𝕜] H}
    (hT : IsSelfAdjoint T) (hc : IsCompactOperator (T : H → H)) :
    (⨆ (μ : 𝕜) (_ : μ ≠ 0), (eigenspace (T : End 𝕜 H) μ : Submodule 𝕜 H)).topologicalClosure =
      (LinearMap.range T.toLinearMap).topologicalClosure ∧
    IsCompl (LinearMap.range T.toLinearMap).topologicalClosure (LinearMap.ker T.toLinearMap) ∧
    OrthogonalFamily 𝕜 (fun μ : 𝕜 => eigenspace (T : End 𝕜 H) μ)
      (fun μ => (eigenspace (T : End 𝕜 H) μ).subtypeₗᵢ)

Uses 1

Proof usesOrthogonal complement of the nonzero-eigenvalue eigenspaces

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.