Hilbert–Schmidt energy and the Hilbert–Schmidt norm

For a bounded operator T : E →L[𝕜] F between Hilbert spaces and a Hilbert basis (bᵢ) of the source, the Hilbert–Schmidt energy is the unconditional sum E_b(T) = ∑' i, ‖T bᵢ‖ₑ² in ℝ≥0∞. Working in ℝ≥0∞ means that no summability hypothesis is ever needed: an operator that is not Hilbert–Schmidt simply has energy ∞, and iterated sums may be exchanged freely.

Expanding each column T bᵢ in a Hilbert basis (cⱼ) of the target by Parseval writes the energy as the double sum ∑' i, ∑' j, ‖⟪cⱼ, T bᵢ⟫‖ₑ². Exchanging the two sums identifies it with the energy of the adjoint, E_b(T) = E_c(T†), and applying this twice shows that E_b(T) does not depend on the basis b. Its square root therefore defines a basis-free Hilbert–Schmidt norm ‖T‖_HS, which is invariant under taking adjoints and homogeneous under scalar multiplication. For operators of finite energy it dominates the operator norm and satisfies the two-sided ideal inequality ‖A T B‖_HS ≤ ‖A‖ ‖T‖_HS ‖B‖; an operator of infinite energy has ‖T‖_HS = 0. The square root of the energy satisfies the triangle inequality, by Minkowski's inequality for unconditional sums in ℝ≥0∞, so the Hilbert–Schmidt norm is subadditive on operators of finite energy. On a finite-dimensional source the energy is the square of the Frobenius seminorm TauCeti.UnitarilyInvariantSeminorm.frobenius.

These are the norm estimates behind the Hilbert–Schmidt class of operators: its identification with ℓ² families of columns, and the compactness of Hilbert–Schmidt operators.

Main definitions

• ContinuousLinearMap.hilbertSchmidtEnergy T b: the energy ∑' i, ‖T bᵢ‖ₑ² in ℝ≥0∞.
• ContinuousLinearMap.hilbertSchmidtNorm T: the Hilbert–Schmidt norm √(E_b(T)).toReal, computed in any Hilbert basis b of the source.

Main results

• ContinuousLinearMap.hilbertSchmidtEnergy_eq_tsum_tsum: the Parseval expansion E_b(T) = ∑' i, ∑' j, ‖⟪cⱼ, T bᵢ⟫‖ₑ².
• ContinuousLinearMap.hilbertSchmidtEnergy_adjoint: E_c(T†) = E_b(T).
• ContinuousLinearMap.hilbertSchmidtEnergy_indep: the energy is independent of the basis.
• ContinuousLinearMap.enorm_sq_le_hilbertSchmidtEnergy: ‖T‖ₑ² ≤ E_b(T).
• ContinuousLinearMap.hilbertSchmidtEnergy_comp_le_left and ContinuousLinearMap.hilbertSchmidtEnergy_comp_le_right: one-sided ideal bounds for the energy.
• ContinuousLinearMap.hilbertSchmidtEnergy_comp_comp_le: E(A T B) ≤ ‖A‖ₑ² E(T) ‖B‖ₑ².
• ContinuousLinearMap.rpow_hilbertSchmidtEnergy_add_le: the triangle inequality E_b(S + T)^(1/2) ≤ E_b(S)^(1/2) + E_b(T)^(1/2).
• ContinuousLinearMap.hilbertSchmidtEnergy_smul and ContinuousLinearMap.hilbertSchmidtNorm_smul: homogeneity, E_b(c • T) = ‖c‖ₑ² E_b(T) and ‖c • T‖_HS = ‖c‖ ‖T‖_HS.
• ContinuousLinearMap.hilbertSchmidtNorm_adjoint: ‖T†‖_HS = ‖T‖_HS, for every operator.
• ContinuousLinearMap.hilbertSchmidtNorm_add_le: ‖S + T‖_HS ≤ ‖S‖_HS + ‖T‖_HS for operators of finite energy.
• ContinuousLinearMap.norm_le_hilbertSchmidtNorm and ContinuousLinearMap.hilbertSchmidtNorm_comp_comp_le: domination of the operator norm and the two-sided ideal inequality for the Hilbert–Schmidt norm of a finite-energy operator.
• ContinuousLinearMap.hilbertSchmidtEnergy_eq_ofReal_sq_frobenius: on a finite-dimensional source, E_b(T) = ‖T‖_F².

References

• M. Reed and B. Simon, Methods of Modern Mathematical Physics I: Functional Analysis, revised edition, Academic Press, 1980, Section VI.6.
• B. Simon, Trace Ideals and Their Applications, second edition, Mathematical Surveys and Monographs 120, American Mathematical Society, 2005, Section 2.

noncomputable def ContinuousLinearMap.hilbertSchmidtEnergy {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) : ENNReal

The Hilbert–Schmidt energy E_b(T) = ∑' i, ‖T bᵢ‖ₑ² of a bounded operator T relative to a Hilbert basis (bᵢ) of its source. It takes values in ℝ≥0∞, and is finite exactly for the Hilbert–Schmidt operators. It does not depend on b, see hilbertSchmidtEnergy_indep.

