Finite-exponent Schatten operator ideals

The Schatten family for a finite real exponent p ≥ 1 is the operator-ideal family induced by the ℓᵖ symmetric gauge. Its gauge on a bounded map T between real or complex Hilbert spaces is (∑' n, aₙ(T)^p)^(1/p), where aₙ are the zero-based approximation numbers. In particular, membership is equivalent to summability of their p-th powers.

The family inherits the triangle inequality, homogeneity, domination of the operator norm, two-sided ideal inequalities and adjoint invariance from the symmetric-gauge construction. Its normed carriers are complete, since the gauge is lower semicontinuous in operator norm.

The Schatten gauges decrease as the exponent grows, because ℓᵖ norms do; hence the Schatten ideals increase with p, S_p ⊆ S_q for 1 ≤ p ≤ q. The endpoints p = 1 and p = 2 are the trace-class and Hilbert–Schmidt families, and the operator-norm family is the endpoint p = ∞ (TauCeti.SymmetricGauge.operatorIdealFamily_supGauge).

References

• B. Simon, Trace Ideals and Their Applications, second edition, AMS, 2005, Chapter 2.

noncomputable def TauCeti.OperatorIdealFamily.schatten (𝕜 : Type u) [RCLike 𝕜] (p : ℝ) (hp : 1 ≤ p) : OperatorIdealFamily 𝕜

The Schatten p operator-ideal family, induced by the ℓᵖ symmetric gauge.

theorem TauCeti.OperatorIdealFamily.schatten_def (𝕜 : Type u) [RCLike 𝕜] (p : ℝ) (hp : 1 ≤ p) : schatten 𝕜 p hp = SymmetricGauge.operatorIdealFamily 𝕜 (SymmetricGauge.lpGauge p hp)

The Schatten p family is the family induced by the ℓᵖ symmetric gauge.

@[simp]

theorem TauCeti.OperatorIdealFamily.gauge_schatten {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (p : ℝ) (hp : 1 ≤ p) (T : E →L[𝕜] F) : (schatten 𝕜 p hp).gauge T = (∑' (n : ℕ), ↑(T.singularValue n) ^ p) ^ (1 / p)

The Schatten gauge is the ℓᵖ sum of the approximation numbers, with value ∞ when that power sum diverges.

theorem TauCeti.OperatorIdealFamily.mem_finiteSubmodule_schatten_iff {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (p : ℝ) (hp : 1 ≤ p) (T : E →L[𝕜] F) : T ∈ ((schatten 𝕜 p hp).operatorGauge E F).finiteSubmodule ↔ Summable fun (n : ℕ) => T.singularValue n ^ p

An operator belongs to the Schatten p ideal exactly when the p-th powers of its approximation numbers are summable.

theorem TauCeti.OperatorIdealFamily.lowerSemicontinuous_gauge_schatten {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (p : ℝ) (hp : 1 ≤ p) : LowerSemicontinuous fun (T : E →L[𝕜] F) => (schatten 𝕜 p hp).gauge T

The Schatten gauge is lower semicontinuous in the operator-norm topology.

theorem TauCeti.OperatorIdealFamily.gauge_schatten_le_of_le {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {p q : ℝ} (hp : 1 ≤ p) (hq : 1 ≤ q) (hpq : p ≤ q) (T : E →L[𝕜] F) : (schatten 𝕜 q hq).gauge T ≤ (schatten 𝕜 p hp).gauge T

Monotonicity of the Schatten scale. For 1 ≤ p ≤ q, the Schatten q gauge of an operator is at most its Schatten p gauge.

theorem TauCeti.OperatorIdealFamily.finiteSubmodule_schatten_le_of_le {𝕜 : Type u} [RCLike 𝕜] (E : Type v) (F : Type w) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {p q : ℝ} (hp : 1 ≤ p) (hq : 1 ≤ q) (hpq : p ≤ q) : ((schatten 𝕜 p hp).operatorGauge E F).finiteSubmodule ≤ ((schatten 𝕜 q hq).operatorGauge E F).finiteSubmodule

Inclusion of Schatten ideals. For 1 ≤ p ≤ q, every operator in the Schatten p ideal lies in the Schatten q ideal.

instance TauCeti.OperatorIdealFamily.schatten_isComplete {𝕜 : Type u} [RCLike 𝕜] (p : ℝ) (hp : 1 ≤ p) : (schatten 𝕜 p hp).IsComplete

Every finite-exponent Schatten ideal has complete normed carriers.

noncomputable def TauCeti.SymmetricOperatorIdealFamily.schatten (𝕜 : Type u) [RCLike 𝕜] (p : ℝ) (hp : 1 ≤ p) : SymmetricOperatorIdealFamily 𝕜

The adjoint-invariant diagonal-universe Schatten p family.

@[simp]

theorem TauCeti.SymmetricOperatorIdealFamily.schatten_toOperatorIdealFamily (𝕜 : Type u) [RCLike 𝕜] (p : ℝ) (hp : 1 ≤ p) : (schatten 𝕜 p hp).toOperatorIdealFamily = OperatorIdealFamily.schatten 𝕜 p hp

The underlying rectangular family of the symmetric Schatten family.