Compact operators on orthonormal sequences

In a (real or complex) Hilbert space, an orthonormal sequence converges to 0 in the weak topology. As a corollary, a compact operator sends orthonormal sequences to norm-null sequences.

These lemmas are useful for iterating the Rayleigh-quotient eigenvector construction toward compact self-adjoint spectral theory (and later, compact-resolvent arguments for unbounded operators such as Laplace–Beltrami).

Main results

• CompactSpectral.tendsto_zero_weakSpace_of_orthonormal
• CompactSpectral.tendsto_zero_apply_of_isCompactOperator_of_orthonormal
• CompactSpectral.tendsto_norm_apply_of_isCompactOperator_of_orthonormal

theorem CompactSpectral.tendsto_zero_weakSpace_of_orthonormal {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {e : ℕ → E} (he : Orthonormal 𝕜 e) : Filter.Tendsto (have ew := fun (n : ℕ) => e n; ew) Filter.atTop (nhds 0)

An orthonormal sequence converges to 0 in the weak topology (WeakSpace).

theorem CompactSpectral.tendsto_zero_apply_of_isCompactOperator_of_orthonormal {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) (hTc : IsCompactOperator ⇑T) {e : ℕ → E} (he : Orthonormal 𝕜 e) : Filter.Tendsto (fun (n : ℕ) => T (e n)) Filter.atTop (nhds 0)

A compact operator sends an orthonormal sequence to a strongly-null sequence.

theorem CompactSpectral.tendsto_norm_apply_of_isCompactOperator_of_orthonormal {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) (hTc : IsCompactOperator ⇑T) {e : ℕ → E} (he : Orthonormal 𝕜 e) : Filter.Tendsto (fun (n : ℕ) => ‖T (e n)‖) Filter.atTop (nhds 0)

A compact operator sends an orthonormal sequence to a norm-null sequence.