Documentation

Mathlib.Analysis.InnerProductSpace.Spectrum

Spectral theory of self-adjoint operators #

This file covers the spectral theory of self-adjoint operators on an inner product space.

The first part of the file covers general properties, true without any condition on boundedness or compactness of the operator or finite-dimensionality of the underlying space, notably:

The second part of the file covers properties of self-adjoint operators in finite dimension. Letting T be a self-adjoint operator on a finite-dimensional inner product space T,

These are forms of the diagonalization theorem for self-adjoint operators on finite-dimensional inner product spaces.

TODO #

Spectral theory for compact self-adjoint operators, bounded self-adjoint operators.

Tags #

self-adjoint operator, spectral theorem, diagonalization theorem

theorem LinearMap.IsSymmetric.invariant_orthogonalComplement_eigenspace {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} (hT : T.IsSymmetric) (ฮผ : ๐•œ) (v : E) (hv : v โˆˆ (Module.End.eigenspace T ฮผ)แ—ฎ) :

A self-adjoint operator preserves orthogonal complements of its eigenspaces.

theorem LinearMap.IsSymmetric.conj_eigenvalue_eq_self {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} (hT : T.IsSymmetric) {ฮผ : ๐•œ} (hฮผ : Module.End.HasEigenvalue T ฮผ) :
(starRingEnd ๐•œ) ฮผ = ฮผ

The eigenvalues of a self-adjoint operator are real.

theorem LinearMap.IsSymmetric.orthogonalFamily_eigenspaces {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} (hT : T.IsSymmetric) :
OrthogonalFamily ๐•œ (fun (ฮผ : ๐•œ) => โ†ฅ(Module.End.eigenspace T ฮผ)) fun (ฮผ : ๐•œ) => (Module.End.eigenspace T ฮผ).subtypeโ‚—แตข

The eigenspaces of a self-adjoint operator are mutually orthogonal.

theorem LinearMap.IsSymmetric.orthogonalFamily_eigenspaces' {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} (hT : T.IsSymmetric) :
OrthogonalFamily ๐•œ (fun (ฮผ : Module.End.Eigenvalues T) => โ†ฅ(Module.End.eigenspace T (โ†‘T ฮผ))) fun (ฮผ : Module.End.Eigenvalues T) => (Module.End.eigenspace T (โ†‘T ฮผ)).subtypeโ‚—แตข
theorem LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_invariant {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} (hT : T.IsSymmetric) โฆƒv : Eโฆ„ (hv : v โˆˆ (โจ† (ฮผ : ๐•œ), Module.End.eigenspace T ฮผ)แ—ฎ) :
T v โˆˆ (โจ† (ฮผ : ๐•œ), Module.End.eigenspace T ฮผ)แ—ฎ

The mutual orthogonal complement of the eigenspaces of a self-adjoint operator on an inner product space is an invariant subspace of the operator.

theorem LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} (hT : T.IsSymmetric) (ฮผ : ๐•œ) :
Module.End.eigenspace (T.restrict โ‹ฏ) ฮผ = โŠฅ

The mutual orthogonal complement of the eigenspaces of a self-adjoint operator on an inner product space has no eigenvalues.

Finite-dimensional theory #

theorem LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} (hT : T.IsSymmetric) [FiniteDimensional ๐•œ E] :
(โจ† (ฮผ : ๐•œ), Module.End.eigenspace T ฮผ)แ—ฎ = โŠฅ

The mutual orthogonal complement of the eigenspaces of a self-adjoint operator on a finite-dimensional inner product space is trivial.

theorem LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot' {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} (hT : T.IsSymmetric) [FiniteDimensional ๐•œ E] :
(โจ† (ฮผ : Module.End.Eigenvalues T), Module.End.eigenspace T (โ†‘T ฮผ))แ—ฎ = โŠฅ
noncomputable instance LinearMap.IsSymmetric.directSumDecomposition {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} [FiniteDimensional ๐•œ E] [hT : Fact T.IsSymmetric] :

