The normed ideals of an operator-ideal family

An operator-ideal family Φ restricts, on each Hilbert-space pair E, F, to the operator gauge Φ.operatorGauge E F. Its finite-gauge submodule is the operator ideal of the family, which is stable under composition with bounded operators on either side, and its carrier is the normed space of operators of finite gauge.

A family is complete (OperatorIdealFamily.IsComplete) when all of its carriers are Banach spaces. This holds as soon as every gauge is lower semicontinuous for the operator-norm topology.

Main declarations

• TauCeti.OperatorIdealFamily.operatorGauge: the operator gauge of a family on a Hilbert-space pair.
• TauCeti.OperatorIdealFamily.comp_left_mem_finiteSubmodule, TauCeti.OperatorIdealFamily.comp_right_mem_finiteSubmodule: the ideal is stable under composition.
• TauCeti.OperatorIdealFamily.IsComplete: every carrier of the family is complete.
• TauCeti.OperatorIdealFamily.isComplete_of_lowerSemicontinuous: a family with lower semicontinuous gauges is complete.

References

• B. Simon, Trace Ideals and Their Applications, second edition, AMS, 2005, Chapter 2.
• I. C. Gohberg, M. G. Krein, Introduction to the Theory of Linear Nonselfadjoint Operators, AMS, 1969, Chapter III.

def TauCeti.OperatorIdealFamily.operatorGauge {𝕜 : Type u} [RCLike 𝕜] (Φ : OperatorIdealFamily 𝕜) (E : Type v) (F : Type w) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] : OperatorGauge 𝕜 E F

The gauge of an operator-ideal family on the bounded operators between a Hilbert-space pair.

@[simp]

theorem TauCeti.OperatorIdealFamily.operatorGauge_apply {𝕜 : 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) : (Φ.operatorGauge E F) A = Φ.gauge A

theorem TauCeti.OperatorIdealFamily.comp_left_mem_finiteSubmodule {𝕜 : 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} (hA : A ∈ (Φ.operatorGauge E F).finiteSubmodule) : L ∘SL A ∈ (Φ.operatorGauge E G).finiteSubmodule

The ideal of a family is stable under composition on the left with a bounded operator.

theorem TauCeti.OperatorIdealFamily.comp_right_mem_finiteSubmodule {𝕜 : 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} (hA : A ∈ (Φ.operatorGauge E F).finiteSubmodule) (R : H →L[𝕜] E) : A ∘SL R ∈ (Φ.operatorGauge H F).finiteSubmodule

The ideal of a family is stable under composition on the right with a bounded operator.

Completeness

class TauCeti.OperatorIdealFamily.IsComplete {𝕜 : Type u} [RCLike 𝕜] (Φ : OperatorIdealFamily 𝕜) : Prop

An operator-ideal family is complete when the normed carrier of every Hilbert-space pair is a Banach space.

• completeSpace_carrier (E : Type v) (F : Type w) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] : CompleteSpace (Φ.operatorGauge E F).Carrier

  Every carrier of the family is complete.

instance TauCeti.OperatorIdealFamily.instCompleteSpaceCarrierOperatorGaugeOfIsComplete {𝕜 : Type u} [RCLike 𝕜] {Φ : OperatorIdealFamily 𝕜} {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] [Φ.IsComplete] : CompleteSpace (Φ.operatorGauge E F).Carrier

theorem TauCeti.OperatorIdealFamily.isComplete_of_lowerSemicontinuous {𝕜 : 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], LowerSemicontinuous fun (A : E →L[𝕜] F) => Φ.gauge A) : Φ.IsComplete

An operator-ideal family whose gauges are lower semicontinuous for the operator-norm topology is complete.