Compact self-adjoint operators: an eigenvalue at the operator norm

This file provides two Hilbert-space facts about compact operators:

• A compact operator attains its operator norm on the unit sphere.
• A compact self-adjoint operator has an eigenvalue whose norm is its operator norm.

These are used downstream to turn “no eigenvalues above ε” into an operator-norm estimate.

Weak continuity of the norm on a weakly-closed ball

theorem CompactSelfAdjoint.continuousOn_weakClosedBall_norm_apply_of_isCompactOperator {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) (hTc : IsCompactOperator ⇑T) (r : ℝ) : ContinuousOn (fun (x : WeakSpace 𝕜 E) => ‖T x‖) (CompactSpectral.weakClosedBall r)

Norm attainment for compact operators

theorem CompactSelfAdjoint.exists_unit_norm_eq_opNorm_of_isCompactOperator {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [Nontrivial E] (T : E →L[𝕜] E) (hTc : IsCompactOperator ⇑T) : ∃ (x : E), ‖x‖ = 1 ∧ ‖T x‖ = ‖T‖

A compact self-adjoint operator has an eigenvalue at the operator norm

theorem CompactSelfAdjoint.exists_hasEigenvector_norm_eq_opNorm_of_isCompactOperator_of_isSelfAdjoint {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [Nontrivial E] (T : E →L[𝕜] E) (hT : IsSelfAdjoint T) (hTc : IsCompactOperator ⇑T) : ∃ (μ : 𝕜) (v : E), Module.End.HasEigenvector (↑T) μ v ∧ ‖μ‖ = ‖T‖