theorem ContinuousLinearMap.hilbertSchmidtEnergy_def {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) : T.hilbertSchmidtEnergy b = ∑' (i : ι), ‖T (b i)‖ₑ ^ 2

theorem ContinuousLinearMap.hilbertSchmidtEnergy_eq_tsum_tsum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_6} {κ : Type u_8} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) (c : HilbertBasis κ 𝕜 F) : T.hilbertSchmidtEnergy b = ∑' (i : ι) (j : κ), ‖inner 𝕜 (c j) (T (b i))‖ₑ ^ 2

Parseval expansion of the Hilbert–Schmidt energy. Expanding each column T bᵢ in a Hilbert basis (cⱼ) of the target gives E_b(T) = ∑' i, ∑' j, ‖⟪cⱼ, T bᵢ⟫‖ₑ².

@[simp]

theorem ContinuousLinearMap.hilbertSchmidtEnergy_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (b : HilbertBasis ι 𝕜 E) : hilbertSchmidtEnergy 0 b = 0

@[simp]

theorem ContinuousLinearMap.hilbertSchmidtEnergy_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (c : 𝕜) (T : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) : (c • T).hilbertSchmidtEnergy b = ‖c‖ₑ ^ 2 * T.hilbertSchmidtEnergy b

The energy is homogeneous of degree two: E_b(c • T) = ‖c‖ₑ² E_b(T).

theorem ContinuousLinearMap.hilbertSchmidtEnergy_comp_le_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {ι : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (A : F →L[𝕜] G) (T : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) : (A ∘SL T).hilbertSchmidtEnergy b ≤ ‖A‖ₑ ^ 2 * T.hilbertSchmidtEnergy b

Composition on the left with a bounded operator scales the energy by at most ‖A‖ₑ².

theorem ContinuousLinearMap.rpow_hilbertSchmidtEnergy_add_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (S T : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) : (S + T).hilbertSchmidtEnergy b ^ (1 / 2) ≤ S.hilbertSchmidtEnergy b ^ (1 / 2) + T.hilbertSchmidtEnergy b ^ (1 / 2)

Triangle inequality for the Hilbert–Schmidt energy. The square root of the energy is subadditive: E_b(S + T)^(1/2) ≤ E_b(S)^(1/2) + E_b(T)^(1/2), with no finiteness assumption.

theorem ContinuousLinearMap.hilbertSchmidtEnergy_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_6} {κ : Type u_8} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (T : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) (c : HilbertBasis κ 𝕜 F) : (adjoint T).hilbertSchmidtEnergy c = T.hilbertSchmidtEnergy b

Adjoint energy swap. For Hilbert bases (bᵢ) of the source and (cⱼ) of the target, the energy of T† relative to c equals the energy of T relative to b: both are the double sum ∑ ‖⟪cⱼ, T bᵢ⟫‖ₑ², summed in the two possible orders.

theorem ContinuousLinearMap.hilbertSchmidtEnergy_indep {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_6} {ι' : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (T : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) (b' : HilbertBasis ι' 𝕜 E) : T.hilbertSchmidtEnergy b = T.hilbertSchmidtEnergy b'

Basis independence of the Hilbert–Schmidt energy. Any two Hilbert bases of the source give the same energy.

theorem ContinuousLinearMap.hilbertSchmidtEnergy_comp_le_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {ι : Type u_6} {ι' : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [CompleteSpace E] [CompleteSpace F] [CompleteSpace G] (T : F →L[𝕜] G) (B : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) (c : HilbertBasis ι' 𝕜 F) : (T ∘SL B).hilbertSchmidtEnergy b ≤ T.hilbertSchmidtEnergy c * ‖B‖ₑ ^ 2

Composition on the right with a bounded operator scales the energy by at most ‖B‖ₑ². The two energies may be computed in Hilbert bases of different spaces.

theorem ContinuousLinearMap.hilbertSchmidtEnergy_comp_comp_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} {ι : Type u_6} {ι' : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace E] [CompleteSpace F] [CompleteSpace G] (A : G →L[𝕜] H) (T : F →L[𝕜] G) (B : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) (c : HilbertBasis ι' 𝕜 F) : (A ∘SL T ∘SL B).hilbertSchmidtEnergy b ≤ ‖A‖ₑ ^ 2 * T.hilbertSchmidtEnergy c * ‖B‖ₑ ^ 2

Two-sided ideal inequality for the energy. E_b(A T B) ≤ ‖A‖ₑ² E_c(T) ‖B‖ₑ², where b and c are Hilbert bases of the sources of B and T.

