Compact self-adjoint operators: spectral finiteness toolkit

This file collects “spectral finiteness” facts for compact self-adjoint operators on Hilbert spaces: finite-dimensionality of nonzero eigenspaces, finiteness away from 0, countability of the nonzero point spectrum, isolation of nonzero eigenvalues, and a packaged ‖μ n‖ → 0 statement for injective eigenvalue sequences.

These are standard ingredients for spectral-iteration proofs and compact-resolvent applications.

Main results

• CompactSelfAdjoint.finiteDimensional_eigenspace_of_isCompactOperator

• CompactSelfAdjoint.finite_set_hasEigenvalue_norm_ge_of_isCompactOperator_of_isSelfAdjoint

• CompactSelfAdjoint.countable_set_hasEigenvalue_ne_zero_of_isCompactOperator_of_isSelfAdjoint

• CompactSelfAdjoint.exists_ball_hasEigenvalue_eq_of_isCompactOperator_of_isSelfAdjoint

• CompactSelfAdjoint.finiteDimensional_iSup_eigenspace_norm_ge

• CompactSelfAdjoint.tendsto_norm_of_injective_hasEigenvalue_of_isCompactOperator_of_isSelfAdjoint

Finite-dimensionality of nonzero eigenspaces

theorem CompactSelfAdjoint.finiteDimensional_eigenspace_of_isCompactOperator {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) (hTc : IsCompactOperator ⇑T) {μ : 𝕜} (hμ : μ ≠ 0) : FiniteDimensional 𝕜 ↥(Module.End.eigenspace (↑T) μ)

If T is compact, then the eigenspace for a nonzero eigenvalue is finite-dimensional.

Finiteness of large eigenvalues (self-adjoint case)

theorem CompactSelfAdjoint.not_exists_injective_hasEigenvalue_norm_ge_of_isCompactOperator_of_isSelfAdjoint {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) (hT : IsSelfAdjoint T) (hTc : IsCompactOperator ⇑T) {ε : ℝ} (hε : 0 < ε) : ¬∃ (μ : ℕ → 𝕜), Function.Injective μ ∧ (∀ (n : ℕ), ε ≤ ‖μ n‖) ∧ ∀ (n : ℕ), Module.End.HasEigenvalue (↑T) (μ n)

For a compact self-adjoint operator, there is no infinite sequence of distinct eigenvalues whose norm is bounded below by ε > 0. This is a standard compact spectral theorem ingredient: since distinct eigenspaces are orthogonal, such a sequence would give an orthonormal family e n with ‖T (e n)‖ = ‖μ n‖ ≥ ε, contradicting that compact operators send orthonormal sequences to norm-null sequences.

theorem CompactSelfAdjoint.finite_set_hasEigenvalue_norm_ge_of_isCompactOperator_of_isSelfAdjoint {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) (hT : IsSelfAdjoint T) (hTc : IsCompactOperator ⇑T) {ε : ℝ} (hε : 0 < ε) : {μ : 𝕜 | ε ≤ ‖μ‖ ∧ Module.End.HasEigenvalue (↑T) μ}.Finite

For a compact self-adjoint operator, the set of eigenvalues with norm bounded below by ε > 0 is finite.

theorem CompactSelfAdjoint.countable_set_hasEigenvalue_ne_zero_of_isCompactOperator_of_isSelfAdjoint {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) (hT : IsSelfAdjoint T) (hTc : IsCompactOperator ⇑T) : {μ : 𝕜 | μ ≠ 0 ∧ Module.End.HasEigenvalue (↑T) μ}.Countable

For a compact self-adjoint operator, the set of nonzero eigenvalues is countable (indeed, only 0 can be an accumulation point).

theorem CompactSelfAdjoint.tendsto_norm_of_injective_hasEigenvalue_of_isCompactOperator_of_isSelfAdjoint {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) (hT : IsSelfAdjoint T) (hTc : IsCompactOperator ⇑T) {μ : ℕ → 𝕜} (hμinj : Function.Injective μ) (hμeig : ∀ (n : ℕ), Module.End.HasEigenvalue (↑T) (μ n)) : Filter.Tendsto (fun (n : ℕ) => ‖μ n‖) Filter.atTop (nhds 0)

For a compact self-adjoint operator, any injective eigenvalue sequence must have eigenvalues converging to 0 in norm.

Isolation of nonzero eigenvalues

theorem CompactSelfAdjoint.exists_ball_hasEigenvalue_eq_of_isCompactOperator_of_isSelfAdjoint {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) (hT : IsSelfAdjoint T) (hTc : IsCompactOperator ⇑T) {μ : 𝕜} (hμ0 : μ ≠ 0) (hμeig : Module.End.HasEigenvalue (↑T) μ) : ∃ r > 0, ∀ {ν : 𝕜}, Module.End.HasEigenvalue (↑T) ν → dist ν μ < r → ν = μ

For a compact self-adjoint operator, any nonzero eigenvalue is isolated among eigenvalues.

Finite-dimensionality of large spectral subspaces

theorem CompactSelfAdjoint.finiteDimensional_iSup_eigenspace_norm_ge {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) (hT : IsSelfAdjoint T) (hTc : IsCompactOperator ⇑T) {ε : ℝ} (hε : 0 < ε) : have t := ↑T; FiniteDimensional 𝕜 ↥(⨆ (i : { μ : 𝕜 // ε ≤ ‖μ‖ ∧ t.HasEigenvalue μ }), t.eigenspace ↑i)

For a compact self-adjoint operator, the sum (iSup) of eigenspaces corresponding to eigenvalues with ‖μ‖ ≥ ε is finite-dimensional.