The operator-norm ideal family

The extended operator norm A ↦ ‖A‖ₑ is the smallest operator-ideal family: every family dominates it by the law OperatorIdealFamily.enorm_le_gauge. Its ideal consists of all bounded operators, and its carrier is complete because the operator norm is continuous.

Taking adjoints preserves the operator norm, so its diagonal-universe restriction is a symmetric family.

Main declarations

• TauCeti.OperatorIdealFamily.opNorm: the operator-ideal family with gauge ‖A‖ₑ.
• TauCeti.OperatorIdealFamily.finiteSubmodule_opNorm: every bounded operator lies in its ideal.
• TauCeti.OperatorIdealFamily.opNorm_isComplete: the operator-norm family is complete.
• TauCeti.SymmetricOperatorIdealFamily.opNorm: the adjoint-invariant diagonal family.

noncomputable def TauCeti.OperatorIdealFamily.opNorm (𝕜 : Type u) [RCLike 𝕜] : OperatorIdealFamily 𝕜

The operator-ideal family whose gauge is the extended operator norm.

@[simp]

theorem TauCeti.OperatorIdealFamily.gauge_opNorm {𝕜 : 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) : (opNorm 𝕜).gauge A = ‖A‖ₑ

@[simp]

theorem TauCeti.OperatorIdealFamily.finiteSubmodule_opNorm {𝕜 : Type u} [RCLike 𝕜] (E : Type v) (F : Type w) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] : ((opNorm 𝕜).operatorGauge E F).finiteSubmodule = ⊤

Every bounded operator lies in the ideal of the operator-norm family.

instance TauCeti.OperatorIdealFamily.opNorm_isComplete {𝕜 : Type u} [RCLike 𝕜] : (opNorm 𝕜).IsComplete

The operator-norm family is complete.

noncomputable def TauCeti.SymmetricOperatorIdealFamily.opNorm (𝕜 : Type u) [RCLike 𝕜] : SymmetricOperatorIdealFamily 𝕜

The adjoint-invariant diagonal-universe operator-norm family.

@[simp]

theorem TauCeti.SymmetricOperatorIdealFamily.opNorm_toOperatorIdealFamily (𝕜 : Type u) [RCLike 𝕜] : (opNorm 𝕜).toOperatorIdealFamily = OperatorIdealFamily.opNorm 𝕜

The underlying rectangular family of the symmetric operator-norm family.