The operator-ideal family induced by a symmetric gauge

A symmetric gauge Φ on finitely supported nonnegative sequences extends to a gauge Φ∞ on all ℝ≥0∞-valued sequences (TauCeti.SymmetricGauge.extend). Applying Φ∞ to the approximation numbers of a bounded operator gives the extended gauge Φ(T) = Φ∞(n ↦ aₙ(T)). Its finite locus is the symmetrically normed operator ideal attached to Φ: the supremum gauge gives the operator norm, the sum gives the nuclear gauge, and the ℓᵖ gauges give the Schatten classes.

The induced gauge is absolutely homogeneous, dominates the operator norm and satisfies the two-sided ideal inequality on bounded maps between arbitrary seminormed spaces, because the approximation numbers have these properties termwise. It depends only on the approximation-number sequence, so it is unchanged under adjoints of Hilbert-space operators. It is monotone for Ky Fan domination: since symmetric gauges are monotone for weak majorization of antitone sequences, if every Ky Fan prefix Kₖ(S) is at most Kₖ(T) then Φ(S) ≤ Φ(T). Combined with the Ky Fan triangle inequality Kₖ(S + T) ≤ Kₖ(S) + Kₖ(T) and the subadditivity of Φ∞, this gives subadditivity of the induced gauge on Hilbert spaces.

These four laws make the induced gauges an operator-ideal family over every pair of Hilbert spaces, and adjoint invariance makes its diagonal-universe restriction a symmetric family.

Since the approximation numbers decrease from a₀(T) = ‖T‖, the supremum gauge induces the operator-norm family: it is the p = ∞ endpoint of the Schatten scale.

Main definitions

• TauCeti.SymmetricGauge.opGauge: the gauge Φ(T) = Φ∞(n ↦ aₙ(T)) of a bounded map.
• TauCeti.SymmetricGauge.operatorIdealFamily: the rectangular operator-ideal family with gauge Φ(T).
• TauCeti.SymmetricGauge.symmetricOperatorIdealFamily: its adjoint-invariant view on the diagonal universe.

Main results

• TauCeti.SymmetricGauge.enorm_le_opGauge: ‖T‖ ≤ Φ(T).
• TauCeti.SymmetricGauge.opGauge_supGauge: the supremum gauge induces the operator norm.
• TauCeti.SymmetricGauge.operatorIdealFamily_supGauge: the family induced by the supremum gauge is the operator-norm family.
• TauCeti.SymmetricGauge.opGauge_smul: Φ(c T) = ‖c‖ Φ(T).
• TauCeti.SymmetricGauge.opGauge_comp_comp_le: Φ(A T B) ≤ ‖A‖ Φ(T) ‖B‖.
• TauCeti.SymmetricGauge.opGauge_comp_comp_le_self: Φ(A T B) ≤ Φ(T) for contractions A, B.
• TauCeti.SymmetricGauge.opGauge_le_of_forall_kyFanGauge_le: Ky Fan domination implies domination of the induced gauges.
• TauCeti.SymmetricGauge.opGauge_add_le: Φ(S + T) ≤ Φ(S) + Φ(T) for maps out of a Hilbert space.
• TauCeti.SymmetricGauge.opGauge_adjoint: Φ(T†) = Φ(T), with source and target in arbitrary universes.
• TauCeti.SymmetricGauge.opGauge_eq_of_sameSingularValues: operators with the same approximation numbers have the same induced gauge.

References

• I. C. Gohberg, M. G. Krein, Introduction to the Theory of Linear Nonselfadjoint Operators in Hilbert Space, Translations of Mathematical Monographs 18, AMS (1969), Chapter III.
• B. Simon, Trace Ideals and Their Applications, 2nd ed., Mathematical Surveys and Monographs 120, AMS (2005), Chapter 1.

noncomputable def TauCeti.SymmetricGauge.opGauge (Φ : SymmetricGauge) {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) : ENNReal

The gauge Φ(T) = Φ∞(n ↦ aₙ(T)) induced by a symmetric gauge Φ on a bounded linear map T: the extension of Φ evaluated on the approximation numbers of T. On Hilbert spaces its finite values select the symmetrically normed operator ideal attached to Φ.

theorem TauCeti.SymmetricGauge.opGauge_def (Φ : SymmetricGauge) {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) : Φ.opGauge T = Φ.extend fun (n : ℕ) => ↑(T.singularValue n)

The induced gauge is the extended symmetric gauge of the approximation numbers.

theorem TauCeti.SymmetricGauge.enorm_le_opGauge (Φ : SymmetricGauge) {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) : ‖T‖ₑ ≤ Φ.opGauge T

The induced gauge dominates the operator norm.

@[simp]

theorem TauCeti.SymmetricGauge.opGauge_supGauge {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) : supGauge.opGauge T = ‖T‖ₑ

The supremum gauge induces the operator norm: supₙ aₙ(T) = ‖T‖.

@[simp]

