Joint eigenspaces of commuting symmetric operators

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

Main Result

• LinearMap.IsSymmetric.directSum_isInternal_of_commute establishes that in finite dimensions if {A B : E →ₗ[𝕜] E}, then IsSymmetric A, IsSymmetric B and Commute A B imply that E decomposes as an internal direct sum of the pairwise orthogonal spaces eigenspace B μ ⊓ eigenspace A ν
• LinearMap.IsSymmetric.iSup_iInf_eigenspace_eq_top_of_commute establishes that in finite dimensions, the indexed supremum of the joint eigenspaces of a commuting tuple of symmetric linear operators equals ⊤
• LinearMap.IsSymmetric.directSum_isInternal_of_pairwise_commute establishes the analogous result to LinearMap.IsSymmetric.directSum_isInternal_of_commute for commuting tuples of symmetric operators.

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

symmetric operator, simultaneous eigenspaces, joint eigenspaces

theorem LinearMap.IsSymmetric.orthogonalFamily_eigenspace_inf_eigenspace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A B : E →ₗ[𝕜] E} (hA : A.IsSymmetric) (hB : B.IsSymmetric) : OrthogonalFamily 𝕜 (fun (i : 𝕜 × 𝕜) => ↥(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 joint eigenspaces of a pair of symmetric operators form an OrthogonalFamily.

theorem LinearMap.IsSymmetric.orthogonalFamily_iInf_eigenspaces {𝕜 : Type u_1} {E : Type u_2} {n : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : n → Module.End 𝕜 E} (hT : ∀ (i : n), IsSymmetric (T i)) : OrthogonalFamily 𝕜 (fun (γ : n → 𝕜) => ↥(⨅ (j : n), (T j).eigenspace (γ j))) fun (γ : n → 𝕜) => (⨅ (j : n), (T j).eigenspace (γ j)).subtypeₗᵢ

The joint eigenspaces of a family of symmetric operators form an OrthogonalFamily.

theorem LinearMap.IsSymmetric.iSup_eigenspace_inf_eigenspace_of_commute {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {α : 𝕜} {A B : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] (hB : B.IsSymmetric) (hAB : Commute A B) : ⨆ (γ : 𝕜), 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_of_commute {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A B : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] (hA : A.IsSymmetric) (hB : B.IsSymmetric) (hAB : Commute A B) : ⨆ (α : 𝕜), ⨆ (γ : 𝕜), 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_isInternal_of_commute {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A B : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] (hA : A.IsSymmetric) (hB : B.IsSymmetric) (hAB : Commute A B) : 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.

theorem LinearMap.IsSymmetric.iSup_iInf_eq_top_of_commute {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ι : Type u_5} {T : ι → E →ₗ[𝕜] E} (hT : ∀ (i : ι), (T i).IsSymmetric) (h : Pairwise (Function.onFun Commute T)) : ⨆ (χ : ι → 𝕜), ⨅ (i : ι), Module.End.eigenspace (T i) (χ i) = ⊤

A commuting family of symmetric linear maps on a finite dimensional inner product space is simultaneously diagonalizable.

theorem LinearMap.IsSymmetric.LinearMap.IsSymmetric.directSum_isInternal_of_pairwise_commute {𝕜 : Type u_1} {E : Type u_2} {n : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : n → Module.End 𝕜 E} [FiniteDimensional 𝕜 E] [DecidableEq (n → 𝕜)] (hT : ∀ (i : n), IsSymmetric (T i)) (hC : Pairwise (Function.onFun Commute T)) : DirectSum.IsInternal fun (α : n → 𝕜) => ⨅ (j : n), (T j).eigenspace (α j)

In finite dimensions, given a commuting family of symmetric linear operators, the inner product space on which they act decomposes as an internal direct sum of joint eigenspaces.