The nuclear gauge of a bounded operator

The nuclear gauge is the sum of the approximation numbers, with values in ℝ≥0∞. Its finite values select the trace-class operators on Hilbert spaces. The supremum of the Ky Fan prefixes gives the gauge, so Ky Fan dominance and the triangle inequality pass to this sum. Homogeneity, adjoint invariance and the two-sided ideal estimate supply the laws needed to construct the trace-class operator ideal.

The gauge is lower semicontinuous in operator norm. Finite gauge forces approximation numbers to tend to zero. Over a locally compact scalar field this implies compactness when the target is complete, and the identity on an infinite-dimensional Banach space has infinite gauge. Finite-rank operators have finite gauge, computed by any prefix beyond their rank.

References

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

noncomputable def ContinuousLinearMap.nuclearENorm {𝕜 : 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 nuclear gauge is the extended sum of the zero-indexed approximation numbers. On Hilbert spaces its finite-gauge operators are the trace-class operators.

theorem ContinuousLinearMap.nuclearENorm_def {𝕜 : 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.nuclearENorm = ∑' (n : ℕ), ↑(T.singularValue n)

The nuclear gauge as a sum of approximation numbers.

theorem ContinuousLinearMap.nuclearENorm_eq_iSup_kyFanGauge {𝕜 : 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.nuclearENorm = ⨆ (k : ℕ), ↑(T.kyFanGauge k)

The nuclear gauge is the supremum of the Ky Fan prefix gauges.

theorem ContinuousLinearMap.kyFanGauge_le_nuclearENorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) (k : ℕ) : ↑(T.kyFanGauge k) ≤ T.nuclearENorm

Every Ky Fan prefix is bounded by the nuclear gauge.

theorem ContinuousLinearMap.enorm_le_nuclearENorm {𝕜 : 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‖ₑ ≤ T.nuclearENorm

The nuclear gauge dominates the operator norm.

@[simp]

theorem ContinuousLinearMap.nuclearENorm_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : nuclearENorm 0 = 0

@[simp]

theorem ContinuousLinearMap.nuclearENorm_smul {𝕜 : 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) : (c • T).nuclearENorm = ‖c‖ₑ * T.nuclearENorm

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

@[simp]

theorem ContinuousLinearMap.nuclearENorm_neg {𝕜 : 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).nuclearENorm = T.nuclearENorm

Negation preserves the nuclear gauge.

theorem ContinuousLinearMap.nuclearENorm_comp_comp_le {𝕜 : 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) : (A ∘SL T ∘SL B).nuclearENorm ≤ ‖A‖ₑ * T.nuclearENorm * ‖B‖ₑ

The nuclear gauge satisfies the two-sided ideal bound.

theorem ContinuousLinearMap.nuclearENorm_le_of_forall_kyFanGauge_le {𝕜 : 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) : S.nuclearENorm ≤ T.nuclearENorm

Domination of every Ky Fan prefix implies domination of the nuclear gauges.

theorem ContinuousLinearMap.nuclearENorm_ne_top_iff_summable {𝕜 : 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.nuclearENorm ≠ ⊤ ↔ Summable T.singularValue

The nuclear gauge is finite exactly when the approximation numbers are summable.

theorem ContinuousLinearMap.nuclearENorm_eq_kyFanGauge_of_rank_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) {k : ℕ} (hT : (↑T).rank ≤ ↑k) : T.nuclearENorm = ↑(T.kyFanGauge k)

A rank cutoff turns the nuclear gauge into a finite Ky Fan prefix.

@[simp]

theorem ContinuousLinearMap.nuclearENorm_smulRight {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (f : StrongDual 𝕜 E) (y : F) : (smulRight f y).nuclearENorm = ‖f‖ₑ * ‖y‖ₑ

The approximation-number gauge of a rank-one operator is the product of the norms of its functional and vector. No Hilbert-space hypothesis is needed for this formula.

theorem ContinuousLinearMap.nuclearENorm_ne_top_of_rank_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) {k : ℕ} (hT : (↑T).rank ≤ ↑k) : T.nuclearENorm ≠ ⊤

Finite-rank operators have finite nuclear gauge.

theorem ContinuousLinearMap.lowerSemicontinuous_nuclearENorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : LowerSemicontinuous nuclearENorm

The nuclear gauge is lower semicontinuous in the operator norm topology.

@[simp]

theorem ContinuousLinearMap.nuclearENorm_eq_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) : T.nuclearENorm = 0 ↔ T = 0

The nuclear gauge vanishes exactly at zero for maps into a separated normed space.

theorem ContinuousLinearMap.isCompactOperator_of_nuclearENorm_ne_top {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [LocallyCompactSpace 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {T : E →L[𝕜] F} (hT : T.nuclearENorm ≠ ⊤) : IsCompactOperator ⇑T

Finite nuclear gauge implies compactness for a complete target over a locally compact field.

theorem ContinuousLinearMap.nuclearENorm_id_eq_top {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [LocallyCompactSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (hE : ¬FiniteDimensional 𝕜 E) : (ContinuousLinearMap.id 𝕜 E).nuclearENorm = ⊤

The identity on an infinite-dimensional Banach space has infinite nuclear gauge.

theorem ContinuousLinearMap.nuclearENorm_add_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (S T : E →L[𝕜] F) : (S + T).nuclearENorm ≤ S.nuclearENorm + T.nuclearENorm

The nuclear gauge is subadditive for operators from a Hilbert space.

theorem ContinuousLinearMap.nuclearENorm_sum_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_4} (s : Finset ι) (T : ι → E →L[𝕜] F) : (∑ i ∈ s, T i).nuclearENorm ≤ ∑ i ∈ s, (T i).nuclearENorm

The trace-class gauge of a finite sum is bounded by the sum of the gauges.

theorem ContinuousLinearMap.nuclearENorm_le_tsum_of_hasSum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_4} {T : ι → E →L[𝕜] F} {S : E →L[𝕜] F} (hT : HasSum T S) : S.nuclearENorm ≤ ∑' (i : ι), (T i).nuclearENorm

Fatou inequality for the trace-class gauge. For a series converging in operator norm, the gauge of its sum is at most the sum of the gauges, even when that sum is infinite.

@[simp]

theorem ContinuousLinearMap.nuclearENorm_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : (adjoint T).nuclearENorm = T.nuclearENorm

Taking adjoints preserves the nuclear gauge.