Families of operator ideals

An operator-ideal family assigns an extended nonnegative gauge to every bounded operator between Hilbert spaces. The gauge is subadditive, absolutely homogeneous, dominates the operator norm, and satisfies the two-sided ideal inequality. Its finite locus therefore selects a rectangular operator ideal, while the extended value ∞ allows one family to describe both members and nonmembers.

A symmetric operator-ideal family additionally identifies the gauges of an operator and its adjoint. This requires source and target to live in the same universe, since taking adjoints swaps them.

This file provides the common algebraic API of these families: zero and negation laws, definiteness, finite-sum subadditivity, one-sided ideal inequalities, contraction bounds, and extensionality. Concrete trace-class, Hilbert--Schmidt, Ky Fan, and Schatten families can use these results without repeating their ideal calculus.

References

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

structure TauCeti.OperatorIdealFamily (𝕜 : Type u) [RCLike 𝕜] : Type (max (max u (v + 1)) (w + 1))

A rectangular family of extended nonnegative operator gauges on Hilbert spaces.

The four fields are subadditivity, absolute homogeneity, domination of the operator norm, and the two-sided ideal inequality. The family is universe-polymorphic in the source and target spaces, so one object supplies a gauge on every Hilbert-space pair in the chosen universes.

• gauge {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] : (E →L[𝕜] F) → ENNReal

  The extended nonnegative gauge on bounded operators between a Hilbert-space pair.

• gauge_add_le {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A B : E →L[𝕜] F) : self.gauge (A + B) ≤ self.gauge A + self.gauge B

  The gauge is subadditive.

