Spectrum of finite-rank operators

10 fully proved

Linear Algebra

TheoremEigenvectors for nonzero eigenvalues lie in the range#✓fully proved

An eigenvector for a nonzero eigenvalue lies in the range: if T v = μ • v with μ ≠ 0, then v = T (μ⁻¹ • v).

theorem Module.End.eigenvector_mem_range_of_hasEigenvector {μ : 𝕜} {v : E}
    (h : T.HasEigenvector μ v) (hμ : μ ≠ 0) : v ∈ LinearMap.range T

Used by 1

Used byIndependent eigenvectors for distinct nonzero eigenvalues

TheoremIndependent eigenvectors for distinct nonzero eigenvalues#✓fully proved

Choose one eigenvector for each nonzero eigenvalue of T. The chosen eigenvectors are linearly independent (eigenvectors for distinct eigenvalues) and all lie in the range of T.

theorem Module.End.exists_linearIndependent_eigenvectors :
    ∃ xs : {μ // Module.End.HasEigenvalue T μ ∧ μ ≠ 0} → E,
      LinearIndependent 𝕜 xs ∧
        (∀ μ, xs μ ∈ LinearMap.range T) ∧
        ∀ μ : {μ // T.HasEigenvalue μ ∧ μ ≠ 0}, T.HasEigenvector (μ : 𝕜) (xs μ)

Uses 1 · Used by 2

Proof usesEigenvectors for nonzero eigenvalues lie in the range

Used byEigenvalue finiteness for finite-rank operators · Eigenvalue-count bound for finite-rank operators

TheoremEigenvalue finiteness for finite-rank operators#✓fully proved

A finite-rank operator has only finitely many distinct nonzero eigenvalues.

theorem Module.End.finite_nonzero_hasEigenvalue_of_finiteDimensional_range
    (hF : FiniteDimensional 𝕜 (LinearMap.range T)) :
    ({μ | Module.End.HasEigenvalue T μ ∧ μ ≠ 0} : Set 𝕜).Finite

Uses 1 · Used by 3

Proof usesIndependent eigenvectors for distinct nonzero eigenvalues

Used bySpectrum of a finite-rank operator is finite · Eigenvalue-count bound for finite-rank operators · Bound on the size of the spectrum of a finite-rank operator

TheoremEigenvalue-count bound for finite-rank operators#✓fully proved

There are at most finrank (range T) distinct nonzero eigenvalues.

theorem Module.End.ncard_nonzero_hasEigenvalue_le_finrank_range
    (hF : FiniteDimensional 𝕜 (LinearMap.range T)) :
    ({μ | Module.End.HasEigenvalue T μ ∧ μ ≠ 0} : Set 𝕜).ncard ≤
      Module.finrank 𝕜 (LinearMap.range T)

Uses 2 · Used by 1

Proof usesIndependent eigenvectors for distinct nonzero eigenvalues · Eigenvalue finiteness for finite-rank operators

Used byBound on the size of the spectrum of a finite-rank operator

Compactness

TheoremFinite-rank operators are compact#✓fully proved

A finite-rank operator is compact: it factors through its finite-dimensional range, and every continuous linear map out of a finite-dimensional (hence locally compact) space is compact.

theorem isCompactOperator_of_finiteDimensional_range
    (hF : FiniteDimensional 𝕜 (LinearMap.range (T : E →ₗ[𝕜] E))) :
    IsCompactOperator T

Used by 2

Used bySpectrum of a finite-rank operator on an infinite-dimensional space · Nonzero spectral values of a finite-rank operator are eigenvalues

Spectrum

TheoremNonzero spectral values of a finite-rank operator are eigenvalues#✓fully proved

The spectrum of a finite-rank operator is contained in {0} ∪ {eigenvalues}: every nonzero spectral value is an eigenvalue, by the Fredholm alternative for compact operators.

theorem spectrum_subset_insert_zero_hasEigenvalue
    (hF : FiniteDimensional 𝕜 (LinearMap.range (T : E →ₗ[𝕜] E))) :
    spectrum 𝕜 T ⊆ insert 0
      {μ | Module.End.HasEigenvalue (T : E →ₗ[𝕜] E) μ}

Uses 1 · Used by 3

Proof usesFinite-rank operators are compact

Used bySpectrum of a finite-rank operator is finite · Bound on the size of the spectrum of a finite-rank operator · Spectrum of a finite-rank operator on an infinite-dimensional space

TheoremEigenvalues of a finite-rank operator lie in its spectrum#✓fully proved

Every eigenvalue of a finite-rank operator lies in its spectrum.

theorem hasEigenvalue_subset_spectrum :
    {μ | Module.End.HasEigenvalue (T : E →ₗ[𝕜] E) μ} ⊆ spectrum 𝕜 T

Used by 1

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

TheoremSpectrum of a finite-rank operator is finite#✓fully proved

The spectrum of a finite-rank operator is finite.

theorem finite_spectrum_of_finiteDimensional_range
    (hF : FiniteDimensional 𝕜 (LinearMap.range (T : E →ₗ[𝕜] E))) :
    (spectrum 𝕜 T).Finite

Uses 2

Proof usesEigenvalue finiteness for finite-rank operators · Nonzero spectral values of a finite-rank operator are eigenvalues

TheoremBound on the size of the spectrum of a finite-rank operator#✓fully proved

The spectrum of a finite-rank operator has at most finrank (range T) + 1 points.

theorem ncard_spectrum_le_finrank_range_add_one
    (hF : FiniteDimensional 𝕜 (LinearMap.range (T : E →ₗ[𝕜] E))) :
    (spectrum 𝕜 T).ncard ≤ Module.finrank 𝕜 (LinearMap.range (T : E →ₗ[𝕜] E)) + 1

Uses 3

Proof usesEigenvalue finiteness for finite-rank operators · Eigenvalue-count bound for finite-rank operators · Nonzero spectral values of a finite-rank operator are eigenvalues

TheoremSpectrum of a finite-rank operator on an infinite-dimensional space#✓fully proved

The spectrum is exactly {0} ∪ {eigenvalues}.

theorem spectrum_eq_insert_zero_hasEigenvalue
    (hF : FiniteDimensional 𝕜 (LinearMap.range (T : E →ₗ[𝕜] E)))
    (hInf : ¬ FiniteDimensional 𝕜 E) :
    spectrum 𝕜 T = insert 0
      {μ | Module.End.HasEigenvalue (T : E →ₗ[𝕜] E) μ}

Uses 4

Proof usesZero lies in the spectrum of a compact operator on an infinite-dimensional space · Eigenvalues of a finite-rank operator lie in its spectrum · Finite-rank operators are compact · Nonzero spectral values of a finite-rank operator are eigenvalues

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.