The trace-class operator-ideal family

The trace-class family assigns to a bounded operator T between real or complex Hilbert spaces its nuclear gauge ν(T) = ∑' n, aₙ(T), the extended sum of its zero-based approximation numbers (ContinuousLinearMap.nuclearENorm). The four operator-ideal laws are the subadditivity, homogeneity, operator-norm domination and two-sided ideal inequality of the nuclear gauge, and adjoint invariance of the approximation numbers makes the diagonal family symmetric.

An operator lies in the trace-class ideal exactly when its approximation numbers are summable. Finite nuclear gauge forces compactness (ContinuousLinearMap.isCompactOperator_of_nuclearENorm_ne_top), while the identity of an infinite-dimensional Hilbert space has infinite nuclear gauge (ContinuousLinearMap.nuclearENorm_id_eq_top) and so is a bounded operator outside the ideal. The nuclear gauge is lower semicontinuous in operator norm, so the normed carriers are complete. The trace-class family is the p = 1 member of the Schatten scale.

Main declarations

• TauCeti.OperatorIdealFamily.traceClass: the trace-class operator-ideal family.
• TauCeti.OperatorIdealFamily.gauge_traceClass: its gauge is the nuclear gauge.
• TauCeti.OperatorIdealFamily.mem_finiteSubmodule_traceClass_iff: membership in the ideal is summability of the approximation numbers.
• TauCeti.OperatorIdealFamily.traceClass_isComplete: its normed carriers are complete.
• TauCeti.OperatorIdealFamily.schatten_one: the Schatten family at p = 1 is the trace-class family.
• TauCeti.SymmetricOperatorIdealFamily.traceClass: the adjoint-invariant diagonal family.

References

• B. Simon, Trace Ideals and Their Applications, second edition, AMS, 2005, Chapters 1–2.
• A. Pietsch, Eigenvalues and s-Numbers, Cambridge University Press, 1987, Chapter 2.

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

The trace-class operator-ideal family, whose gauge is the nuclear gauge ν(T) = ∑' n, aₙ(T): the extended sum of the approximation numbers.

@[simp]

theorem TauCeti.OperatorIdealFamily.gauge_traceClass {𝕜 : 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) : (traceClass 𝕜).gauge T = T.nuclearENorm

The trace-class gauge is the nuclear gauge.

theorem TauCeti.OperatorIdealFamily.mem_finiteSubmodule_traceClass_iff {𝕜 : 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) : T ∈ ((traceClass 𝕜).operatorGauge E F).finiteSubmodule ↔ Summable T.singularValue

An operator is trace class exactly when its approximation numbers are summable.

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

The trace-class operator-ideal family has complete normed carriers.

theorem TauCeti.OperatorIdealFamily.schatten_one {𝕜 : Type u} [RCLike 𝕜] : schatten 𝕜 1 ⋯ = traceClass 𝕜

The trace-class endpoint of the Schatten scale. The Schatten family at p = 1 is the trace-class family.

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

The adjoint-invariant diagonal-universe trace-class family.

@[simp]

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

The underlying rectangular family of the symmetric trace-class family.

theorem TauCeti.SymmetricOperatorIdealFamily.schatten_one (𝕜 : Type u) [RCLike 𝕜] : schatten 𝕜 1 ⋯ = traceClass 𝕜

The symmetric Schatten family at p = 1 is the symmetric trace-class family.