Compact self-adjoint operators: compression / restriction helpers

This file provides small lemmas that make it convenient to iterate the Rayleigh-extremum eigenvector construction for compact self-adjoint operators by passing to orthogonal complements.

The key technical device is to compress a bounded operator T to a complete submodule V using the orthogonal projection E →L[𝕜] V. When V is invariant under T, this compression agrees with the naive restriction and eigenvectors lift back to eigenvectors of T.

Main definitions

• CompactSelfAdjoint.compress: compression of T to a complete submodule V.

Main results

• CompactSelfAdjoint.isSelfAdjoint_compress
• CompactSelfAdjoint.isCompactOperator_compress
• CompactSelfAdjoint.hasEigenvector_of_hasEigenvector_compress_of_invariant
• CompactSelfAdjoint.invariant_orthogonalComplement_eigenspace_of_isSelfAdjoint

noncomputable def CompactSelfAdjoint.compress {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) (V : Submodule 𝕜 E) [CompleteSpace ↥V] : ↥V →L[𝕜] ↥V

Compress a bounded operator T to a complete submodule V using the orthogonal projection.

Equations

• CompactSelfAdjoint.compress T V = V.orthogonalProjectionOnto ∘SL T ∘SL V.subtypeL

theorem CompactSelfAdjoint.coe_compress_apply_of_invariant {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) (V : Submodule 𝕜 E) [CompleteSpace ↥V] (hV : ∀ v ∈ V, T v ∈ V) (v : ↥V) : ↑((compress T V) v) = T ↑v

theorem CompactSelfAdjoint.hasEigenvector_of_hasEigenvector_compress_of_invariant {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) (V : Submodule 𝕜 E) [CompleteSpace ↥V] (hV : ∀ v ∈ V, T v ∈ V) {μ : 𝕜} {v : ↥V} (hv : Module.End.HasEigenvector (↑(compress T V)) μ v) : Module.End.HasEigenvector (↑T) μ ↑v

theorem CompactSelfAdjoint.isCompactOperator_compress {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) (hTc : IsCompactOperator ⇑T) (V : Submodule 𝕜 E) [CompleteSpace ↥V] : IsCompactOperator ⇑(compress T V)

theorem CompactSelfAdjoint.isSelfAdjoint_compress {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) (hT : IsSelfAdjoint T) (V : Submodule 𝕜 E) [CompleteSpace ↥V] : IsSelfAdjoint (compress T V)

theorem CompactSelfAdjoint.invariant_orthogonalComplement_eigenspace_of_isSelfAdjoint {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) (hT : IsSelfAdjoint T) (μ : 𝕜) (v : E) : v ∈ (Module.End.eigenspace (↑T) μ)ᗮ → T v ∈ (Module.End.eigenspace (↑T) μ)ᗮ