theorem ContinuousLinearMap.enorm_sq_le_hilbertSchmidtEnergy {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (T : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) : ‖T‖ₑ ^ 2 ≤ T.hilbertSchmidtEnergy b

Hilbert–Schmidt domination of the operator norm, in energy form: ‖T‖ₑ² ≤ E_b(T).

theorem ContinuousLinearMap.hilbertSchmidtEnergy_eq_ofReal_sq_frobenius {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] [FiniteDimensional 𝕜 E] (T : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) : T.hilbertSchmidtEnergy b = ENNReal.ofReal ((TauCeti.UnitarilyInvariantSeminorm.frobenius 𝕜 E F) ↑T ^ 2)

On a finite-dimensional source, the Hilbert–Schmidt energy is the square of the Frobenius seminorm TauCeti.UnitarilyInvariantSeminorm.frobenius.

noncomputable def ContinuousLinearMap.hilbertSchmidtNorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] (T : E →L[𝕜] F) : ℝ

The Hilbert–Schmidt norm ‖T‖_HS = √(E_b(T)).toReal of a bounded operator, computed in a Hilbert basis b of the source chosen once and for all; by hilbertSchmidtNorm_eq_sqrt any Hilbert basis gives the same value. It is meaningful for operators of finite energy: an operator of infinite energy has Hilbert–Schmidt norm 0.

theorem ContinuousLinearMap.hilbertSchmidtNorm_eq_sqrt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (T : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) : T.hilbertSchmidtNorm = √(T.hilbertSchmidtEnergy b).toReal

The Hilbert–Schmidt norm may be computed in any Hilbert basis of the source.

theorem ContinuousLinearMap.hilbertSchmidtNorm_eq_toReal_rpow {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (T : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) : T.hilbertSchmidtNorm = (T.hilbertSchmidtEnergy b ^ (1 / 2)).toReal

The Hilbert–Schmidt norm is the real value of the square root E_b(T)^(1/2) of the energy, computed in any Hilbert basis of the source.

theorem ContinuousLinearMap.hilbertSchmidtNorm_nonneg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] (T : E →L[𝕜] F) : 0 ≤ T.hilbertSchmidtNorm

theorem ContinuousLinearMap.sq_hilbertSchmidtNorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (T : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) : T.hilbertSchmidtNorm ^ 2 = (T.hilbertSchmidtEnergy b).toReal

The square of the Hilbert–Schmidt norm is the real value of the energy.

theorem ContinuousLinearMap.ofReal_sq_hilbertSchmidtNorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (T : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) (h : T.hilbertSchmidtEnergy b ≠ ⊤) : ENNReal.ofReal (T.hilbertSchmidtNorm ^ 2) = T.hilbertSchmidtEnergy b

For an operator of finite energy, the square of the Hilbert–Schmidt norm recovers the energy without loss.

@[simp]

theorem ContinuousLinearMap.hilbertSchmidtNorm_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] : hilbertSchmidtNorm 0 = 0

@[simp]

theorem ContinuousLinearMap.hilbertSchmidtNorm_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] (c : 𝕜) (T : E →L[𝕜] F) : (c • T).hilbertSchmidtNorm = ‖c‖ * T.hilbertSchmidtNorm

Homogeneity of the Hilbert–Schmidt norm. ‖c • T‖_HS = ‖c‖ ‖T‖_HS, for every operator.

theorem ContinuousLinearMap.hilbertSchmidtNorm_add_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (S T : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) (hS : S.hilbertSchmidtEnergy b ≠ ⊤) (hT : T.hilbertSchmidtEnergy b ≠ ⊤) : (S + T).hilbertSchmidtNorm ≤ S.hilbertSchmidtNorm + T.hilbertSchmidtNorm

Triangle inequality for the Hilbert–Schmidt norm. If S and T have finite energy, then ‖S + T‖_HS ≤ ‖S‖_HS + ‖T‖_HS.

theorem ContinuousLinearMap.norm_le_hilbertSchmidtNorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (T : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) (h : T.hilbertSchmidtEnergy b ≠ ⊤) : ‖T‖ ≤ T.hilbertSchmidtNorm

Hilbert–Schmidt domination of the operator norm. An operator of finite energy satisfies ‖T‖ ≤ ‖T‖_HS.

@[simp]

theorem ContinuousLinearMap.hilbertSchmidtNorm_adjoint {𝕜 : 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) : (adjoint T).hilbertSchmidtNorm = T.hilbertSchmidtNorm

Adjoint invariance of the Hilbert–Schmidt norm. ‖T†‖_HS = ‖T‖_HS.

theorem ContinuousLinearMap.hilbertSchmidtNorm_comp_comp_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} {ι' : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace E] [CompleteSpace F] [CompleteSpace G] [CompleteSpace H] (A : G →L[𝕜] H) (T : F →L[𝕜] G) (B : E →L[𝕜] F) (c : HilbertBasis ι' 𝕜 F) (h : T.hilbertSchmidtEnergy c ≠ ⊤) : (A ∘SL T ∘SL B).hilbertSchmidtNorm ≤ ‖A‖ * T.hilbertSchmidtNorm * ‖B‖

Two-sided ideal inequality for the Hilbert–Schmidt norm. If T has finite energy, then ‖A T B‖_HS ≤ ‖A‖ ‖T‖_HS ‖B‖.