Compact self-adjoint operators: large-eigenspace cutoff projectors

This file defines the “large-eigenvalue” spectral cutoff subspace for a compact self-adjoint operator and packages its orthogonal projector, together with basic algebraic properties.

The key downstream use is to build finite-dimensional (hence finite-rank) approximations and to enable spectral iteration by compressing to invariant orthogonal complements.

Main definitions

• CompactSelfAdjoint.largeEigenspace
• CompactSelfAdjoint.largeEigenspaceProjector

Main results

• CompactSelfAdjoint.finiteDimensional_largeEigenspace_of_isCompactOperator_of_isSelfAdjoint
• CompactSelfAdjoint.isStarProjection_largeEigenspaceProjector
• CompactSelfAdjoint.range_largeEigenspaceProjector
• CompactSelfAdjoint.largeEigenspaceProjector_comp

Large-eigenspace cutoff subspace and projector

noncomputable def CompactSelfAdjoint.largeEigenspace {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) (ε : ℝ) : Submodule 𝕜 E

The spectral cutoff subspace spanned by all eigenspaces with ‖μ‖ ≥ ε.

Equations

• CompactSelfAdjoint.largeEigenspace T ε = ⨆ (i : { μ : 𝕜 // ε ≤ ‖μ‖ ∧ Module.End.HasEigenvalue (↑T) μ }), Module.End.eigenspace ↑T ↑i

theorem CompactSelfAdjoint.finiteDimensional_largeEigenspace_of_isCompactOperator_of_isSelfAdjoint {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) (hT : IsSelfAdjoint T) (hTc : IsCompactOperator ⇑T) {ε : ℝ} (hε : 0 < ε) : FiniteDimensional 𝕜 ↥(largeEigenspace T ε)

For a compact self-adjoint operator, largeEigenspace is finite-dimensional (hence complete).

noncomputable def CompactSelfAdjoint.largeEigenspaceProjector {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) (hT : IsSelfAdjoint T) (hTc : IsCompactOperator ⇑T) {ε : ℝ} (hε : 0 < ε) : E →L[𝕜] E

The orthogonal projector onto the largeEigenspace cutoff subspace.

Equations

• CompactSelfAdjoint.largeEigenspaceProjector T hT hTc hε = (CompactSelfAdjoint.largeEigenspace T ε).starProjection

theorem CompactSelfAdjoint.isStarProjection_largeEigenspaceProjector {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) (hT : IsSelfAdjoint T) (hTc : IsCompactOperator ⇑T) {ε : ℝ} (hε : 0 < ε) : IsStarProjection (largeEigenspaceProjector T hT hTc hε)

theorem CompactSelfAdjoint.isSelfAdjoint_largeEigenspaceProjector {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) (hT : IsSelfAdjoint T) (hTc : IsCompactOperator ⇑T) {ε : ℝ} (hε : 0 < ε) : IsSelfAdjoint (largeEigenspaceProjector T hT hTc hε)

theorem CompactSelfAdjoint.largeEigenspaceProjector_idem {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) (hT : IsSelfAdjoint T) (hTc : IsCompactOperator ⇑T) {ε : ℝ} (hε : 0 < ε) : largeEigenspaceProjector T hT hTc hε ∘SL largeEigenspaceProjector T hT hTc hε = largeEigenspaceProjector T hT hTc hε

theorem CompactSelfAdjoint.range_largeEigenspaceProjector {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) (hT : IsSelfAdjoint T) (hTc : IsCompactOperator ⇑T) {ε : ℝ} (hε : 0 < ε) : (↑(largeEigenspaceProjector T hT hTc hε)).range = largeEigenspace T ε

Cutoff projectors commute with the operator

theorem CompactSelfAdjoint.largeEigenspaceProjector_comp {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) (hT : IsSelfAdjoint T) (hTc : IsCompactOperator ⇑T) {ε : ℝ} (hε : 0 < ε) : largeEigenspaceProjector T hT hTc hε ∘SL T = T ∘SL largeEigenspaceProjector T hT hTc hε