Compact self-adjoint operators: large-eigenspace approximation in operator norm

For a compact self-adjoint operator T and ε > 0, the “large-eigenvalue” cutoff projector largeEigenspaceProjector T ε yields a finite-dimensional approximation:

• T ∘ largeEigenspaceProjector T ε has finite-dimensional range, and
• ‖T - T ∘ largeEigenspaceProjector T ε‖ ≤ ε.

theorem CompactSelfAdjoint.largeEigenspace_mem_invtSubmodule_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 < ε) : have t := ↑T; largeEigenspace T ε ∈ t.invtSubmodule

theorem CompactSelfAdjoint.largeEigenspace_orthogonal_mem_invtSubmodule_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 < ε) : have t := ↑T; (largeEigenspace T ε)ᗮ ∈ t.invtSubmodule

Finite-rank approximation in operator norm

theorem CompactSelfAdjoint.finiteDimensional_range_comp_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 < ε) : FiniteDimensional 𝕜 ↥(↑(T ∘SL largeEigenspaceProjector T hT hTc hε)).range

theorem CompactSelfAdjoint.opNorm_sub_comp_largeEigenspaceProjector_le {𝕜 : 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 < ε) : ‖T - T ∘SL largeEigenspaceProjector T hT hTc hε‖ ≤ ε