Hilbert–Schmidt energy and approximation numbers

For a bounded operator T : E →L[𝕜] F from a Hilbert space to an inner product space and a Hilbert basis (bᵢ) of the source, the Hilbert–Schmidt energy E_b(T) = ∑' i, ‖T bᵢ‖ₑ² is defined by an orthonormal expansion, without any spectral theory. This file proves that it is the sum of the squares of the approximation numbers:

∑' n, aₙ(T)² = E_b(T) in ℝ≥0∞.

So the Hilbert–Schmidt class, defined through columns, is the class of operators whose approximation-number sequence is square-summable, and the Hilbert–Schmidt norm is the ℓ² norm of that sequence. This is the p = 2 case of the identification of Schatten classes defined by approximation numbers with their concrete models.

Both inequalities go through finite-dimensional compressions. For a finite-dimensional subspace V ≤ E, the compression C : V → T(V), C x = P_{T(V)} (T x), has approximation numbers at most those of T and energy at most that of T. Between finite-dimensional spaces, Eckart–Young identifies the approximation numbers of C with its singular values, and the energy of C is the square of its Frobenius seminorm, the sum of the squared singular values.

• E_b(T) ≤ ∑' n, aₙ(T)²: each finite partial sum ∑_{i ∈ s} ‖T bᵢ‖² is the energy of the compression of T to the span of the bᵢ with i ∈ s. This direction needs no completeness.
• ∑' n, aₙ(T)² ≤ E_b(T): on a complete source, the converse min–max localization supplies, for every k and δ > 0, a compression C with aₙ(T) ≤ aₙ(C) + δ for all n < k. Letting δ → 0 bounds every partial sum ∑_{n < k} aₙ(T)² by E_b(T).

Main results

• ContinuousLinearMap.hilbertSchmidtEnergy_le_tsum_singularValue_sq: E_b(T) ≤ ∑' n, aₙ(T)².
• ContinuousLinearMap.tsum_singularValue_sq_le_hilbertSchmidtEnergy: ∑' n, aₙ(T)² ≤ E_b(T).
• ContinuousLinearMap.tsum_singularValue_sq_eq_hilbertSchmidtEnergy: ∑' n, aₙ(T)² = E_b(T).
• ContinuousLinearMap.hilbertSchmidtEnergy_ne_top_iff_summable_singularValue_sq: T has finite energy exactly when n ↦ aₙ(T)² is summable.
• ContinuousLinearMap.sq_hilbertSchmidtNorm_eq_tsum_singularValue_sq: ‖T‖_HS² = ∑' n, aₙ(T)².

References

• A. Pietsch, Eigenvalues and s-Numbers, Cambridge Studies in Advanced Mathematics 13, Cambridge University Press (1987), Chapter 2.
• B. Simon, Trace Ideals and Their Applications, second edition, Mathematical Surveys and Monographs 120, American Mathematical Society, 2005, Section 2.

theorem ContinuousLinearMap.hilbertSchmidtEnergy_le_tsum_singularValue_sq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) : T.hilbertSchmidtEnergy b ≤ ∑' (n : ℕ), ↑(T.singularValue n) ^ 2

Lower half of the Hilbert–Schmidt reconciliation. The Hilbert–Schmidt energy is at most the sum of the squared approximation numbers: E_b(T) ≤ ∑' n, aₙ(T)². No completeness is needed.

theorem ContinuousLinearMap.tsum_singularValue_sq_le_hilbertSchmidtEnergy {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] (T : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) : ∑' (n : ℕ), ↑(T.singularValue n) ^ 2 ≤ T.hilbertSchmidtEnergy b

Upper half of the Hilbert–Schmidt reconciliation. For a bounded operator from a Hilbert space to an inner product space, the sum of the squared approximation numbers is at most the Hilbert–Schmidt energy: ∑' n, aₙ(T)² ≤ E_b(T).

theorem ContinuousLinearMap.tsum_singularValue_sq_eq_hilbertSchmidtEnergy {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] (T : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) : ∑' (n : ℕ), ↑(T.singularValue n) ^ 2 = T.hilbertSchmidtEnergy b

Hilbert–Schmidt reconciliation. For a bounded operator from a Hilbert space to an inner product space and any Hilbert basis (bᵢ) of the source, the sum of the squared approximation numbers is the Hilbert–Schmidt energy: ∑' n, aₙ(T)² = ∑' i, ‖T bᵢ‖² in ℝ≥0∞.

theorem ContinuousLinearMap.hilbertSchmidtEnergy_ne_top_iff_summable_singularValue_sq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] (T : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) : T.hilbertSchmidtEnergy b ≠ ⊤ ↔ Summable fun (n : ℕ) => ↑(T.singularValue n) ^ 2

An operator from a Hilbert space to an inner product space has finite Hilbert–Schmidt energy exactly when its approximation numbers are square-summable.

theorem ContinuousLinearMap.sq_hilbertSchmidtNorm_eq_tsum_singularValue_sq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (T : E →L[𝕜] F) : T.hilbertSchmidtNorm ^ 2 = ∑' (n : ℕ), ↑(T.singularValue n) ^ 2

The square of the Hilbert–Schmidt norm is the sum of the squared approximation numbers, ‖T‖_HS² = ∑' n, aₙ(T)². When T has infinite energy both sides are 0.