Joint eigenspaces of a commuting pair of symmetric operators

This file collects various decomposition results for joint eigenspaces of a commuting pair of symmetric operators on a finite-dimensional inner product space.

Main Result

• LinearMap.IsSymmetric.directSum_isInternal_of_commute establishes that if {A B : E →ₗ[𝕜] E}, then IsSymmetric A, IsSymmetric B and A ∘ₗ B = B ∘ₗ A imply that E decomposes as an internal direct sum of the pairwise orthogonal spaces eigenspace B μ ⊓ eigenspace A ν

TODO

Develop a Diagonalization structure for linear maps and / or matrices which consists of a basis, and a proof obligation that the basis vectors are eigenvectors.

Tags

self-adjoint operator, simultaneous eigenspaces, joint eigenspaces

theorem LinearMap.IsSymmetric.eigenspace_invariant_of_commute {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ[𝕜] E} {B : E →ₗ[𝕜] E} (hAB : A ∘ₗ B = B ∘ₗ A) (α : 𝕜) (v : E) : v ∈ Module.End.eigenspace A α → B v ∈ Module.End.eigenspace A α

If a pair of operators commute, then the eigenspaces of one are invariant under the other.

theorem LinearMap.IsSymmetric.orthogonalFamily_eigenspace_inf_eigenspace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ[𝕜] E} {B : E →ₗ[𝕜] E} (hA : A.IsSymmetric) (hB : B.IsSymmetric) : OrthogonalFamily 𝕜 (fun (i : 𝕜 × 𝕜) => { x : E // x ∈ Module.End.eigenspace A i.2 ⊓ Module.End.eigenspace B i.1 }) fun (i : 𝕜 × 𝕜) => (Module.End.eigenspace A i.2 ⊓ Module.End.eigenspace B i.1).subtypeₗᵢ

The simultaneous eigenspaces of a pair of commuting symmetric operators form an OrthogonalFamily.

theorem LinearMap.IsSymmetric.eigenspace_inf_eigenspace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {α : 𝕜} {A : E →ₗ[𝕜] E} {B : E →ₗ[𝕜] E} (hAB : A ∘ₗ B = B ∘ₗ A) (γ : 𝕜) : Module.End.eigenspace A α ⊓ Module.End.eigenspace B γ = Submodule.map (Module.End.eigenspace A α).subtype (Module.End.eigenspace (B.restrict ⋯) γ)

The intersection of eigenspaces of commuting selfadjoint operators is equal to the eigenspace of one operator restricted to the eigenspace of the other, which is an invariant subspace because the operators commute.

theorem LinearMap.IsSymmetric.iSup_eigenspace_inf_eigenspace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {α : 𝕜} {A : E →ₗ[𝕜] E} {B : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] (hB : B.IsSymmetric) (hAB : A ∘ₗ B = B ∘ₗ A) : ⨆ (γ : 𝕜), Module.End.eigenspace A α ⊓ Module.End.eigenspace B γ = Module.End.eigenspace A α

If A and B are commuting symmetric operators on a finite dimensional inner product space then the eigenspaces of the restriction of B to any eigenspace of A exhaust that eigenspace.

theorem LinearMap.IsSymmetric.iSup_iSup_eigenspace_inf_eigenspace_eq_top {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ[𝕜] E} {B : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] (hA : A.IsSymmetric) (hB : B.IsSymmetric) (hAB : A ∘ₗ B = B ∘ₗ A) : ⨆ (α : 𝕜), ⨆ (γ : 𝕜), Module.End.eigenspace A α ⊓ Module.End.eigenspace B γ = ⊤

If A and B are commuting symmetric operators acting on a finite dimensional inner product space, then the simultaneous eigenspaces of A and B exhaust the space.

theorem LinearMap.IsSymmetric.directSum_isInteral_of_commute {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ[𝕜] E} {B : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] (hA : A.IsSymmetric) (hB : B.IsSymmetric) (hAB : A ∘ₗ B = B ∘ₗ A) : DirectSum.IsInternal fun (i : 𝕜 × 𝕜) => Module.End.eigenspace A i.2 ⊓ Module.End.eigenspace B i.1

Given a commuting pair of symmetric linear operators on a finite dimensional inner product space, the space decomposes as an internal direct sum of simultaneous eigenspaces of these operators.