The Hilbert–Schmidt operator-ideal family

The Hilbert–Schmidt family assigns to a bounded operator T between real or complex Hilbert spaces the square root E_b(T)^(1/2) of its Hilbert–Schmidt energy E_b(T) = ∑' i, ‖T bᵢ‖ₑ², computed in any Hilbert basis (bᵢ) of the source. The four operator-ideal laws come directly from the geometry of the energy, without approximation numbers: subadditivity is Minkowski's inequality for unconditional sums in ℝ≥0∞, homogeneity is the scaling of the energy, domination of the operator norm and the two-sided ideal inequality are the energy bounds ‖T‖ₑ² ≤ E_b(T) and E(A T B) ≤ ‖A‖ₑ² E(T) ‖B‖ₑ². Adjoint invariance of the energy makes the diagonal family symmetric.

An operator lies in the ideal exactly when its energy is finite, and there the ideal norm is the Hilbert–Schmidt norm ContinuousLinearMap.hilbertSchmidtNorm. The energy is the sum of the squared approximation numbers, so the Hilbert–Schmidt family is the p = 2 member of the Schatten scale; in particular its normed carriers are complete.

Main declarations

• TauCeti.OperatorIdealFamily.hilbertSchmidt: the Hilbert–Schmidt operator-ideal family.
• TauCeti.OperatorIdealFamily.gauge_hilbertSchmidt: its gauge is E_b(T)^(1/2) for every Hilbert basis b of the source.
• TauCeti.OperatorIdealFamily.mem_finiteSubmodule_hilbertSchmidt_iff: membership in the ideal is finiteness of the energy.
• TauCeti.OperatorIdealFamily.toReal_gauge_hilbertSchmidt: the ideal norm is the Hilbert–Schmidt norm.
• TauCeti.OperatorIdealFamily.schatten_two: the Schatten family at p = 2 is the Hilbert–Schmidt family.
• TauCeti.OperatorIdealFamily.hilbertSchmidt_isComplete: its normed carriers are complete.
• TauCeti.SymmetricOperatorIdealFamily.hilbertSchmidt: the adjoint-invariant diagonal family.

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, AMS, 2005, Chapter 2.

noncomputable def TauCeti.OperatorIdealFamily.hilbertSchmidt (𝕜 : Type u) [RCLike 𝕜] : OperatorIdealFamily 𝕜

The Hilbert–Schmidt operator-ideal family. Its gauge is the square root E_b(T)^(1/2) of the Hilbert–Schmidt energy, computed in a Hilbert basis b of the source chosen once and for all; by gauge_hilbertSchmidt every Hilbert basis gives the same value.

theorem TauCeti.OperatorIdealFamily.gauge_hilbertSchmidt {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {ι : Type u_1} (T : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) : (hilbertSchmidt 𝕜).gauge T = T.hilbertSchmidtEnergy b ^ (1 / 2)

The Hilbert–Schmidt gauge is the square root of the Hilbert–Schmidt energy, computed in any Hilbert basis of the source.

theorem TauCeti.OperatorIdealFamily.mem_finiteSubmodule_hilbertSchmidt_iff {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {ι : Type u_1} (T : E →L[𝕜] F) (b : HilbertBasis ι 𝕜 E) : T ∈ ((hilbertSchmidt 𝕜).operatorGauge E F).finiteSubmodule ↔ T.hilbertSchmidtEnergy b ≠ ⊤

An operator belongs to the Hilbert–Schmidt ideal exactly when its Hilbert–Schmidt energy is finite, in any Hilbert basis of the source.

@[simp]

theorem TauCeti.OperatorIdealFamily.toReal_gauge_hilbertSchmidt {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : ((hilbertSchmidt 𝕜).gauge T).toReal = T.hilbertSchmidtNorm

The real value of the Hilbert–Schmidt gauge is the Hilbert–Schmidt norm. On the ideal this is the norm of the carrier.

theorem TauCeti.OperatorIdealFamily.schatten_two {𝕜 : Type u} [RCLike 𝕜] : schatten 𝕜 2 ⋯ = hilbertSchmidt 𝕜

The Hilbert–Schmidt endpoint of the Schatten scale. The Schatten family at p = 2 is the Hilbert–Schmidt family: the sum of the squared approximation numbers is the Hilbert–Schmidt energy.

instance TauCeti.OperatorIdealFamily.hilbertSchmidt_isComplete {𝕜 : Type u} [RCLike 𝕜] : (hilbertSchmidt 𝕜).IsComplete

The Hilbert–Schmidt operator-ideal family has complete normed carriers.

noncomputable def TauCeti.SymmetricOperatorIdealFamily.hilbertSchmidt (𝕜 : Type u) [RCLike 𝕜] : SymmetricOperatorIdealFamily 𝕜

The adjoint-invariant diagonal-universe Hilbert–Schmidt family.

@[simp]

theorem TauCeti.SymmetricOperatorIdealFamily.hilbertSchmidt_toOperatorIdealFamily (𝕜 : Type u) [RCLike 𝕜] : (hilbertSchmidt 𝕜).toOperatorIdealFamily = OperatorIdealFamily.hilbertSchmidt 𝕜

The underlying rectangular family of the symmetric Hilbert–Schmidt family.

theorem TauCeti.SymmetricOperatorIdealFamily.schatten_two (𝕜 : Type u) [RCLike 𝕜] : schatten 𝕜 2 ⋯ = hilbertSchmidt 𝕜

The symmetric Schatten family at p = 2 is the symmetric Hilbert–Schmidt family.