• gauge_smul {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (c : 𝕜) (A : E →L[𝕜] F) : self.gauge (c • A) = ‖c‖ₑ * self.gauge A

  The gauge is absolutely homogeneous.

• enorm_le_gauge {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A : E →L[𝕜] F) : ‖A‖ₑ ≤ self.gauge A

  The gauge dominates the extended operator norm.

• gauge_comp_le {E H : Type v} {F G : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [CompleteSpace G] (L : F →L[𝕜] G) (A : E →L[𝕜] F) (R : H →L[𝕜] E) : self.gauge (L ∘SL A ∘SL R) ≤ ‖L‖ₑ * self.gauge A * ‖R‖ₑ

  The gauge satisfies the two-sided ideal inequality.

structure TauCeti.SymmetricOperatorIdealFamily (𝕜 : Type u) [RCLike 𝕜] extends TauCeti.OperatorIdealFamily 𝕜 : Type (max u (v + 1))

A symmetric operator-ideal family is an operator-ideal family whose diagonal-universe gauge is invariant under adjoints.

• gauge {E F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] : (E →L[𝕜] F) → ENNReal
• gauge_add_le {E F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A B : E →L[𝕜] F) : self.gauge (A + B) ≤ self.gauge A + self.gauge B
• gauge_smul {E F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (c : 𝕜) (A : E →L[𝕜] F) : self.gauge (c • A) = ‖c‖ₑ * self.gauge A
• enorm_le_gauge {E F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A : E →L[𝕜] F) : ‖A‖ₑ ≤ self.gauge A
• gauge_comp_le {E H F G : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [CompleteSpace G] (L : F →L[𝕜] G) (A : E →L[𝕜] F) (R : H →L[𝕜] E) : self.gauge (L ∘SL A ∘SL R) ≤ ‖L‖ₑ * self.gauge A * ‖R‖ₑ
• gauge_adjoint {E F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A : E →L[𝕜] F) : self.gauge (ContinuousLinearMap.adjoint A) = self.gauge A

  Taking the adjoint preserves the gauge.

theorem TauCeti.OperatorIdealFamily.ext {𝕜 : Type u} [RCLike 𝕜] {Φ Ψ : OperatorIdealFamily 𝕜} (h : ∀ {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace 𝕜 E] [inst_2 : CompleteSpace E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : CompleteSpace F] (A : E →L[𝕜] F), Φ.gauge A = Ψ.gauge A) : Φ = Ψ

Two operator-ideal families are equal when all of their gauges agree.

theorem TauCeti.OperatorIdealFamily.ext_iff {𝕜 : Type u} [RCLike 𝕜] {Φ Ψ : OperatorIdealFamily 𝕜} : Φ = Ψ ↔ ∀ {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace 𝕜 E] [inst_2 : CompleteSpace E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : CompleteSpace F] (A : E →L[𝕜] F), Φ.gauge A = Ψ.gauge A

@[simp]

theorem TauCeti.OperatorIdealFamily.gauge_zero {𝕜 : Type u} [RCLike 𝕜] (Φ : OperatorIdealFamily 𝕜) {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] : Φ.gauge 0 = 0

Every operator-ideal gauge vanishes at the zero operator.

@[simp]

theorem TauCeti.OperatorIdealFamily.gauge_eq_zero_iff {𝕜 : Type u} [RCLike 𝕜] (Φ : OperatorIdealFamily 𝕜) {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A : E →L[𝕜] F) : Φ.gauge A = 0 ↔ A = 0

An operator-ideal gauge vanishes exactly at the zero operator.

@[simp]

theorem TauCeti.OperatorIdealFamily.gauge_neg {𝕜 : Type u} [RCLike 𝕜] (Φ : OperatorIdealFamily 𝕜) {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A : E →L[𝕜] F) : Φ.gauge (-A) = Φ.gauge A

Negating an operator does not change its operator-ideal gauge.

theorem TauCeti.OperatorIdealFamily.gauge_sum_le {𝕜 : Type u} [RCLike 𝕜] (Φ : OperatorIdealFamily 𝕜) {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {ι : Type u_1} (s : Finset ι) (A : ι → E →L[𝕜] F) : Φ.gauge (∑ i ∈ s, A i) ≤ ∑ i ∈ s, Φ.gauge (A i)

The gauge of a finite sum is at most the sum of the gauges.

theorem TauCeti.OperatorIdealFamily.gauge_comp_left_le {𝕜 : Type u} [RCLike 𝕜] (Φ : OperatorIdealFamily 𝕜) {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {G : Type w} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [CompleteSpace G] (L : F →L[𝕜] G) (A : E →L[𝕜] F) : Φ.gauge (L ∘SL A) ≤ ‖L‖ₑ * Φ.gauge A

Composition on the left satisfies the one-sided ideal inequality.

theorem TauCeti.OperatorIdealFamily.gauge_comp_right_le {𝕜 : Type u} [RCLike 𝕜] (Φ : OperatorIdealFamily 𝕜) {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {H : Type v} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (A : E →L[𝕜] F) (R : H →L[𝕜] E) : Φ.gauge (A ∘SL R) ≤ Φ.gauge A * ‖R‖ₑ

Composition on the right satisfies the one-sided ideal inequality.

theorem TauCeti.OperatorIdealFamily.gauge_comp_left_le_self {𝕜 : Type u} [RCLike 𝕜] (Φ : OperatorIdealFamily 𝕜) {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {G : Type w} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [CompleteSpace G] {L : F →L[𝕜] G} (hL : ‖L‖ ≤ 1) (A : E →L[𝕜] F) : Φ.gauge (L ∘SL A) ≤ Φ.gauge A

Left composition by a contraction does not increase an operator-ideal gauge.

theorem TauCeti.OperatorIdealFamily.gauge_comp_right_le_self {𝕜 : Type u} [RCLike 𝕜] (Φ : OperatorIdealFamily 𝕜) {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {H : Type v} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (A : E →L[𝕜] F) {R : H →L[𝕜] E} (hR : ‖R‖ ≤ 1) : Φ.gauge (A ∘SL R) ≤ Φ.gauge A

Right composition by a contraction does not increase an operator-ideal gauge.

theorem TauCeti.SymmetricOperatorIdealFamily.ext {𝕜 : Type u} [RCLike 𝕜] {Φ Ψ : SymmetricOperatorIdealFamily 𝕜} (h : ∀ {E F : Type v} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace 𝕜 E] [inst_2 : CompleteSpace E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : CompleteSpace F] (A : E →L[𝕜] F), Φ.gauge A = Ψ.gauge A) : Φ = Ψ

Two symmetric operator-ideal families are equal when all of their gauges agree.

theorem TauCeti.SymmetricOperatorIdealFamily.ext_iff {𝕜 : Type u} [RCLike 𝕜] {Φ Ψ : SymmetricOperatorIdealFamily 𝕜} : Φ = Ψ ↔ ∀ {E F : Type v} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace 𝕜 E] [inst_2 : CompleteSpace E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : CompleteSpace F] (A : E →L[𝕜] F), Φ.gauge A = Ψ.gauge A