The eigenspaces of a self-adjoint operator on a finite-dimensional inner product space E gives an internal direct sum decomposition of E.

Note this takes hT as a Fact to allow it to be an instance.

Equations
  • LinearMap.IsSymmetric.directSumDecomposition = โ‹ฏ.decomposition โ‹ฏ
theorem LinearMap.IsSymmetric.directSum_decompose_apply {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} [FiniteDimensional ๐•œ E] [_hT : Fact T.IsSymmetric] (x : E) (ฮผ : Module.End.Eigenvalues T) :
((DirectSum.decompose fun (ฮผ : Module.End.Eigenvalues T) => Module.End.eigenspace T (โ†‘T ฮผ)) x) ฮผ = (orthogonalProjection (Module.End.eigenspace T (โ†‘T ฮผ))) x
theorem LinearMap.IsSymmetric.direct_sum_isInternal {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} (hT : T.IsSymmetric) [FiniteDimensional ๐•œ E] :
DirectSum.IsInternal fun (ฮผ : Module.End.Eigenvalues T) => Module.End.eigenspace T (โ†‘T ฮผ)

The eigenspaces of a self-adjoint operator on a finite-dimensional inner product space E gives an internal direct sum decomposition of E.

noncomputable def LinearMap.IsSymmetric.diagonalization {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} (hT : T.IsSymmetric) [FiniteDimensional ๐•œ E] :
E โ‰ƒโ‚—แตข[๐•œ] PiLp 2 fun (ฮผ : Module.End.Eigenvalues T) => โ†ฅ(Module.End.eigenspace T (โ†‘T ฮผ))

Isometry from an inner product space E to the direct sum of the eigenspaces of some self-adjoint operator T on E.

Equations
  • hT.diagonalization = โ‹ฏ.isometryL2OfOrthogonalFamily โ‹ฏ
