The operator norm as an ideal family

The largest operator ideal is the whole space of bounded operators, gauged by the operator norm. It is the canonical example of TauCeti.OperatorIdealFamily, and — since the adjoint is an isometry — of TauCeti.SymmetricOperatorIdealFamily.

This module also records the two facts that make the example useful as a sanity check on the abstract layer: the ideal is everything (carrier_operatorNormFamily), and the ideal norm on it is the operator norm (operatorNormFamilyElemEquiv, a linear isometry equivalence onto E →L[𝕜] F), from which completeness of the family is inherited from completeness of E →L[𝕜] F.

Main definitions

• TauCeti.operatorNormIdealFamily: the operator norm as an ideal family over a general nontrivially normed field, with independent source and target universes.
• TauCeti.operatorNormFamily: its symmetric (Hilbert, adjoint-invariant) refinement.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: authored directly in ForTauCeti at Davis--Kahan commit b283d23; it has had no prior home.
• Extraction class: authored in place for the Tau Ceti staging layer.
• Original authors / copyright: Jon Crall, Claude Opus 5, OpenAI GPT-5.6 Thinking; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none — this module imports only Mathlib and sibling ForTauCeti staging modules.

theorem TauCeti.ContinuousLinearMap.opNorm_comp_comp_le {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup H] [NormedSpace 𝕜 H] (L : F →L[𝕜] G) (A : E →L[𝕜] F) (R : H →L[𝕜] E) : ‖L ∘SL A ∘SL R‖ ≤ ‖L‖ * ‖A‖ * ‖R‖

Submultiplicativity of the operator norm across a two-sided composition.

Mathlib has the two-fold ContinuousLinearMap.opNorm_comp_le; the two-sided form is what every ideal law is stated against, so it is worth a name. Nothing here needs an inner product or completeness — it is a fact about normed spaces — but it is stated where its first consumer is rather than in a file of its own.

opNorm_comp_comp_le in the legacy rectangular namespace was this same calc proof, verbatim; it now delegates here.

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

The operator norm, as an operator ideal family: every bounded operator is a member, and the gauge is the operator norm.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

The gauge of the operator-norm family is the operator norm, definitionally. This is the lemma that lets the generic ideal-family API be read as ordinary operator-norm statements.

@[simp]

theorem TauCeti.carrier_operatorNormIdealFamily {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] : (operatorNormIdealFamily 𝕜).carrier = ⊤

The operator-norm family is the largest ideal: every bounded operator belongs to it, because every bounded operator has finite operator norm. It is the top element against which the other families (Ky Fan, Hilbert--Schmidt, trace class) are proper.

noncomputable def TauCeti.operatorNormIdealFamilyElemEquiv {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] : (operatorNormIdealFamily 𝕜).Elem E F ≃ₗᵢ[𝕜] E →L[𝕜] F

The ideal of the operator-norm family is all of E →L[𝕜] F, isometrically: its ideal norm is the operator norm.

Equations

• One or more equations did not get rendered due to their size.

instance TauCeti.instIsCompleteOperatorNormIdealFamily {𝕜 : Type u} [RCLike 𝕜] : (operatorNormIdealFamily 𝕜).IsComplete

The operator-norm ideal is complete, transported along the isometry operatorNormIdealFamilyElemEquiv from completeness of E →L[𝕜] F.

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

The operator norm, as a symmetric ideal family: the adjoint is an isometry, so the operator norm is adjoint-invariant.

Equations

• TauCeti.operatorNormFamily 𝕜 = { toOperatorIdealFamily := TauCeti.operatorNormIdealFamily 𝕜, gauge_adjoint := ⋯ }

instance TauCeti.instIsCompleteOperatorNormFamily {𝕜 : Type u} [RCLike 𝕜] : (operatorNormFamily 𝕜).IsComplete

Completeness transfers to the symmetric view, which shares its underlying family with operatorNormIdealFamily. The instance has to be restated rather than inherited: instIsCompleteOperatorNormIdealFamily is stated at three independent universes, and the symmetric family constrains the last two to be equal, so instance search does not find it without this specialization.

@[simp]

theorem TauCeti.gauge_operatorNormFamily {𝕜 : Type u} [RCLike 𝕜] {E F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A : E →L[𝕜] F) : (operatorNormFamily 𝕜).gauge A = ‖A‖ₑ

The symmetric operator-norm family has the same gauge as the plain one; the symmetric structure adds adjoint-invariance, not a different norm.