Operator ideal families #

An operator ideal in the sense of Pietsch is a rule assigning to every pair of spaces E, F a linear subspace of E →L[𝕜] F that is stable under composition with arbitrary bounded maps on either side, together with a norm on that subspace dominating the operator norm and submultiplicative against outer compositions. Because Davis--Kahan compares operators between different spaces, the ideal must be handled as a coherent family across all pairs at once, not as a norm on a single endomorphism algebra.

The families here range over Hilbert spaces, with source and target still in independent universes. See "Why Hilbert and not Banach" below: the restriction is forced by the examples, not by the laws.

The single-field representation #

The family is presented by exactly one datum, an extended-real-valued gauge

gauge : (E →L[𝕜] F) → ℝ≥0∞

defined on all operators, with the ideal recovered as its finiteness domain OperatorIdealFamily.carrier. This is the classical presentation of a symmetric norming function (Gohberg--Krein): an operator lies in the ideal exactly when its ideal norm is finite. Three things follow.

Extensionality is structural. Two families with the same gauge are equal (OperatorIdealFamily.ext), because the gauge is the only field. A representation carrying membership and a gauge as independent data cannot have such a theorem: the gauge is then unconstrained off the ideal, so two families can agree on every ideal element and still differ.
Every law is unconditional. In ℝ≥0∞ the triangle inequality, the homogeneity gauge (c • A) = ‖c‖ₑ * gauge A, and the ideal bound gauge (L ∘L A ∘L R) ≤ ‖L‖ₑ * gauge A * ‖R‖ₑ all hold verbatim at non-members, so no law needs a membership hypothesis and no lemma needs to carry one.
The axiom list is short. Four laws suffice. Closure of the ideal under 0, +, •, -, and finite sums is a consequence (it is Submodule membership for carrier), gauge 0 = 0 follows from homogeneity at c = 0, and definiteness follows from enorm_le_gauge.

Why Hilbert and not Banach #

The four laws are statements about a norm, and every one of them is meaningful verbatim for Banach E, F. The examples are not. Of the five gauges this development has — the operator norm, the finite Ky Fan gauges, Schatten p, trace class and Hilbert--Schmidt — only the first survives outside Hilbert space, and the obstruction is gauge_add_le, not the definition. Concretely, for the finite Ky Fan gauge ∑_{n < k} aₙ(A) the gauge is defined at full Banach generality (ContinuousLinearMap.approximationNumber is stated for seminormed spaces over a NontriviallyNormedField) while its subadditivity is Hilbertian: the proof runs through singular values and majorization, and the classical additivity of approximation numbers, a_{m+n}(S + T) ≤ aₘ(S) + aₙ(T), does not recover it — already at k = 2 that bound only gives a₀(S) + 2a₀(T) + a₁(S), which is not ∑_{n<2} aₙ(S) + ∑_{n<2} aₙ(T).

So a Banach-wide version of this structure would be a notion with one instance and no way to acquire the motivating ones. The parameters are therefore Hilbert throughout. Re-widening is a purely mechanical edit should an instance ever appear: no proof in this file uses the inner product, only the norm.

Layering #

OperatorIdealFamily keeps independent source and target universes. Adjoint symmetry cannot be added at that generality: A✝ swaps the roles of source and target, so a family closed under adjoints must be defined on a single universe. That is SymmetricOperatorIdealFamily, which extends the diagonal instantiation.

The two universes occur only through max v w in the type of the structure itself, so linter.checkUnivs flags them. They stay independent, and the argument is the layering itself rather than an appeal to generality:

SymmetricOperatorIdealFamily extends OperatorIdealFamily.{u, v, v} — it is the diagonal instantiation. Collapse v and w and .{u, v, v} becomes .{u, v}: the two structures acquire the same generality, and the distinction this section is about stops existing. The rectangular layer earns its second universe by being the thing the symmetric layer specializes.
Family/OperatorNorm.lean carries a hand-written specialization of instIsCompleteOperatorNormIdealFamily precisely because the general instance is stated at three independent universes and instance search cannot see it once the symmetric family equates the last two.

So the independence is exercised, not merely declared; the linter's heuristic reads the structure's type, where it is invisible.

Main definitions #

TauCeti.OperatorIdealFamily: the gauge and its four laws.
TauCeti.OperatorIdealFamily.carrier: the ideal, as a Submodule.
TauCeti.OperatorIdealFamily.Elem: the ideal as a normed space in its own right — a type synonym for the carrier carrying the ideal norm rather than the operator norm inherited from the ambient space.
TauCeti.OperatorIdealFamily.IsComplete: completeness of the ideal, expressed as CompleteSpace for that norm rather than as a hand-rolled Cauchy criterion.
TauCeti.SymmetricOperatorIdealFamily: the adjoint-invariant diagonal layer.

Provenance #

Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
Original module: DavisKahan/OperatorIdeal/UnitarilyInvariant/RectangularFamily.lean (RectangularSymmetricIdealFamily, Jon Crall / OpenAI GPT-5.6 Thinking); Apache 2.0.
Extraction class: redesigned. Per the signature-polish backlog the free-data presentation (Mem plus a total real gauge constrained only on members, one universe, hand-rolled completeness, fourteen fields) is replaced here by the single-gauge presentation above, and this is the only presentation of an operator ideal in the library. The legacy structure was retired downstream on 2026-08-27, together with both directions of the conversion between the two and the four concrete ideals that were built by converting a canonical family into a legacy record and back. Its free data survives only as SymmetricOperatorIdealFamily.Core in DavisKahan/OperatorIdeal/UnitarilyInvariant/FamilyCore.lean: constructor arguments for ofCore, carrying no gauge of their own and used by the two source-facing Hilbert--Schmidt ideals, which are families from the moment they are defined.