theorem TauCeti.SymmetricGauge.opGauge_smul (Φ : SymmetricGauge) {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (c : 𝕜) (T : E →L[𝕜] F) : Φ.opGauge (c • T) = ‖c‖ₑ * Φ.opGauge T

Absolute homogeneity of the induced gauge, including its infinite values.

@[simp]

theorem TauCeti.SymmetricGauge.opGauge_zero (Φ : SymmetricGauge) {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : Φ.opGauge 0 = 0

@[simp]

theorem TauCeti.SymmetricGauge.opGauge_neg (Φ : SymmetricGauge) {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) : Φ.opGauge (-T) = Φ.opGauge T

Negation preserves the induced gauge.

theorem TauCeti.SymmetricGauge.opGauge_comp_comp_le (Φ : SymmetricGauge) {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup H] [NormedSpace 𝕜 H] (A : G →L[𝕜] H) (T : F →L[𝕜] G) (B : E →L[𝕜] F) : Φ.opGauge (A ∘SL T ∘SL B) ≤ ‖A‖ₑ * Φ.opGauge T * ‖B‖ₑ

The induced gauge satisfies the two-sided ideal inequality Φ(A T B) ≤ ‖A‖ Φ(T) ‖B‖.

theorem TauCeti.SymmetricGauge.opGauge_comp_comp_le_self (Φ : SymmetricGauge) {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup H] [NormedSpace 𝕜 H] {A : G →L[𝕜] H} (hA : ‖A‖ ≤ 1) (T : F →L[𝕜] G) {B : E →L[𝕜] F} (hB : ‖B‖ ≤ 1) : Φ.opGauge (A ∘SL T ∘SL B) ≤ Φ.opGauge T

Composition on both sides by contractions does not increase the induced gauge.

theorem TauCeti.SymmetricGauge.opGauge_le_of_forall_kyFanGauge_le (Φ : SymmetricGauge) {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup H] [NormedSpace 𝕜 H] {S : G →L[𝕜] H} {T : E →L[𝕜] F} (h : ∀ (k : ℕ), S.kyFanGauge k ≤ T.kyFanGauge k) : Φ.opGauge S ≤ Φ.opGauge T

Ky Fan dominance. If every Ky Fan prefix of S is at most the corresponding prefix of T, then the induced gauge of S is at most that of T. The two maps may act between different spaces.

theorem TauCeti.SymmetricGauge.opGauge_eq_of_sameSingularValues (Φ : SymmetricGauge) {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup H] [NormedSpace 𝕜 H] {S : G →L[𝕜] H} {T : E →L[𝕜] F} (h : S.SameSingularValues T) : Φ.opGauge S = Φ.opGauge T

Operators with the same approximation-number sequence have the same induced gauge.

theorem TauCeti.SymmetricGauge.opGauge_add_le (Φ : SymmetricGauge) {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] (S T : E →L[𝕜] F) : Φ.opGauge (S + T) ≤ Φ.opGauge S + Φ.opGauge T

Subadditivity of the induced gauge. For bounded maps from a Hilbert space to an inner product space, Φ(S + T) ≤ Φ(S) + Φ(T).

@[simp]

theorem TauCeti.SymmetricGauge.opGauge_adjoint (Φ : SymmetricGauge) {𝕜 : 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) : Φ.opGauge (ContinuousLinearMap.adjoint T) = Φ.opGauge T

Adjoint invariance of the induced gauge. A bounded operator between Hilbert spaces and its adjoint have the same induced gauge. Source and target may lie in different universes.

noncomputable def TauCeti.SymmetricGauge.operatorIdealFamily (𝕜 : Type u) [RCLike 𝕜] (Φ : SymmetricGauge) : OperatorIdealFamily 𝕜

The rectangular operator-ideal family induced by a symmetric gauge Φ, with gauge T ↦ Φ∞(n ↦ aₙ(T)) on bounded operators between Hilbert spaces in arbitrary source and target universes.

@[simp]

theorem TauCeti.SymmetricGauge.operatorIdealFamily_gauge (Φ : SymmetricGauge) {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A : E →L[𝕜] F) : (operatorIdealFamily 𝕜 Φ).gauge A = Φ.opGauge A

noncomputable def TauCeti.SymmetricGauge.symmetricOperatorIdealFamily (𝕜 : Type u) [RCLike 𝕜] (Φ : SymmetricGauge) : SymmetricOperatorIdealFamily 𝕜

The symmetric operator-ideal family induced by a symmetric gauge Φ: the diagonal-universe restriction of TauCeti.SymmetricGauge.operatorIdealFamily, whose gauge is invariant under adjoints.

@[simp]

theorem TauCeti.SymmetricGauge.symmetricOperatorIdealFamily_toOperatorIdealFamily (Φ : SymmetricGauge) (𝕜 : Type u) [RCLike 𝕜] : (symmetricOperatorIdealFamily 𝕜 Φ).toOperatorIdealFamily = operatorIdealFamily 𝕜 Φ

theorem TauCeti.SymmetricGauge.operatorIdealFamily_supGauge (𝕜 : Type u) [RCLike 𝕜] : operatorIdealFamily 𝕜 supGauge = OperatorIdealFamily.opNorm 𝕜

The operator-norm endpoint of the Schatten scale. The family induced by the supremum gauge, with gauge supₙ aₙ(T), is the operator-norm family.

theorem TauCeti.SymmetricGauge.symmetricOperatorIdealFamily_supGauge (𝕜 : Type u) [RCLike 𝕜] : symmetricOperatorIdealFamily 𝕜 supGauge = SymmetricOperatorIdealFamily.opNorm 𝕜

The symmetric family induced by the supremum gauge is the symmetric operator-norm family.