Instances For
    @[simp]
    theorem LinearMap.IsSymmetric.diagonalization_symm_apply {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} (hT : T.IsSymmetric) [FiniteDimensional ๐•œ E] (w : PiLp 2 fun (ฮผ : Module.End.Eigenvalues T) => โ†ฅ(Module.End.eigenspace T (โ†‘T ฮผ))) :
    hT.diagonalization.symm w = โˆ‘ ฮผ : Module.End.Eigenvalues T, โ†‘(w ฮผ)
    theorem LinearMap.IsSymmetric.diagonalization_apply_self_apply {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} (hT : T.IsSymmetric) [FiniteDimensional ๐•œ E] (v : E) (ฮผ : Module.End.Eigenvalues T) :
    hT.diagonalization (T v) ฮผ = โ†‘T ฮผ โ€ข hT.diagonalization v ฮผ

    Diagonalization theorem, spectral theorem; version 1: A self-adjoint operator T on a finite-dimensional inner product space E acts diagonally on the decomposition of E into the direct sum of the eigenspaces of T.

    theorem LinearMap.IsSymmetric.eigenvectorBasis_def {๐•œ : Type u_3} [RCLike ๐•œ] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} (hT : T.IsSymmetric) [FiniteDimensional ๐•œ E] {n : โ„•} (hn : FiniteDimensional.finrank ๐•œ E = n) :
    hT.eigenvectorBasis hn = DirectSum.IsInternal.subordinateOrthonormalBasis hn โ‹ฏ โ‹ฏ
    @[irreducible]
    noncomputable def LinearMap.IsSymmetric.eigenvectorBasis {๐•œ : Type u_3} [RCLike ๐•œ] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} (hT : T.IsSymmetric) [FiniteDimensional ๐•œ E] {n : โ„•} (hn : FiniteDimensional.finrank ๐•œ E = n) :
    OrthonormalBasis (Fin n) ๐•œ E

    A choice of orthonormal basis of eigenvectors for self-adjoint operator T on a finite-dimensional inner product space E.

    TODO Postcompose with a permutation so that these eigenvectors are listed in increasing order of eigenvalue.

    Equations
    Instances For
      theorem LinearMap.IsSymmetric.eigenvalues_def {๐•œ : Type u_3} [RCLike ๐•œ] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} (hT : T.IsSymmetric) [FiniteDimensional ๐•œ E] {n : โ„•} (hn : FiniteDimensional.finrank ๐•œ E = n) (i : Fin n) :
      hT.eigenvalues hn i = RCLike.re (โ†‘T (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn โ‹ฏ i โ‹ฏ))
      @[irreducible]
      noncomputable def LinearMap.IsSymmetric.eigenvalues {๐•œ : Type u_3} [RCLike ๐•œ] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} (hT : T.IsSymmetric) [FiniteDimensional ๐•œ E] {n : โ„•} (hn : FiniteDimensional.finrank ๐•œ E = n) (i : Fin n) :

      The sequence of real eigenvalues associated to the standard orthonormal basis of eigenvectors for a self-adjoint operator T on E.

      TODO Postcompose with a permutation so that these eigenvalues are listed in increasing order.

      Equations
      Instances For
        theorem LinearMap.IsSymmetric.hasEigenvector_eigenvectorBasis {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} (hT : T.IsSymmetric) [FiniteDimensional ๐•œ E] {n : โ„•} (hn : FiniteDimensional.finrank ๐•œ E = n) (i : Fin n) :
        Module.End.HasEigenvector T (โ†‘(hT.eigenvalues hn i)) ((hT.eigenvectorBasis hn) i)
        theorem LinearMap.IsSymmetric.hasEigenvalue_eigenvalues {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} (hT : T.IsSymmetric) [FiniteDimensional ๐•œ E] {n : โ„•} (hn : FiniteDimensional.finrank ๐•œ E = n) (i : Fin n) :
        Module.End.HasEigenvalue T โ†‘(hT.eigenvalues hn i)
        @[simp]
        theorem LinearMap.IsSymmetric.apply_eigenvectorBasis {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} (hT : T.IsSymmetric) [FiniteDimensional ๐•œ E] {n : โ„•} (hn : FiniteDimensional.finrank ๐•œ E = n) (i : Fin n) :
        T ((hT.eigenvectorBasis hn) i) = โ†‘(hT.eigenvalues hn i) โ€ข (hT.eigenvectorBasis hn) i
        theorem LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} (hT : T.IsSymmetric) [FiniteDimensional ๐•œ E] {n : โ„•} (hn : FiniteDimensional.finrank ๐•œ E = n) (v : E) (i : Fin n) :
        (hT.eigenvectorBasis hn).repr (T v) i = โ†‘(hT.eigenvalues hn i) * (hT.eigenvectorBasis hn).repr v i

        Diagonalization theorem, spectral theorem; version 2: A self-adjoint operator T on a finite-dimensional inner product space E acts diagonally on the identification of E with Euclidean space induced by an orthonormal basis of eigenvectors of T.

        @[simp]
        theorem inner_product_apply_eigenvector {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮผ : ๐•œ} {v : E} {T : E โ†’โ‚—[๐•œ] E} (h : v โˆˆ Module.End.eigenspace T ฮผ) :
        โŸชv, T vโŸซ_๐•œ = ฮผ * โ†‘โ€–vโ€– ^ 2
        theorem eigenvalue_nonneg_of_nonneg {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮผ : โ„} {T : E โ†’โ‚—[๐•œ] E} (hฮผ : Module.End.HasEigenvalue T โ†‘ฮผ) (hnn : โˆ€ (x : E), 0 โ‰ค RCLike.re โŸชx, T xโŸซ_๐•œ) :
        0 โ‰ค ฮผ
        theorem eigenvalue_pos_of_pos {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮผ : โ„} {T : E โ†’โ‚—[๐•œ] E} (hฮผ : Module.End.HasEigenvalue T โ†‘ฮผ) (hnn : โˆ€ (x : E), 0 < RCLike.re โŸชx, T xโŸซ_๐•œ) :
        0 < ฮผ