How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 16 results · all verified · 14 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 2 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Fredholm Determinants and the Lidskii Trace Formula

1 · Prerequisites

2 · Summary

This page builds a local Fredholm determinant theory for trace-class operators on complex Hilbert spaces. The construction begins on separable spaces with exterior powers and their induced operators; singular-value estimates and finite-rank compressions supply the trace-norm control needed for the determinant series. The resulting determinant is entire, normalized at zero, and has trace-norm continuity, growth, and multiplicativity properties.

The analytic results identify its logarithmic derivative and prove that its zeros occur exactly at the noninvertibility parameters, with order equal to the algebraic multiplicity of the corresponding nonzero eigenvalue. Algebraic multiplicity is defined through the stabilized generalized eigenspace of a compact operator. For the trace formula, a trace-class quasinilpotent operator has trace zero, and the generalized-eigenspace decomposition computes the trace through the nonzero eigenvalues. This decomposition uses invariant subspaces and quotient/compression arguments; invariance alone does not make a subspace reducing.

The trace-power and logarithmic-derivative argument gives the spectral product for the local determinant. A final support theorem extends the determinant to arbitrary complex Hilbert spaces by restricting to a separable reducing support, and proves that the value is independent of the chosen support. AC is stated where the nuclear representation, Hilbert projection, or spectral multiplicity inputs require it; the rank-one example separately records the library's linear-first inner-product convention.

The published determinant definition, its arbitrary-space properties, and Lidskii's trace formula now follow these local lemmas on this page. The definition uses the support construction; the properties transfer the local separable estimates and identities through common supports; and the trace formula differentiates the locally uniform product at zero.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30Open item page →

Algebraic multiplicity of a nonzero compact-operator eigenvalue

Definition

Assume the Axiom of Choice (The Axiom of Choice). Let $T$ be a compact operator on a complex Hilbert space $H$ , and let $λ \neq 0$ belong to its spectrum. Riesz–Schauder stabilization supplies an integer $m_{0}$ for which the kernels of $(I - T / λ)^{m}$ are constant for $m \geq m_{0}$ . Define the generalized eigenspace and algebraic multiplicity by

$G_{λ} (T) : = \ker (T - λ I)^{m_{0}}, m_{a l g} (λ; T) : = \dim G_{λ} (T) .$

The value is independent of the choice of stabilized exponent. If $P_{λ}$ is the Riesz spectral projection of $T$ at $λ$ , then $G_{λ} (T) = ran P_{λ}$ ; in particular the algebraic multiplicity is the finite rank of that projection.

Facts & Assumptions

Given: AC; a complex Hilbert space $H$ ; a compact $T : H \to H$ ; and $λ \neq 0$ in $σ (T)$ .

[A1]

For compact $T$ , each nonzero spectral value is an eigenvalue with finite-dimensional generalized eigenspace (Riesz schauder spectrum of a compact operator).

[A2]

For every $ε > 0$ , only finitely many spectral values of a compact operator have modulus at least $ε$ (Riesz schauder spectrum of a compact operator).

[A3]

If $A = I - K$ with $K$ compact on a Banach space and DC holds, the kernels of $A^{m}$ stabilize at a finite index (Riesz Schauder ascent and descent stabilize).

[A4]

For the isolated spectral set $E = {λ}$ , the Riesz spectral projection is defined as $P_{λ} = χ_{E} (T)$ (Riesz spectral projection).

[A5]

The Riesz projection is idempotent, commutes with $T$ , and splits $H$ into its closed invariant range and kernel (Riesz spectral projection properties).

[A6]

If nonzero, the restriction spectra on $ran P_{λ}$ and $\ker P_{λ}$ are respectively ${λ}$ and $σ (T) ∖ {λ}$ (Riesz spectral projection properties).

[A7]

A subspace $W$ is $T$ -invariant when $T (W) \subseteq W$ (Invariant subspaces, restrictions, and induced quotient operators).

[A8]

A compact operator on an infinite-dimensional Banach space has $0$ in its spectrum (Riesz schauder spectrum of a compact operator).

[A9]

Every nonconstant complex polynomial has a root (Fundamental theorem of algebra by Liouville's theorem); an endomorphism of a finite-dimensional space whose characteristic polynomial splits has a Jordan form (Jordan form over the base field exists exactly when the characteristic polynomial splits).

[A10]

In ZF, AC implies DC (AC implies DC implies countable choice).

Proof

technique · direct

1.1A1A3A10

With $A = I - T / λ$ , we have $T - λ I = - λ A$ . The declared AC assumption supplies DC by [A10], so [A3] gives an $m_{0}$ for which $\ker (T - λ I)^{m} = \ker A^{m}$ is constant for every $m \geq m_{0}$ ; [A1] makes this stabilized space finite-dimensional.

1.2A2A4construct

Put $ε = ∣ λ ∣ / 2$ . By [A2] the set $S_{ε} = {μ \in σ (T) : ∣ μ ∣ \geq ε}$ is finite. Every spectral point within distance $∣ λ ∣ / 2$ of $λ$ lies in $S_{ε}$ ; because $λ \in S_{ε}$ , choose a smaller positive radius excluding the finitely many other points of $S_{ε}$ . Thus $λ$ is isolated and [A4] defines $P_{λ}$ .

2.1A4A5A6A7A8step 1.2

Let $P = P_{λ}$ from [A4]. By [A5] and the meaning of invariant subspace in [A7], $H = ran P \oplus \ker P$ with both summands closed and $T$ -invariant. The restriction of $T$ to $ran P$ is compact. If this range were infinite-dimensional, [A8] would put $0$ in its restriction spectrum, contrary to [A6], which gives that spectrum as ${λ}$ and $λ \neq 0$ . Hence $ran P$ is finite-dimensional.

3.1A6A9step 2.1

If $ran P = {0}$ , then $P = 0$ and [A6] would give $σ (T) = σ (T ∣_{\ker P}) = σ (T) ∖ {λ}$ , impossible since $λ \in σ (T)$ . Thus the range is nonzero. Its finite-dimensional restriction has spectrum ${λ}$ by [A6]. By [A9], its characteristic polynomial splits over $C$ and it has a Jordan form; all Jordan blocks have eigenvalue $λ$ . Therefore $(T - λ I)^{d}$ vanishes on $ran P$ , where $d = \dim ran P$ , so $ran P \subseteq G_{λ} (T)$ .

4.1A5A6step 1.1step 2.1∎

Conversely, take $x \in G_{λ} (T)$ and write $x = P x + (I - P) x$ using [A5]. Since $P$ commutes with $T$ , the second term lies in $\ker P$ and is killed by a power of $T - λ I$ . If $\ker P \neq {0}$ , [A6] says $λ$ is outside the spectrum of $T ∣_{\ker P}$ , so $T - λ I$ is invertible there and the second term is zero. If $\ker P = {0}$ it is zero directly. Hence $x \in ran P$ , and $G_{λ} (T) = ran P$ . The rank and dimension are finite by step 2.1, and step 1.1 proves independence of the stabilized exponent.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30Open item page →

Finite-rank orthogonal compressions converge in trace norm

Statement

Assume Countable Choice. Let $H$ be a separable complex Hilbert space, let $T \in S_{1} (H)$ be trace class, and let $(P_{n})_{n \geq 1}$ be any supplied sequence of finite-rank orthogonal projections on $H$ such that $P_{n} \to I$ strongly. Then $∥ P_{n} T P_{n} - T ∥_{1} ⟶ 0.$ The projections need not be increasing. For example, the initial projections onto the first $n$ vectors of a supplied countable orthonormal basis satisfy the hypothesis.

Facts & Assumptions

Given: Countable Choice, separable complex $H$ , trace-class $T \in B (H)$ , and the specified finite-rank orthogonal projections $P_{n}$ .

[A1]

By the trace-class definition, a trace-class operator is compact (Trace class operator).

[A2]

Every finite-rank operator is trace class, and hence each SVD truncation $F_{N}$ is trace class (Trace class operator).

[A3]

Under Countable Choice the singular-value decomposition supplies orthonormal families $(e_{j})$ and $(f_{j})$ and the operator-norm convergent expansion $T x = \sum_{j} s_{j} ⟨ x, e_{j} ⟩ f_{j}$ ; its index set is finite exactly in the finite-rank case (Singular value decomposition for compact operators).

[A4]

If a trace-class operator $R$ has a nuclear representation $R = \sum_{j} ⟨ \cdot, u_{j} ⟩ v_{j}$ converging in operator norm, then $∥ R ∥_{1} \leq \sum_{j} ∥ u_{j} ∥ ∥ v_{j} ∥$ (Nuclear series characterizes trace norm).

[A5]

Trace-class operators form a linear space and the trace norm satisfies the triangle inequality (Trace class is a two sided Banach operator ideal).

[A6]

For bounded $A, B$ and trace-class $R$ , $∥ A R B ∥_{1} \leq ∥ A ∥ ∥ R ∥_{1} ∥ B ∥$ (Trace class is a two sided Banach operator ideal).

[A7]

Each orthogonal projection $P_{n}$ is self-adjoint (Hilbert projections are linear, self-adjoint and contractive).

[A8]

Each orthogonal projection satisfies $∥ P_{n} x ∥ \leq ∥ x ∥$ , hence $∥ P_{n} ∥ \leq 1$ (Hilbert projections are linear, self-adjoint and contractive).

[A9]

Strong convergence means pointwise norm convergence: $∥ P_{n} x - x ∥ \to 0$ for every fixed $x \in H$ (Strong and weak operator topologies).

[A10]

Countable Choice supplies the hypotheses of the trace-class, SVD, nuclear-series, ideal, orthogonal-projection, and Fourier-expansion results used below (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Its explicit countable basis-selection use here is through the SVD in [A3], which selects bases of its countably many finite-dimensional singular eigenspaces; no orthonormal basis of the ambient $H$ is separately chosen.

[A11]

The trace-class singular-value series converges, so its tails tend to zero (Trace class operator).

[A12]

The complex inner product is linear in its first argument, so for each positive real $s_{j}$ , $⟨ x, s_{j} e_{j} ⟩ = s_{j} ⟨ x, e_{j} ⟩$ (Real and complex inner-product spaces and their induced length).

[A13]

If $(g_{j})_{j \geq 1}$ is a supplied countable complete orthonormal family, then the initial Fourier sums $\sum_{j = 1}^{n} ⟨ x, g_{j} ⟩ g_{j}$ converge to each $x$ in norm (Orthonormal families, complete orthonormal systems and Hilbert bases, Fourier expansion in a Hilbert space).

[A14]

The orthogonal projection onto a closed subspace is characterized by $P_{M} x \in M$ and $x - P_{M} x \in M^{⊥}$ (The Hilbert orthogonal projection onto a closed subspace).

Proof

technique · direct

Given: The data in the statement and facts [A1]–[A14].

1.1A1A2A3A4A5A10A11

By [A1]–[A3] and [A10], write the SVD of $T$ and let $J$ be its positive-singular-value index set. For $N \geq 0$ set $F_{N} = \sum_{j \in J, j \leq N} s_{j} ⟨ \cdot, e_{j} ⟩ f_{j}$ , with $F_{0} = 0$ . Since $F_{N}$ is trace class by [A2], [A5] makes $R_{N} : = T - F_{N}$ trace class; the SVD gives the operator-norm convergent nuclear tail $R_{N} = \sum_{j \in J, j > N} ⟨ \cdot, s_{j} e_{j} ⟩ f_{j}$ , so [A4] gives $∥ R_{N} ∥_{1} \leq \sum_{j > N} s_{j} \to 0$ by [A11]. If $T$ has finite rank $r$ , then $R_{N} = 0$ for $N \geq r$ ; when $T = 0$ or $H = {0}$ the sum is empty and $F_{N} = R_{N} = 0$ .

1.2A10A12A13A14

For the stated basis example, let $(g_{j})_{j \geq 1}$ be the supplied complete orthonormal basis and let $P_{n}$ project onto $M_{n} : = span {g_{1}, \dots, g_{n}}$ . The sum $s_{n} : = \sum_{j = 1}^{n} ⟨ x, g_{j} ⟩ g_{j}$ lies in $M_{n}$ , and orthonormality plus [A12] gives $x - s_{n} \in M_{n}^{⊥}$ , so [A14] gives $s_{n} = P_{n} x$ ; now [A13] yields $P_{n} x \to x$ .

2.1A4A7A8A9A10A12step 1.1

Fix $N$ and the finite SVD sum $F_{N}$ from step 1.1; by [A12] write it as $F_{N} = \sum_{j \in J, j \leq N} ⟨ \cdot, u_{j} ⟩ v_{j}$ , where $u_{j} = s_{j} e_{j}$ and $v_{j} = f_{j}$ . Self-adjointness in [A7] gives $P_{n} F_{N} P_{n} = \sum_{j} ⟨ \cdot, P_{n} u_{j} ⟩ P_{n} v_{j}$ , so $P_{n} F_{N} P_{n} - F_{N} = \sum_{j} (⟨ \cdot, P_{n} u_{j} ⟩ (P_{n} v_{j} - v_{j}) + ⟨ \cdot, P_{n} u_{j} - u_{j} ⟩ v_{j})$ . This finite nuclear representation and [A4] bound its trace norm by $\sum_{j \in J, j \leq N} (∥ P_{n} u_{j} ∥ ∥ P_{n} v_{j} - v_{j} ∥ + ∥ P_{n} u_{j} - u_{j} ∥ ∥ v_{j} ∥)$ , which tends to zero by [A8]–[A9] and finiteness of the sum. Thus $∥ P_{n} F_{N} P_{n} - F_{N} ∥_{1} \to 0$ for each fixed $N$ , including the empty sum when $N = 0$ or $T = 0$ .

3.1A5A6A8A10step 1.1step 2.1

For every $n, N$ , the residual $R_{N}$ from step 1.1 satisfies $∥ P_{n} R_{N} P_{n} ∥_{1} \leq ∥ P_{n} ∥^{2} ∥ R_{N} ∥_{1} \leq ∥ R_{N} ∥_{1}$ by [A6] and [A8]. Decomposing $P_{n} T P_{n} - T = P_{n} R_{N} P_{n} + (P_{n} F_{N} P_{n} - F_{N}) - R_{N}$ using step 2.1, and applying [A5]'s trace-norm triangle inequality, yields $∥ P_{n} T P_{n} - T ∥_{1} \leq 2 ∥ R_{N} ∥_{1} + ∥ P_{n} F_{N} P_{n} - F_{N} ∥_{1}$ . All terms are trace class by [A5]–[A6].

4.1A3A10step 1.1step 2.1step 3.1∎

Given $ε > 0$ , choose $N$ by step 1.1 so that $∥ R_{N} ∥_{1} < ε / 4$ . For this fixed $N$ , step 2.1 gives an index $n_{0}$ such that $∥ P_{n} F_{N} P_{n} - F_{N} ∥_{1} < ε / 2$ for every $n \geq n_{0}$ . Step 3.1 then gives $∥ P_{n} T P_{n} - T ∥_{1} < ε$ for every $n \geq n_{0}$ , proving the claim. Countable Choice is the stated hypothesis of the trace-class, nuclear-series, ideal, orthogonal-projection, Fourier-expansion, and SVD suppliers in [A10]; the explicit countable basis selection used here is the SVD construction in [A3].

DefinitionDefinition: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30Open item page →

Hilbert exterior powers and induced operators

Definition

Let $H$ be a complex Hilbert space and let $n \geq 0$ . Set $Λ^{0} H : = C$ . For $n \geq 1$ , the algebraic $n$ -fold tensor product $H^{\otimes_{a l g} n}$ is the complex vector space generated by symbols $x_{1} \otimes \dots \otimes x_{n}$ subject to complex linearity in each slot. Equivalently, it is the quotient of the free complex vector space on $H^{n}$ by the span of the coordinate-wise additivity and scalar-linearity relations. Give it the sesquilinear form determined on elementary tensors by

$⟨ x_{1} \otimes \dots \otimes x_{n}, y_{1} \otimes \dots \otimes y_{n} ⟩ = \prod_{i = 1}^{n} ⟨ x_{i}, y_{i} ⟩,$

which is well defined because the product is linear in each first-slot vector and conjugate-linear in each second-slot vector. Complete $H^{\otimes_{a l g} n}$ in the induced norm to obtain the Hilbert tensor power $H^{\otimes n}$ . Use the action convention $U_{π} (x_{1} \otimes \dots \otimes x_{n}) = x_{π^{- 1} (1)} \otimes \dots \otimes x_{π^{- 1} (n)}$ for $π \in S_{n}$ . The Hilbert exterior power $Λ^{n} H$ is the range of the orthogonal projection

$A_{n} : = \frac{1}{n!} \sum_{π \in S_{n}} sgn (π) U_{π} .$

For $x_{1}, \dots, x_{n} \in H$ , write $x_{1} \land \dots \land x_{n} : = \sqrt{n!} A_{n} (x_{1} \otimes \dots \otimes x_{n})$ . Its inner product is

$⟨ x_{1} \land \dots \land x_{n}, y_{1} \land \dots \land y_{n} ⟩ = \det [⟨ x_{i}, y_{j} ⟩]_{i, j = 1}^{n} .$

If $T : H \to H$ is bounded, its induced operator $Λ^{n} T$ is the restriction of $T^{\otimes n}$ to $Λ^{n} H$ ; equivalently $(Λ^{n} T) (x_{1} \land \dots \land x_{n}) = T x_{1} \land \dots \land T x_{n}$ . Set $Λ^{0} T = I_{C}$ . For every bound $C$ of $T$ , $C^{n}$ is a bound for $Λ^{n} T$ , and $Λ^{n} (S T) = Λ^{n} S Λ^{n} T$ for bounded $S, T$ .

Facts & Assumptions

Given: A complex Hilbert space $H$ (Hilbert space), an integer $n \geq 0$ , and, when an induced operator is considered, a bounded linear operator $T : H \to H$ .

[A1]

The complex inner product is linear in its first argument and conjugate-linear in its second (Real and complex inner-product spaces and their induced length).

[A2]

The determinant of a square matrix is given by its finite signed permutation sum (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix).

[A3]

For bounded $T$ there is $C \geq 0$ such that $∥ T x ∥ \leq C ∥ x ∥$ for every $x$ (A bounded linear operator between normed spaces).

[A4]

Every finite-dimensional real or complex inner-product space has a finite orthonormal basis, including the empty basis in dimension zero (Every finite-dimensional real or complex inner product space has an orthonormal basis).

[A5]

A supplied orthonormal basis is a complete orthonormal family, so its finite linear span is dense in $H$ (Orthonormal families, complete orthonormal systems and Hilbert bases).

Proof

technique · direct

1.1A1A4construct

Fix $n \geq 1$ . In any finite tensor sum, all factor vectors lie in a finite-dimensional subspace $E \subseteq H$ . Choose a finite orthonormal basis $(f_{j})$ of $E$ by [A4]. Multilinearity expands the sum in the elementary tensors $f_{j_{1}} \otimes \dots \otimes f_{j_{n}}$ ; the product form makes these tensors orthonormal. Their linear independence follows by applying the multilinear coordinate functionals $(x_{1}, \dots, x_{n}) \mapsto \prod_{r = 1}^{n} ⟨ x_{r}, f_{j_{r}} ⟩$ , which descend to the quotient and extract their coefficients. Thus the form is positive definite on every finite tensor span. Its completion is the Hilbert tensor power $H^{\otimes n}$ .

2.1step 1.1algebra

Each $U_{π}$ is unitary and $U_{π} U_{τ} = U_{π τ}$ . Replacing $π$ by $π^{- 1}$ in the adjoint sum gives $A_{n}^{*} = A_{n}$ ; grouping the $n!$ pairs with product $ρ$ gives $A_{n}^{2} = A_{n}$ . Thus $A_{n}$ is an orthogonal projection and is bounded with norm at most $1$ by the orthogonal decomposition into its range and kernel. Its range is closed. It is exactly the alternating subspace because the signed average is alternating and fixes every alternating tensor.

2.2A3A4step 1.1

Let $C$ be any bound for $T$ from [A3]. After permuting tensor factors, a finite tensor sum can be written $\sum_{j = 1}^{m} x_{j} \otimes y_{j}$ with $(y_{j})$ an orthonormal basis of the finite-dimensional span of its remaining-factor tensors. Its squared norm is $\sum_{j} ∥ x_{j} ∥^{2}$ , while applying $T$ in that factor gives squared norm $\sum_{j} ∥ T x_{j} ∥^{2} \leq C^{2} \sum_{j} ∥ x_{j} ∥^{2}$ . Since factor permutations are unitary, this proves the bound $C$ for applying $T$ in any one slot. Composing over the $n$ slots extends $T^{\otimes n}$ to the completion with bound $C^{n}$ .

3.1A1A2step 2.1

By step 2.1 the normalized wedges are vectors in the alternating range. For pure tensors, self-adjointness and idempotence give $⟨ \sqrt{n!} A_{n} x, \sqrt{n!} A_{n} y ⟩ = n! ⟨ x, A_{n} y ⟩$ . Expanding the signed average yields $\sum_{π \in S_{n}} sgn (π) \prod_{i} ⟨ x_{i}, y_{π (i)} ⟩$ , which is the determinant in [A2]. This proves the stated Gram formula and its positivity from the Hilbert-space norm.

3.2A3step 2.1step 2.2

On elementary tensors $T^{\otimes n}$ commutes with every permutation, hence preserves $ran A_{n}$ and restricts to a bounded $Λ^{n} T$ with bound $C^{n}$ . Its action on wedges is the displayed formula. Applying that formula twice proves $Λ^{n} (S T) = Λ^{n} S Λ^{n} T$ on a dense span and therefore everywhere. For $n = 0$ the space is $C$ and the induced map is its identity; for $n = 1$ , $A_{1} = I$ and $Λ^{1} T = T$ . If $T = 0$ and $n \geq 1$ , its induced map is zero.

4.1A5step 2.1step 3.1construct∎

If $(e_{j})$ is a supplied orthonormal basis of $H$ , its finite span is dense by [A5]. Approximate the factors of each elementary tensor by finite linear combinations of the $e_{j}$ . The telescoping tensor identity and $∥ x_{1} \otimes \dots \otimes x_{n} ∥ = \prod_{r} ∥ x_{r} ∥$ show that elementary tensors in those finite spans are dense in $H^{\otimes n}$ . Since $A_{n}$ is bounded, their images are dense in $ran A_{n}$ . Applying $A_{n}$ to a basis tensor gives zero if indices repeat and otherwise a signed multiple of the wedge with increasing indices. These wedges are orthonormal by step 3.1 and span a dense subspace, so they form an orthonormal basis of $Λ^{n} H$ . If $H$ is finite-dimensional with $n > \dim H$ , there are no increasing $n$ -tuples and $Λ^{n} H = {0}$ .

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30Open item page →

Trace-norm bound for exterior powers of trace-class operators

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H$ be a separable complex Hilbert space and let $T : H \to H$ be trace class (Trace class operator). For every integer $n \geq 0$ , the induced operator $(Λ^{n} T) : Λ^{n} H \to Λ^{n} H$ is trace class. If $n \geq 1$ and $J_{T}$ indexes the positive singular values $(s_{j} (T))_{j \in J_{T}}$ with multiplicity, then the positive singular values of $Λ^{n} T$ , with multiplicity, are ${\prod_{k = 1}^{n} s_{j_{k}} (T) : (j_{1}, \dots, j_{n}) \in J_{T}^{n}, j_{1} < \dots < j_{n}} .$ Consequently, $∥ Λ^{n} T ∥_{1} = \sum_{j_{1} < \dots < j_{n}} s_{j_{1}} (T) \dots s_{j_{n}} (T) \leq \frac{∥ T ∥_{1}^{n}}{n!} .$ For $n = 0$ , $Λ^{0} T = I_{C}$ is trace class and $tr (Λ^{0} T) = 1$ ; its singular-value list is $1$ followed by zeros.

Facts & Assumptions

Given: ${A C}_{ω}$ , a separable complex Hilbert space $H$ , a trace-class operator $T : H \to H$ , and an integer $n \geq 0$ .

[A1]

The wedge inner product is the Gram determinant (Hilbert exterior powers and induced operators).

[A2]

The exterior power is the range of the stated orthogonal antisymmetrizing projection (Hilbert exterior powers and induced operators).

[A3]

The wedge is defined by applying that projection to a tensor; the induced operator has the stated wedge action, is bounded, and is functorial (Hilbert exterior powers and induced operators).

[A4]

The SVD of $T$ supplies a finite or countably infinite positive index set $J_{T}$ , positive singular values in nonincreasing order, orthonormal families $(e_{j})$ and $(f_{j})$ , a Hilbert basis $(e_{j})$ of $(\ker T)^{⊥}$ , the expansion $T x = \sum_{j} s_{j} (T) ⟨ x, e_{j} ⟩ f_{j}$ , and a partial isometry $U$ with $T = U ∣ T ∣$ and $U^{*} U$ the orthogonal projection onto $(\ker T)^{⊥}$ (Singular value decomposition for compact operators).

[A5]

Under ${A C}_{ω}$ , every at-most-countable family of nonempty sets has a choice function; the SVD is stated under this hypothesis and its proof selects bases from the countable family of finite-dimensional singular eigenspaces (The Axiom of Countable Choice ( ${A C}_{ω}$ ), Singular value decomposition for compact operators).

[A6]

Trace class means compactness and $∥ T ∥_{1} = \sum_{j} s_{j} (T) < \infty$ ; $∥ T ∥ = s_{1} (T)$ and the singular values tend to zero when the list is infinite (Trace class operator, Absolute value and singular values of a compact operator).

[A7]

Under ${A C}_{ω}$ , a norm limit of compact operators into a Banach space is compact (Norm limit of compact operators is compact).

[A8]

For a compact operator $S$ , its positive singular values with multiplicity are the positive eigenvalues of $∣ S ∣ = (S^{*} S)^{1 / 2}$ (Absolute value and singular values of a compact operator).

[A9]

A nonnegative family is summable when its finite subsums are bounded, and its sum is the supremum of those finite subsums; the finite power of a countable set and every subset of a countable set are countable (Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ , Every finite power of an at most countable set is at most countable, Every subset of an at most countable set is at most countable).

[A10]

For a trace-class operator, the basis-free trace equals the scalar sum of any nuclear representation (Trace is absolutely convergent and basis independent).

[A11]

The degree-zero exterior space is $Λ^{0} H = C$ (Hilbert exterior powers and induced operators).

[A12]

A complex Hilbert space is a complete inner-product space and hence a Banach space for its induced norm (Hilbert space).

[A13]

For a complete orthonormal family $(e_{i})_{i \in I}$ in a Hilbert space, Countable Choice and Parseval's theorem give $\sum_{i \in I} ∣ ⟨ x, e_{i} ⟩ ∣^{2} = ∥ x ∥^{2}$ for every $x$ (Parseval equivalences for an orthonormal family).

[A14]

A bounded finite-rank operator whose range has a finite ordered basis is compact (Bounded finite rank operators are compact).

[A15]

The positive square root of a compact positive operator is unique, and positivity means its quadratic form is nonnegative (Positive square root of a compact positive operator, Self-adjoint, positive, unitary and normal operators).

[A16]

The Hilbert adjoint is characterized uniquely by $⟨ S x, y ⟩ = ⟨ x, S^{*} y ⟩$ ; in particular $I_{C}^{*} = I_{C}$ by this identity and uniqueness (The Hilbert-space adjoint of a bounded operator, Hilbert-adjoint identities).

Choice accounting: The exact hypothesis is ${A C}_{ω}$ . It supplies the countably many SVD eigenspace-basis choices [A4, A5] and is an explicit hypothesis of Parseval [A13]; the trace-class/singular-value definitions are stated under it [A6]; the adjoint and positive-square-root suppliers assume it [A15, A16]; the norm-limit compactness theorem uses it [A7]; and the basis-free trace theorem used in degree zero assumes it [A10]. No basis of all of $H$ is selected: the proof uses only the SVD basis of $(\ker T)^{⊥}$ . Separability is retained from the assigned claim, though these arguments do not otherwise require it.

Proof

technique · direct

Given: The data in the statement, the positive singular-value index set $J_{T}$ , the SVD families $(e_{j})$ and $(f_{j})$ , and $P : = U^{*} U$ from [A4].

1.1A3A6A8A10A11A14A15A16

If $n = 0$ , [A11] gives $Λ^{0} H = C$ and [A3] gives $Λ^{0} T = I_{C}$ . Its range has the one-element ordered orthonormal basis $(1)$ , so it is compact by [A14]. [A16] gives $I_{C}^{*} = I_{C}$ ; the identity is positive and its positive square root is itself, so [A15] gives $∣ I_{C} ∣ = I_{C}$ . Thus its only positive singular value is $1$ , with the remaining sequence entries zero by [A8]. By [A6], $I_{C}$ is trace class and has trace norm $1$ . Now the rank-one nuclear representation $I_{C} x = ⟨ x, 1 ⟩ 1$ has scalar trace sum $⟨ 1, 1 ⟩ = 1$ , so [A10] gives $tr (Λ^{0} T) = 1$ .

1.2A3A4A6

Henceforth let $n \geq 1$ . If $J_{T} = \emptyset$ , then $T = 0$ by [A4], so $Λ^{n} T = 0$ ; the singular-value product family is empty and the trace norm and bound are both zero.

1.3A1A4A5

Suppose $J_{T} \neq \emptyset$ , put $K : = (\ker T)^{⊥}$ , and define $I_{n} : = {(j_{1}, \dots, j_{n}) \in J_{T}^{n} : j_{1} < \dots < j_{n}}$ . For each $J = (j_{1} < \dots < j_{n}) \in I_{n}$ set $η_{J} : = e_{j_{1}} \land \dots \land e_{j_{n}}$ , $θ_{J} : = f_{j_{1}} \land \dots \land f_{j_{n}}$ , and $μ_{J} : = \prod_{k = 1}^{n} s_{j_{k}} (T)$ . The Gram determinant in [A1] makes both families orthonormal.

1.4A6A9

Let $F$ be any finite subset of $I_{n}$ and choose $N$ at least every index appearing in $F$ . Expanding $(\sum_{j = 1}^{N} s_{j} (T))^{n} = \sum_{(i_{1}, \dots, i_{n}) \in {1, \dots, N}^{n}} s_{i_{1}} (T) \dots s_{i_{n}} (T)$ shows it is at least $n! \sum_{J \in F} μ_{J}$ , because every increasing tuple in $F$ contributes its $n!$ distinct permutations and all other terms are nonnegative. The left side is at most $∥ T ∥_{1}^{n}$ by [A6]. Taking the supremum over finite $F$ in [A9] proves $\sum_{J \in I_{n}} μ_{J} \leq ∥ T ∥_{1}^{n} / n!$ .

2.1A1A2A3A4A5step 1.3

From the SVD expansion, $(e_{j})$ is total in $K$ : if $x \in K$ is orthogonal to every $e_{j}$ , then $T x = 0$ , so $x \in K \cap \ker T = {0}$ . Thus finite linear combinations of $(e_{j})$ are dense in $K$ . Functoriality and $T = T P$ give $S : = Λ^{n} T = S Λ^{n} P$ ; the Gram identity and self-adjointness of $P$ show $Λ^{n} P$ is self-adjoint, while functoriality and $P^{2} = P$ show it is idempotent. Its range is the closed span $M$ of the $η_{J}$ : on dense decomposable wedges, $Λ^{n} P$ gives wedges of vectors in $K$ , and approximating each such vector by finite linear combinations of $(e_{j})$ , then expanding by multilinearity, places that wedge in $M$ . Continuity follows from the antisymmetrizer tensor construction in [A2]. Conversely, every $η_{J}$ is fixed by $Λ^{n} P$ . Thus $Λ^{n} P$ is the orthogonal projection onto $M$ and $S$ vanishes on $M^{⊥}$ .

3.1A2A3A4A5A6A7A12A13A14step 2.1

On each basis wedge, $S η_{J} = μ_{J} θ_{J}$ . For each $N$ let $S_{N} x : = \sum_{J \in I_{n}, j_{n} \leq N} μ_{J} ⟨ x, η_{J} ⟩ θ_{J}$ ; this is bounded and finite rank, hence compact by [A14]. By [step 2.1], both $S$ and $S_{N}$ vanish on $M^{⊥}$ , and $(η_{J})$ is a complete orthonormal family in $M$ , its closed span. For $x \in M$ , Parseval [A13] and orthonormality of $(θ_{J})$ give $∥ (S - S_{N}) x ∥^{2} = \sum_{J : j_{n} > N} μ_{J}^{2} ∣ ⟨ x, η_{J} ⟩ ∣^{2} \leq (s_{N + 1} (T) s_{1} (T)^{n - 1})^{2} ∥ x ∥^{2}$ , because each omitted tuple has largest index greater than $N$ . Decomposing a general vector into $M \oplus M^{⊥}$ therefore gives $∥ S - S_{N} ∥ \leq s_{N + 1} (T) s_{1} (T)^{n - 1}$ when $J_{T}$ is infinite. If $J_{T}$ is finite, $S_{N} = S$ for $N \geq ∣ J_{T} ∣$ . Therefore $S_{N} \to S$ in operator norm and [A7] makes $S$ compact. The target $Λ^{n} H$ is Banach by its Hilbert construction [A2, A12].

4.1A1A3A4A6A7A8A14A15A16step 2.1step 3.1

Define $D η_{J} : = μ_{J} η_{J}$ on the orthonormal basis of $M$ and set $D = 0$ on $M^{⊥}$ ; since $0 \leq μ_{J} \leq s_{1} (T)^{n} = ∥ T ∥^{n}$ , this diagonal rule extends boundedly. Its finite diagonal truncations $D_{N}$ (retaining only tuples with all indices at most $N$ ) have finite rank and are compact by [A14], and converge in norm by the coefficient estimate of [step 3.1] with output vectors $η_{J}$ instead of $θ_{J}$ . Thus [A7] makes $D$ compact; its real nonnegative diagonal coefficients make it positive and self-adjoint. By [step 2.1, step 3.1] and the adjoint identity [A16], for $x \in Λ^{n} H$ the expansion of $S x$ in the $θ_{J}$ gives $⟨ S x, θ_{J} ⟩ = μ_{J} ⟨ x, η_{J} ⟩ = ⟨ x, μ_{J} η_{J} ⟩$ , hence $S^{*} θ_{J} = μ_{J} η_{J}$ and $S^{*} S η_{J} = μ_{J}^{2} η_{J} = D^{2} η_{J}$ ; both operators vanish on $M^{⊥}$ , so $S^{*} S = D^{2}$ . Uniqueness of the compact positive square root in [A15] yields $D = ∣ S ∣$ by the definition [A8].

5.1A4A6A8step 4.1

By [step 4.1], the positive eigenvalues of $∣ S ∣$ , counted with multiplicity, are exactly the values $μ_{J}$ over $J \in I_{n}$ : the $η_{J}$ form a basis of its support $M$ and $D$ is diagonal there. By the compact-operator singular-value definition [A8], these are precisely the positive singular values of $S = Λ^{n} T$ ; the remaining entries of its singular-value sequence are zero padding.

6.1A4A6A9step 5.1step 1.4∎

The tuple index set $I_{n}$ is countable by [A9], and [step 5.1] identifies its nonnegative family, with multiplicities, with the singular values of $S$ . Thus [step 1.4] says their singular-value series converges, so $S$ is trace class by [A6] and its trace norm equals that sum. This proves the equality and factorial bound in the statement. If $n$ exceeds the finite rank of $T$ , $I_{n} = \emptyset$ and $S = 0$ ; if $n = 1$ , the tuples are single indices and the sum is exactly $∥ T ∥_{1}$ .

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30Open item page →

Weyl product and sum inequalities for compact operators

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $H$ be a complex Hilbert space and let $T : H \to H$ be compact (Hilbert space, Compact linear operator). List the nonzero eigenvalues of $T$ , repeated according to algebraic multiplicity (Algebraic multiplicity of a nonzero compact-operator eigenvalue) and ordered so that $∣ λ_{1} (T) ∣ \geq ∣ λ_{2} (T) ∣ \geq \dots$ ; if this list is finite, pad it with zeros. Let $s_{1} (T) \geq s_{2} (T) \geq \dots$ be the zero-padded singular-value sequence (Absolute value and singular values of a compact operator). For every integer $N \geq 0$ , with an empty product equal to $1$ when $N = 0$ , $\prod_{j = 1}^{N} ∣ λ_{j} (T) ∣ \leq \prod_{j = 1}^{N} s_{j} (T) .$ If $T$ is trace class (Trace class operator), then $\sum_{j \geq 1} ∣ λ_{j} (T) ∣ \leq \sum_{j \geq 1} s_{j} (T) = ∥ T ∥_{1} .$

Facts & Assumptions

Given: AC, a complex Hilbert space $H$ , a compact operator $T : H \to H$ , its eigenvalue list with algebraic multiplicity, and its singular-value list.

[A1]

AC is the choice-function axiom and supplies the prescribed-initial-point form of Dependent Choice used in the Riesz–Schauder supplier (The Axiom of Choice, AC supplies the countable and dependent choices used in Banach integration).

[A2]

AC implies Countable Choice, which supplies the narrower hypotheses of the SVD, singular-value, trace-class, and orthogonal-decomposition suppliers (AC supplies the countable and dependent choices used in Banach integration).

[A3]

Every nonzero spectral value of a compact operator is an eigenvalue with finite-dimensional generalized eigenspace, and only finitely many spectral values have modulus at least any fixed $ε > 0$ (Riesz schauder spectrum of a compact operator).

[A4]

For each nonzero eigenvalue $λ$ , its generalized eigenspace is $G_{λ} (T) = \ker (T - λ I)^{m_{λ}}$ for a stabilized exponent $m_{λ}$ , is finite-dimensional, and has dimension equal to its algebraic multiplicity (Algebraic multiplicity of a nonzero compact-operator eigenvalue). Thus $(T - λ I) ∣_{G_{λ} (T)}$ is nilpotent.

[A5]

Every nilpotent endomorphism of a finite-dimensional vector space has a basis arranged in Jordan strings; each string has an initial invariant segment of every length from zero through its full length by the definition of a Jordan string (Every finite-dimensional nilpotent endomorphism has a basis of Jordan strings, Jordan blocks, Jordan strings, and their endpoints).

[A6]

Under Countable Choice, the singular values of $T$ have a finite or countably infinite positive list $(s_{j})_{j \in J_{T}}$ , with orthonormal families $(e_{j})$ , $(f_{j})$ , SVD expansion $T x = \sum_{j \in J_{T}} s_{j} ⟨ x, e_{j} ⟩ f_{j}$ , and partial isometry $U$ such that $T = U ∣ T ∣$ and $U^{*} U$ is the orthogonal projection onto $(\ker T)^{⊥}$ ; the singular values are nonincreasing and $s_{1} (T) = ∥ T ∥$ (Singular value decomposition for compact operators, Absolute value and singular values of a compact operator).

[A7]

The exterior space is the alternating range in the Hilbert tensor power; its wedges have Gram-determinant inner product, the induced map obeys $(Λ^{N} T) (x_{1} \land \dots \land x_{N}) = T x_{1} \land \dots \land T x_{N}$ , is bounded, and is functorial (Hilbert exterior powers and induced operators).

[A8]

The determinant is the signed permutation sum and the determinant of a triangular matrix is the product of its diagonal entries (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix, The determinant of a triangular matrix is the product of its diagonal entries).

[A9]

The operator norm bounds the norm of every image vector: $∥ S x ∥ \leq ∥ S ∥ ∥ x ∥$ (The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

[A10]

For trace-class $T$ , the singular-value series converges and its sum is $∥ T ∥_{1}$ (Trace class operator).

[A11]

Every closed subspace of a Hilbert space has an orthogonal complement that gives a direct-sum decomposition (Orthogonal decomposition by a closed subspace).

[A12]

Under Countable Choice, a countable union of at most countable sets is at most countable; in particular this applies to a sequence of finite sets (Countable unions of at most countable sets, assuming ${A C}_{ω}$ ).

[A13]

For a complete orthonormal family, Parseval's identity holds and the finite-subset coefficient net converges in norm to each vector (Parseval equivalences for an orthonormal family).

[A14]

A decomposable wedge in a finite-dimensional vector space is nonzero exactly when its factors are linearly independent (In a finite-dimensional vector space, a decomposable wedge is nonzero exactly when its vectors are linearly independent).

[A15]

The positive part $r_{+} : = \max {r, 0}$ is continuous when $r$ is a continuous real function; the exponential is continuous and strictly positive (Maximum and minimum of a set, The real exponential function and the number $e$ by a power series, Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, The exponential function is strictly increasing, The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ ).

[A16]

Continuous real functions on a compact interval are Riemann integrable; the integral preserves pointwise order, is linear on a common interval, and is additive over subintervals. The integral of the zero function is zero (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ , Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ , For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ , If $m \leq f \leq M$ on $[a, b]$ then $m (b - a) \leq L (f, P) \leq \underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f \leq U (f, P) \leq M (b - a)$ for every partition $P$ ; in particular every constant function is integrable, with $\int_{a}^{b} c = c (b - a)$ ).

[A17]

The product rule and $(\exp)^{'} = \exp$ hold, and the second fundamental theorem evaluates an integral of a continuous derivative on a compact interval (The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set, Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The exponential function is smooth and $(\exp)^{'} = \exp$ , The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ ).

[A18]

For every fixed real $c$ , as $R \to + \infty$ , $(R + c) \exp (c - R) \to 0$ : use the exponential addition and reciprocal laws to write $\exp (c - R) = \exp (c) / \exp (R)$ , then bound $∣ R + c ∣$ by $2 R$ for sufficiently large $R$ and apply $R / \exp (R) \to 0$ . The latter is the case $m = 1$ , $a = 1$ of the exponential-beats-polynomials theorem (Limits at $+ \infty$ and $- \infty$ , and infinite limits at a point, The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ , The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ , The exponential dominates every fixed nonnegative integer power at $+ \infty$ ).

[A19]

For every $q > 0$ , $\exp (\log q) = q$ by the inverse definition of the natural logarithm (The natural logarithm as the inverse of the exponential function).

[A20]

The natural logarithm is strictly increasing and satisfies $\log (a b) = \log a + \log b$ for $a, b > 0$ (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[A21]

For a nonnegative real series, convergence is equivalent to bounded partial sums, and its sum is the supremum of those partial sums (Series, partial sums, convergence and the sum, divergence, and the tail series, A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum).

[A22]

Every nonempty finite set of real numbers has a maximum and a minimum (Maximum and minimum of a set, Every nonempty finite set of reals has a maximum and a minimum).

[A23]

For every positive real $ε$ there is $m \geq 1$ with $1 / m < ε$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

[A24]

A real $x$ is nonzero exactly when $∣ x ∣ > 0$ (Basic properties of the absolute value).

Choice accounting: The exact statement assumes AC. The Riesz–Schauder and algebraic-multiplicity suppliers are AC-qualified; AC supplies the dependent choice used by the former [A1]. Countable Choice follows from AC by [A2] and is used by the countable-union theorem [A12], Parseval [A13], the SVD, the singular-value and trace-class suppliers, and orthogonal decomposition; SVD uses it to select bases in the countable family of finite-dimensional singular eigenspaces. The Jordan-string choices are finite and local to each prefix. No basis of all of $H$ is selected.

Proof

technique · direct

Given: The data in the statement, and for a fixed finite positive-eigenvalue prefix the stabilized exponents $m_{λ}$ from [A4].

1.1A1A2A3A4A12A22A23A24

By [A1, A3, A4], the nonzero spectral values are eigenvalues of finite algebraic multiplicity, and there are only finitely many above any positive modulus threshold. Every nonzero spectral value lies in the threshold set ${λ : ∣ λ ∣ \geq 1 / m}$ for some $m \geq 1$ by [A23, A24]. Each threshold set is finite by [A3], so Countable Choice [A2] and [A12] make their union at most countable. Repeating each value according to its finite algebraic multiplicity still gives a countable list by another application of [A12]. If that list is infinite, after choosing any remaining value only finitely many remaining values have at least its modulus; that finite nonempty set has a maximum modulus by [A22], which is then maximal among all remaining values. Finite ties can be ordered arbitrarily. AC permits iterating this selection to obtain a sequence ordered by decreasing modulus. If $N = 0$ , both products are the empty product $1$ . If $N \geq 1$ and the zero-padded eigenvalue list has $λ_{N} (T) = 0$ , its first $N$ -term product is zero and the asserted inequality follows from nonnegativity of singular values. It remains to prove the claim when $N \geq 1$ and all of $λ_{1} (T), \dots, λ_{N} (T)$ are nonzero.

1.2A4A5

For each distinct eigenvalue $λ$ among this prefix, let $r_{λ}$ be its number of occurrences. Then $r_{λ} \leq \dim G_{λ} (T)$ by [A4]. Apply [A5] to $(T - λ I) ∣_{G_{λ} (T)}$ and list the resulting finite Jordan-string lengths as $ℓ_{1}, \dots, ℓ_{q}$ . In that order, take an initial segment of length $k_{i} : = \min (ℓ_{i}, r_{λ} - \sum_{h < i} k_{h})$ from string $i$ while the residual is positive, and take length zero thereafter. Since $\sum_{i} ℓ_{i} = \dim G_{λ} (T) \geq r_{λ}$ , these lengths sum to $r_{λ}$ . The definition in [A5] makes each selected initial segment invariant under $T$ , so their direct sum $F_{λ}$ is $T$ -invariant, has dimension $r_{λ}$ , and the restriction of $T$ to it is triangular with diagonal entry $λ$ repeated $r_{λ}$ times.

1.3A2A6A7A11A13A14

Put $S : = Λ^{N} T$ , $K : = (\ker T)^{⊥}$ , and $P : = U^{*} U$ , the orthogonal projection onto $K$ from [A6]. For every increasing $N$ -tuple $J = (j_{1} < \dots < j_{N})$ in $J_{T}$ , set $η_{J} : = e_{j_{1}} \land \dots \land e_{j_{N}}$ , $θ_{J} : = f_{j_{1}} \land \dots \land f_{j_{N}}$ , and $μ_{J} : = \prod_{k = 1}^{N} s_{j_{k}} (T)$ . By the Gram formula [A7], both wedge families are orthonormal. The $e_{j}$ span $K$ : if their closed span were proper, [A11] would give a nonzero $x \in K$ orthogonal to all $e_{j}$ , while the SVD expansion [A6] would imply $T x = 0$ , contradicting $K \cap \ker T = {0}$ . Since decomposable wedges are dense by the exterior construction, approximating each factor by finite $e_{j}$ -sums and expanding by multilinearity shows that the $η_{J}$ span $Λ^{N} K$ . The tensor projection $P^{\otimes N}$ is self-adjoint and idempotent and commutes with permutations; its restriction to the alternating range is $Λ^{N} P$ , the orthogonal projection onto $M : = \overset{}{span} {η_{J}}$ . Since $T = T P$ , functoriality [A7] gives $S = S Λ^{N} P$ , so $S$ vanishes on $M^{⊥}$ . On each $η_{J}$ , $S η_{J} = μ_{J} θ_{J}$ . If there are at least $N$ positive singular values, the family $(η_{J})$ is a complete orthonormal family in $M$ . For $x \in M$ , Parseval and net convergence [A13] give $x_{F} : = \sum_{J \in F} c_{J} η_{J} \to x$ over finite subsets $F$ , with $c_{J} = ⟨ x, η_{J} ⟩$ . Orthonormality of both wedge families gives $∥ S x_{F} ∥^{2} = \sum_{J \in F} μ_{J}^{2} ∣ c_{J} ∣^{2} \leq (\sup_{J} μ_{J})^{2} \sum_{J \in F} ∣ c_{J} ∣^{2} = (\sup_{J} μ_{J})^{2} ∥ x_{F} ∥^{2}$ . Since $S$ is bounded [A7], passing to the norm limit yields $∥ S x ∥ \leq (\sup_{J} μ_{J}) ∥ x ∥$ . The unit vector $η_{(1, \dots, N)}$ attains $\sup_{J} μ_{J} = \prod_{j = 1}^{N} s_{j} (T)$ , because every increasing tuple has $s_{j_{k}} (T) \leq s_{k} (T)$ . If there are fewer than $N$ positive singular values, $K$ is finite-dimensional of dimension less than $N$ , so every decomposable $N$ -wedge in $K$ vanishes by [A14]; density gives $Λ^{N} K = {0}$ and $S = 0$ , the same norm formula holding with $s_{N} (T) = 0$ .

2.1A4step 1.2

The spaces $G_{λ} (T)$ for the finitely many distinct prefix values form a direct sum: if $\sum_{ν} x_{ν} = 0$ with $x_{ν} \in G_{ν} (T)$ , fix $λ$ and apply $Q_{λ} : = \prod_{ν \neq λ} (T - ν I)^{m_{ν}}$ . It kills every $x_{ν}$ for $ν \neq λ$ . On $G_{λ} (T)$ each factor is $(λ - ν) I + N_{λ}$ , where $N_{λ} = (T - λ I) ∣_{G_{λ}}$ is nilpotent, so that factor is invertible by its finite geometric-series inverse. Thus $Q_{λ} ∣_{G_{λ}}$ is invertible and $x_{λ} = 0$ . Consequently $E_{N} : = ⨁_{λ} F_{λ}$ is a $T$ -invariant $N$ -dimensional subspace.

3.1A7A8A14step 2.1

Choose the concatenated Jordan-segment basis $v_{1}, \dots, v_{N}$ of $E_{N}$ and put $w : = v_{1} \land \dots \land v_{N}$ . The vectors are linearly independent by their being a basis, so [A14] gives $w \neq 0$ . If $A$ is the triangular matrix of $T ∣_{E_{N}}$ in this basis, multilinearity and alternation [A7] expand $(T v_{1}) \land \dots \land (T v_{N}) = \det (A) w$ . By [A8], $\det (A) = \prod_{j = 1}^{N} λ_{j} (T)$ . Hence $(Λ^{N} T) w = (\prod_{j = 1}^{N} λ_{j} (T)) w$ .

4.1A9step 1.1step 3.1step 1.3

In the nonzero-prefix case of step 1.1, step 3.1 gives an eigenvector of $S$ with eigenvalue $\prod_{j = 1}^{N} λ_{j} (T)$ . The operator-norm bound [A9] and norm identity [step 1.3] yield $\prod_{j = 1}^{N} ∣ λ_{j} (T) ∣ \leq ∥ S ∥ = \prod_{j = 1}^{N} s_{j} (T)$ . Together with step 1.1 this proves the product inequality for every $N \geq 0$ .

5.1A6A20A24step 4.1

Fix $N \geq 1$ with $λ_{1} (T), \dots, λ_{N} (T)$ all nonzero. For each $k \leq N$ , step 4.1 gives the product inequality for the first $k$ terms. Its left side is positive, hence $s_{k} (T) > 0$ . The eigenvalue moduli are positive by [A24], so set $x_{j} : = \log ∣ λ_{j} (T) ∣$ and $y_{j} : = \log s_{j} (T)$ for $j \leq N$ . Both sequences are nonincreasing because modulus, singular values and logarithm preserve the indicated order; taking logarithms in the product inequalities and using the logarithm product law [A20] gives $\sum_{j = 1}^{k} x_{j} \leq \sum_{j = 1}^{k} y_{j}$ for every $k \leq N$ .

6.1A15A16A17A18A19A22step 5.1algebra

For a nonincreasing real list $x_{1}, \dots, x_{N}$ and real $t$ , $\sum_{j = 1}^{N} (x_{j} - t)_{+} = \max_{0 \leq k \leq N} (\sum_{j = 1}^{k} x_{j} - k t)$ , where the $k = 0$ sum is zero: the positive terms form an initial segment, and adding any nonpositive later term cannot increase the prefix sum. This finite maximum exists by [A22]. Applying the identity to the lists in step 5.1 and their prefix-sum inequalities gives $\sum_{j = 1}^{N} (x_{j} - t)_{+} \leq \sum_{j = 1}^{N} (y_{j} - t)_{+}$ for every $t \in R$ . Put $c : = \min {x_{N}, y_{N}} - 1$ and $b : = \max {x_{1}, y_{1}} + 1$ , so $c < x_{j}, y_{j} < b$ for every $j$ , and for $R \geq 0$ put $a_{R} : = c - R$ and $ϕ_{u} (t) : = (u - t)_{+} \exp (t)$ . By [A15, A16], these functions and their finite sums are continuous and integrable on $[a_{R}, b]$ ; since $\exp (t) > 0$ , the positive-part inequality remains true after multiplication by $\exp (t)$ . Monotonicity and linearity of the integral [A16] give $\sum_{j} \int_{a_{R}}^{b} ϕ_{x_{j}} (t) d t \leq \sum_{j} \int_{a_{R}}^{b} ϕ_{y_{j}} (t) d t$ . Fix any $u$ among these finitely many $x_{j}, y_{j}$ . On $[a_{R}, u]$ , $ϕ_{u} (t) = (u - t) \exp (t)$ , whose primitive is $G_{u} (t) : = (u - t + 1) \exp (t)$ : directly from the derivative definition [A17], $(u - t + 1)^{'} = - 1$ , and the product rule and $(\exp)^{'} = \exp$ give $G_{u}^{'} (t) = (u - t) \exp (t)$ . On $[u, b]$ , $ϕ_{u} = 0$ . Applying the fundamental theorem, the zero-integral case and interval additivity [A16, A17] yields $\int_{a_{R}}^{b} ϕ_{u} (t) d t = \exp (u) - (u - a_{R} + 1) \exp (a_{R})$ . The error $E_{u, R} : = (u - a_{R} + 1) \exp (a_{R}) = (R + u - c + 1) \exp (c - R)$ is nonnegative and tends to zero: for sufficiently large $R$ , it is at most $2 \exp (c) R / \exp (R)$ , which tends to zero by [A18]. Because there are finitely many $x_{j}$ , for every $ε > 0$ one common sufficiently large $R$ makes $\sum_{j} E_{x_{j}, R} < ε$ . The integral inequality then gives $\sum_{j} \exp (x_{j}) \leq \sum_{j} \exp (y_{j}) + ε$ , since $E_{y_{j}, R} \geq 0$ . As $ε$ was arbitrary, [A19] gives $\sum_{j = 1}^{N} ∣ λ_{j} (T) ∣ \leq \sum_{j = 1}^{N} s_{j} (T)$ .

7.1A10A21step 6.1∎

If the nonzero eigenvalue list is finite with length $m > 0$ , step 6.1 at $N = m$ bounds its full absolute sum; for $m = 0$ that sum is zero. If the list is infinite, step 6.1 bounds every eigenvalue partial sum by the corresponding singular-value partial sum, which is at most $∥ T ∥_{1}$ by trace class [A10]. The eigenvalue terms are nonnegative, so [A21] gives convergence of their series and bounds its sum, the supremum of its partial sums, by $∥ T ∥_{1}$ . Zero padding changes neither sum, and [A10] identifies the singular-value sum with $∥ T ∥_{1}$ . This proves the sum conclusion, including finite-rank and zero operators.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30Open item page →

Diagonal trace-class operators on $ℓ^{2} (N, C)$

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $H : = ℓ^{2} (N, C)$ be the space of square-summable complex families with its pairing, norm and induced metric (Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ , Real and complex inner-product spaces and their induced length), and for $n \in N$ let $u_{n} \in H$ be the family that is $1$ at $n$ and $0$ elsewhere. Then:

$H$ is a complex Hilbert space (Hilbert space) and $(u_{n})_{n \in N}$ is a complete orthonormal family in $H$ (Orthonormal families, complete orthonormal systems and Hilbert bases).
For every bounded complex sequence $c = (c_{n})_{n \in N}$ the series $D_{c} x : = \sum_{n \in N} c_{n} ⟨ x, u_{n} ⟩ u_{n}$ converges in $H$ for every $x \in H$ , and $D_{c}$ is a bounded linear operator with $D_{c} u_{n} = c_{n} u_{n}$ and $∥ D_{c} ∥ \leq \sup_{n} ∣ c_{n} ∣$ (A bounded linear operator between normed spaces, The operator norm as the least bound and as the unit-sphere or unit-ball supremum). For bounded $c, c^{'}$ and $λ \in C$ , $D_{c} + D_{c^{'}} = D_{c + c^{'}}, λ D_{c} = D_{λ c}, D_{c} D_{c^{'}} = D_{c c^{'}},$ with $D_{0} = 0$ and $D_{(1)} = I_{H}$ the zero and identity operators of $H$ , and $D_{c}$ is boundedly invertible if and only if $\inf_{n} ∣ c_{n} ∣ > 0$ ; in that case $D_{c}^{- 1} = D_{c^{- 1}}$ .
If in addition $\sum_{n \in N} ∣ c_{n} ∣ < + \infty$ , then $D_{c}$ is trace class (Trace class operator) with $∥ D_{c} ∥_{1} = \sum_{n \in N} ∣ c_{n} ∣$ and $tr (D_{c}) = \sum_{n \in N} c_{n}$ (Trace of a trace class operator), and its nonzero eigenvalues, repeated according to algebraic multiplicity (Algebraic multiplicity of a nonzero compact-operator eigenvalue), are exactly the nonzero scalars of the list $(c_{n})_{n \in N}$ , each nonzero $λ$ occurring exactly $# {n : c_{n} = λ}$ times.

Facts & Assumptions

Given: AC; the square-summable space $H = ℓ^{2} (N, C)$ with its coordinate vectors $u_{n}$ ; a bounded complex sequence $c$ , and in the final part a summable one with $\sum_{n} ∣ c_{n} ∣ < + \infty$ .

[A1]

AC is the axiom of choice, and it implies Dependent Choice and Countable Choice (The Axiom of Choice, AC implies DC implies countable choice).

[A2]

On $ℓ^{2} (N, C)$ the vector operations are pointwise, $Q (a) : = \sum_{n} ∣ a_{n} ∣^{2}$ is the supremum of the finite subsums and $∥ a ∥^{2} = Q (a)$ for $a \in H$ , the pairing is $⟨ a, b ⟩ = \sum_{n} a_{n} \overline{b_{n}}$ , linear in the first and conjugate-linear in the second argument with $⟨ a, a ⟩ = ∥ a ∥^{2}$ ; for nonnegative families $\sum_{n} c_{n} = \sum_{n \in F} c_{n} + \sum_{n \notin F} c_{n}$ for every finite $F$ ; if $\sum_{n} c_{n} < + \infty$ then for every real $ε > 0$ there is a finite $F$ with $\sum_{n \notin F} c_{n} < ε$ ; and $u_{n}$ is the family that is $1$ at $n$ and $0$ elsewhere (Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ ).

[A3]

Cauchy–Schwarz gives $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , and squaring is monotone on the nonnegative reals: $0 \leq u \leq v$ implies $u^{2} \leq v^{2}$ (Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs, Squaring is monotone on the nonnegatives).

[A4]

The induced length of an inner-product space is a norm, so it satisfies the triangle inequality and vanishes only at $0$ ; its metric is the metric of convergence used below (The induced length is a norm, Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ , Real and complex inner-product spaces and their induced length).

[A5]

Bessel's inequality: for an orthonormal family $(e_{i})_{i \in I}$ and every $x$ , $\sum_{i} ∣ ⟨ x, e_{i} ⟩ ∣^{2} \leq ∥ x ∥^{2}$ , so the coefficient family lies in $ℓ^{2} (I, C)$ (The Bessel inequality for an arbitrary orthonormal family).

[A6]

Summation theorem: for an orthogonal family $(x_{i})$ with $\sum_{i} ∥ x_{i} ∥^{2} < + \infty$ the finite-subset net $\sum_{i \in F} x_{i}$ converges to a vector $s$ with $∥ s ∥^{2} = \sum_{i} ∥ x_{i} ∥^{2}$ ; in particular, for an orthonormal family $(e_{i})$ and $a \in ℓ^{2} (I, C)$ the net $\sum_{i \in F} a_{i} e_{i}$ converges to $s$ with $∥ s ∥^{2} = \sum_{i} ∣ a_{i} ∣^{2}$ and $⟨ s, e_{j} ⟩ = a_{j}$ for every $j$ (Square-summable orthogonal families have norm-convergent finite sums).

[A7]

Fourier expansion: in a complete orthonormal family $(e_{i})$ every $x$ equals the norm limit of the net $\sum_{i \in F} ⟨ x, e_{i} ⟩ e_{i}$ , and the coefficients are unique (Fourier expansion in a Hilbert space, Orthonormal families, complete orthonormal systems and Hilbert bases).

[A8]

Orthonormal means $⟨ e_{i}, e_{j} ⟩ = δ_{i j}$ ; every finite subfamily of an orthonormal family is linearly independent and coefficients in a finite expansion are unique; the span of a family is the set of its finite linear combinations and is a linear subspace, and the family is complete when that span is dense (Orthonormal families, complete orthonormal systems and Hilbert bases, Linear independence: a finite list $v : n \to V$ is independent when $\sum_{i < n} λ_{i} v_{i} = 0_{V}$ forces every $λ_{i} = 0_{F}$ , and a subset $S \subseteq V$ is independent when every injective finite list into $S$ is independent).

[A9]

A bounded linear operator satisfies $∥ S x ∥ \leq ∥ S ∥ ∥ x ∥$ with $∥ S ∥$ the unit-ball supremum; a bounded operator on a normed space is continuous on convergent nets (A bounded linear operator between normed spaces, The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

[A10]

Convergence in a metric space means $d (x_{k}, x) \to 0$ , a Cauchy sequence converges in a complete metric space, the complex plane $C$ is complete, and convergence in $C$ is convergence of real and imaginary parts (Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ , Cauchy sequence in a metric space, Complete metric space: every Cauchy sequence converges in the space, The complex plane is complete, and convergence is equivalent to convergence of real and imaginary parts, The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane).

[A11]

Algebra of limits: sums, scalar multiples and products of finitely many convergent real sequences converge to the corresponding combinations of the limits; with componentwise convergence in $C$ this gives the same statements for finitely many convergent complex sequences (Algebra of limits: sums, scalar multiples, products and quotients, The complex plane is complete, and convergence is equivalent to convergence of real and imaginary parts).

[A12]

A Hilbert space is a complete inner-product space, hence a Banach space: every Cauchy sequence converges (Hilbert space, Banach space, Complete metric space: every Cauchy sequence converges in the space).

[A13]

A net in a Hausdorff space has at most one limit; and if two nets in a normed space converge, then the net of termwise sums converges to the sum of the limits by the triangle inequality (A topological space is Hausdorff if and only if every net has at most one limit, The induced length is a norm).

[A14]

Bounded finite-rank operators are compact, and a norm limit of compact operators is compact (Bounded finite rank operators are compact, Norm limit of compact operators is compact).

[A15]

Nuclear series: a compact operator is trace class exactly when it has a nuclear representation, and then $∥ T ∥_{1}$ is the infimum of the nuclear sums, attained by the singular-value series (Nuclear series characterizes trace norm, Trace class operator).

[A16]

Trace: for a supplied Hilbert basis $E$ of $H$ the family $(⟨ T e, e ⟩)_{e \in E}$ is absolutely summable, and ${tr}_{E} (T) = \sum_{e \in E} ⟨ T e, e ⟩$ agrees with the basis-independent $tr (T)$ (Trace of a trace class operator, Trace is absolutely convergent and basis independent).

[A17]

Algebraic multiplicity: for a compact operator and a nonzero spectral value $λ$ , the generalized eigenspace is the stabilized kernel $\ker (T - λ I)^{m}$ and $m_{a l g} (λ; T)$ is its dimension (Algebraic multiplicity of a nonzero compact-operator eigenvalue).

[A18]

Weyl's inequality: for a compact operator on a complex Hilbert space, whose nonzero eigenvalues are listed with algebraic multiplicity and ordered by decreasing modulus, $\sum_{j} ∣ λ_{j} ∣ \leq ∥ T ∥_{1}$ whenever $T$ is trace class (Weyl product and sum inequalities for compact operators).

[A19]

A finite-dimensional space has a well-defined dimension, the common cardinality of all its bases, and the span of $k$ linearly independent vectors has dimension $k$ (Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis, Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis).

Proof

technique · direct

Given: AC; the space $H = ℓ^{2} (N, C)$ with coordinate vectors $u_{n}$ ; bounded complex sequences $c$ , $c^{'}$ ; a scalar $λ$ ; and, from step 7.2 on, $\sum_{n} ∣ c_{n} ∣ < + \infty$ .

1.1A2A8algebra

By [A2] every family in $H$ has pointwise coordinates, and for the coordinate vectors the finite-subset description of the pairing gives $⟨ u_{n}, u_{m} ⟩ = \sum_{k} u_{n} (k) \overline{u_{m} (k)} = u_{n} (n) \overline{u_{m} (n)} = δ_{n m}$ , all other terms being $0$ ; in particular $∥ u_{n} ∥ = 1$ and $u_{n} \neq 0$ .

2.1A2A3step 1.1

For $x \in H$ and $n \in N$ the pairing with $u_{n}$ picks out the $n$ -th coordinate, $⟨ x, u_{n} ⟩ = \sum_{k} x_{k} \overline{u_{n} (k)} = x_{n}$ , so by Cauchy–Schwarz and step 1.1 $∣ x_{n} ∣ = ∣ ⟨ x, u_{n} ⟩ ∣ \leq ∥ x ∥ ∥ u_{n} ∥ = ∥ x ∥$ .

2.2A2A3A7A8step 1.1algebra

The span of $(u_{n})$ is dense in $H$ : given $x \in H$ and a real $ε > 0$ , the finite sum $\sum_{n} ∣ x_{n} ∣^{2} = ∥ x ∥^{2}$ is finite, so by the small-tail property [A2] there is a finite $F$ with $\sum_{n \notin F} ∣ x_{n} ∣^{2} < ε^{2}$ . The vector $s : = \sum_{n \in F} x_{n} u_{n}$ lies in the span [A8], and the difference $x - s$ has coordinates $0$ on $F$ and $x_{n}$ off $F$ , so the splitting identity gives $∥ x - s ∥^{2} = \sum_{n \notin F} ∣ x_{n} ∣^{2} < ε^{2}$ and therefore $∥ x - s ∥ < ε$ by [A3]. Hence $(u_{n})$ is a complete orthonormal family in $H$ .

3.1A2A3A4A10A11A12step 2.1algebra

Let $(a^{(m)})_{m \in N}$ be a Cauchy sequence in $H$ ; for every $n$ step 2.1 applied to the differences $a^{(m)} - a^{(p)} \in H$ (pointwise operations, [A2]) gives $∣ a_{n}^{(m)} - a_{n}^{(p)} ∣ \leq ∥ a^{(m)} - a^{(p)} ∥$ , so each coordinate sequence is Cauchy in $C$ and converges to a scalar $a_{n}$ by [A10]. Fix a real $ε > 0$ and $M$ with $∥ a^{(m)} - a^{(p)} ∥ \leq ε$ for all $m, p \geq M$ . For a finite $F \subseteq N$ the sum $\sum_{n \in F} ∣ a_{n}^{(p)} - a_{n}^{(M)} ∣^{2}$ tends, as $p \to \infty$ , to $\sum_{n \in F} ∣ a_{n} - a_{n}^{(M)} ∣^{2}$ by [A11] applied to the finitely many coordinates, while every finite subsum of a square sum is at most that square sum [A2], so each value is at most $∥ a^{(p)} - a^{(M)} ∥^{2} \leq ε^{2}$ ; hence $\sum_{n \in F} ∣ a_{n} - a_{n}^{(M)} ∣^{2} \leq ε^{2}$ . Taking the supremum over finite $F$ gives $Q (a - a^{(M)}) \leq ε^{2} < + \infty$ , so $a - a^{(M)} \in H$ with $∥ a - a^{(M)} ∥ \leq ε$ by [A3], and $a = a^{(M)} + (a - a^{(M)}) \in H$ ; then for every $m \geq M$ the triangle inequality [A4] gives $∥ a^{(m)} - a ∥ \leq ∥ a^{(m)} - a^{(M)} ∥ + ∥ a^{(M)} - a ∥ \leq 2 ε$ . Thus $a^{(m)} \to a$ and $H$ is complete, hence a complex Hilbert space.

4.1A2A5A6A9step 3.1step 2.2

Let $c$ be bounded with $C : = \sup_{n} ∣ c_{n} ∣$ , and let $x \in H$ . The coefficients $b_{n} : = c_{n} ⟨ x, u_{n} ⟩$ satisfy $\sum_{n} ∣ b_{n} ∣^{2} \leq C^{2} \sum_{n} ∣ ⟨ x, u_{n} ⟩ ∣^{2} \leq C^{2} ∥ x ∥^{2} < + \infty$ by Bessel [A5], so by the summation theorem [A6] applied to the orthonormal family $(u_{n})$ in the Hilbert space $H$ the net $\sum_{n \in F} b_{n} u_{n}$ converges to a vector $D_{c} x \in H$ with $∥ D_{c} x ∥^{2} = \sum_{n} ∣ b_{n} ∣^{2} \leq C^{2} ∥ x ∥^{2}$ . Thus $D_{c}$ is a well-defined map $H \to H$ satisfying $∥ D_{c} x ∥ \leq C ∥ x ∥$ for every $x$ .

5.1A2A7A8A13step 4.1

Additivity and homogeneity: for $x, y \in H$ and finite $F$ , additivity of the pairing in its first argument [A2] gives $\sum_{n \in F} c_{n} ⟨ x + y, u_{n} ⟩ u_{n} = \sum_{n \in F} c_{n} ⟨ x, u_{n} ⟩ u_{n} + \sum_{n \in F} c_{n} ⟨ y, u_{n} ⟩ u_{n}$ ; the two nets on the right converge to $D_{c} x$ and $D_{c} y$ , so by [A13] the left net converges to $D_{c} x + D_{c} y$ , and uniqueness of limits [A13] together with the defining series of step 4.1 gives $D_{c} (x + y) = D_{c} x + D_{c} y$ . The same computation with $λ x$ in place of $x + y$ gives $D_{c} (λ x) = λ D_{c} x$ , so $D_{c}$ is linear and therefore bounded with $∥ D_{c} ∥ \leq C$ by step 4.1. For a coordinate vector the coefficient family of $u_{m}$ is supported at $m$ with value $c_{m}$ (unique coefficients, [A8]), so its finite-subset net is eventually constant at $c_{m} u_{m}$ and $D_{c} u_{m} = c_{m} u_{m}$ ; in particular $D_{(1)}$ is the identity of $H$ by the Fourier expansion [A7], the constant sequence $1$ being bounded.

6.1A2A6step 4.1step 5.1

Operator identities: fix $x \in H$ and a bounded $c^{'}$ . Applying the coefficient clause of [A6] to the vector $D_{c^{'}} x$ gives $⟨ D_{c^{'}} x, u_{n} ⟩ = c_{n}^{'} ⟨ x, u_{n} ⟩$ for every $n$ , so by step 4.1 the coefficient family of $D_{c^{'}} x$ for the operator $D_{c}$ is $c_{n} c_{n}^{'} ⟨ x, u_{n} ⟩$ and $D_{c} D_{c^{'}} x = \sum_{n} c_{n} c_{n}^{'} ⟨ x, u_{n} ⟩ u_{n} = D_{c c^{'}} x$ . Likewise the finite sums for $D_{c + c^{'}}$ and for $D_{c} + D_{c^{'}}$ have equal terms, since $(c_{n} + c_{n}^{'}) ⟨ x, u_{n} ⟩ = c_{n} ⟨ x, u_{n} ⟩ + c_{n}^{'} ⟨ x, u_{n} ⟩$ , so $D_{c} + D_{c^{'}} = D_{c + c^{'}}$ ; and $D_{λ c} x = λ D_{c} x$ by homogeneity of the coefficients. As $x$ , $c$ and $c^{'}$ were arbitrary, $D_{c} D_{c^{'}} = D_{c c^{'}}$ , $D_{c} + D_{c^{'}} = D_{c + c^{'}}$ and $λ D_{c} = D_{λ c}$ .

7.1A2A4A9step 1.1step 5.1step 6.1algebra

Invertibility criterion: suppose $\inf_{n} ∣ c_{n} ∣ > 0$ . Then no $c_{n}$ vanishes, the reciprocal sequence $c^{- 1} = (c_{n}^{- 1})$ is bounded with $\sup_{n} ∣ c_{n}^{- 1} ∣ = (\inf_{n} ∣ c_{n} ∣)^{- 1}$ , and step 6.1 gives $D_{c^{- 1}} D_{c} = D_{c^{- 1} c} = D_{(1)} = I$ and $D_{c} D_{c^{- 1}} = I$ by step 5.1, so $D_{c}$ is boundedly invertible with inverse $D_{c^{- 1}}$ . Conversely let $S$ be a bounded two-sided inverse of $D_{c}$ . If $∥ S ∥ = 0$ then $S = 0$ and $I = S D_{c} = 0$ , contradicting $u_{0} = I u_{0} \neq 0$ from step 1.1; hence $∥ S ∥ > 0$ , and for every $n$ the operator bound [A9] gives $1 = ∥ u_{n} ∥ = ∥ S D_{c} u_{n} ∥ \leq ∥ S ∥ ∥ c_{n} u_{n} ∥ = ∥ S ∥ ∣ c_{n} ∣$ , so $∣ c_{n} ∣ \geq ∥ S ∥^{- 1} > 0$ for all $n$ and $\inf_{n} ∣ c_{n} ∣ > 0$ .

7.2A2A8A14A15step 4.1step 6.1

Now assume $\sum_{n} ∣ c_{n} ∣ < + \infty$ . Put $c_{n}^{(m)} : = c_{n}$ for $n < m$ and $c_{n}^{(m)} : = 0$ for $n \geq m$ , and $R_{m} : = D_{c^{(m)}}$ , so that $R_{m} x = \sum_{n < m} c_{n} ⟨ x, u_{n} ⟩ u_{n}$ lies in the span of $u_{0}, \dots, u_{m - 1}$ and $R_{m}$ has finite rank and is compact [A8, A14]. By step 6.1 applied to the bounded sequences $c^{(m)}$ and $c - c^{(m)}$ one has $D_{c} - R_{m} = D_{c - c^{(m)}}$ , so step 4.1 bounds $∥ D_{c} - R_{m} ∥ \leq \sup_{n \geq m} ∣ c_{n} ∣ \leq \sum_{n \geq m} ∣ c_{n} ∣$ , and this tail tends to $0$ by the small-tail property [A2] of the summable family $(∣ c_{n} ∣)$ ; therefore $D_{c}$ is a norm limit of compact operators and is compact. Indexing the same finite-rank sums by the positive integers, $R_{m} = \sum_{j = 1}^{m} ⟨ \cdot, u_{j - 1} ⟩ c_{j - 1} u_{j - 1}$ with $\sum_{j \geq 1} ∥ u_{j - 1} ∥ ∥ c_{j - 1} u_{j - 1} ∥ = \sum_{n} ∣ c_{n} ∣ < + \infty$ , so the nuclear-series characterization [A15] makes $D_{c}$ trace class with $∥ D_{c} ∥_{1} \leq \sum_{n} ∣ c_{n} ∣$ .

8.1A2A6A7A8A9A17A19step 5.1step 6.1step 7.2

Eigenvalues and multiplicities: let $b$ be any bounded sequence and let $λ \in C$ . By steps 5.1 and 6.1, $D_{b} - λ I = D_{b - λ}$ and $(D_{b} - λ I)^{k} = D_{(b - λ)^{k}}$ for every $k \geq 1$ . For $x \in H$ the norm identity of [A6] applied to the coefficient family $((b_{n} - λ)^{k} ⟨ x, u_{n} ⟩)_{n}$ gives $∥ (D_{b} - λ I)^{k} x ∥^{2} = \sum_{n} ∣ (b_{n} - λ)^{k} ⟨ x, u_{n} ⟩ ∣^{2}$ , so $(D_{b} - λ I)^{k} x = 0$ exactly when $⟨ x, u_{n} ⟩ = 0$ for every $n$ with $b_{n} \neq λ$ ; by the Fourier expansion [A7] these are exactly the vectors of the closed span of ${u_{n} : b_{n} = λ}$ , and conversely every vector of that closed span is killed by $D_{(b - λ)^{k}}$ , because each such $u_{n}$ is and bounded operators are continuous [A9]. Now take $b = c$ summable and $λ \neq 0$ . The index set ${n : c_{n} = λ}$ is finite: it is contained in ${n : ∣ c_{n} ∣ \geq ∣ λ ∣}$ , and if the latter were infinite the finite subsums of the nonnegative family $(∣ c_{n} ∣)$ would be unbounded, contradicting $\sum_{n} ∣ c_{n} ∣ < + \infty$ [A2]. Hence its closed span is the algebraic span of finitely many orthonormal vectors, of dimension $# {n : c_{n} = λ}$ by [A8] and [A19], and since this kernel is the same for every $k \geq 1$ it is the stabilized kernel of [A17], so $m_{a l g} (λ; D_{c}) = # {n : c_{n} = λ}$ . These are all the nonzero eigenvalues: if $D_{c} x = λ x$ with $x \neq 0$ and $λ \neq 0$ , then some coefficient $⟨ x, u_{n} ⟩$ is nonzero by [A7], and the identity above forces $c_{n} = λ$ .

9.1A2A16A18step 7.2step 8.1

Trace norm and trace: by step 7.2 the operator $D_{c}$ is compact and trace class with $∥ D_{c} ∥_{1} \leq \sum_{n} ∣ c_{n} ∣$ , and step 8.1 identifies its nonzero eigenvalues with algebraic multiplicity, so their moduli are the terms $∣ c_{n} ∣$ over the indices with $c_{n} \neq 0$ . Weyl's inequality [A18] therefore gives $\sum_{n} ∣ c_{n} ∣ = \sum_{j} ∣ λ_{j} ∣ \leq ∥ D_{c} ∥_{1}$ , and with step 7.2 $∥ D_{c} ∥_{1} = \sum_{n} ∣ c_{n} ∣$ . Since $(u_{n})$ is a supplied Hilbert basis of the Hilbert space $H$ by steps 3.1 and 2.2, the trace theorem [A16] identifies $tr (D_{c}) = {tr}_{(u_{n})} (D_{c}) = \sum_{n} ⟨ D_{c} u_{n}, u_{n} ⟩ = \sum_{n} c_{n}$ , the family $(c_{n})$ being absolutely summable by hypothesis.

10.1A1A2A6A7A14A15A16A17A18step 1.1step 2.2step 3.1step 4.1step 7.1step 7.2step 8.1step 9.1∎

Collecting the parts: claim 1 is steps 3.1 and 2.2, claim 2 is steps 4.1–7.1, and claim 3 is steps 7.2–9.1. The zero sequence $c = 0$ gives $D_{0} = 0$ with $∥ D_{0} ∥_{1} = 0 = \sum_{n} ∣ c_{n} ∣$ , $tr (D_{0}) = 0$ and an empty list of nonzero eigenvalues, so the conventions hold there; the finite-support and one-dimensional cases are instances of the general argument, and $H \neq {0}$ because $u_{0} \neq 0$ . AC is consumed only through the declared hypotheses of the cited suppliers: the Countable Choice clause of the summation theorem [A6], of the Fourier expansion [A7] and of the norm-limit clause of [A14], the Countable Choice hypotheses of the nuclear-series characterization [A15] and of the trace theorem [A16], and the AC hypotheses of the algebraic-multiplicity definition [A17] and of Weyl's inequality [A18]; the coordinate family $(u_{n})$ is explicit and the argument selects nothing further. Both directions of the invertibility criterion are proved in step 7.1, and the equality of the trace norm is obtained from the two inequalities of steps 7.2 and 9.1. No interval, endpoint or degenerate parameter occurs in the statement.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30Open item page →

Local separable trace-class determinant construction

Statement

Assume Countable Choice. Let $K$ be a separable complex Hilbert space. For a trace-class operator $T : K \to K$ , define $D_{T} (z) : = \sum_{n \geq 0} z^{n} tr (Λ^{n} T) .$ This series converges locally uniformly on $C$ , defines an entire function, and satisfies $D_{T} (0) = 1$ and $D_{T}^{'} (0) = tr (T)$ . For every bounded finite-rank operator $F : K \to K$ and every finite-dimensional $F$ -invariant subspace $E$ with $ran F \subseteq E$ , $D_{F} (z) = \det_{E} (I_{E} + z (F ∣_{E})) (z \in C) .$ The determinant on the zero-dimensional space is $1$ .

Facts & Assumptions

Given: Countable Choice, a separable complex Hilbert space $K$ , a trace-class operator $T : K \to K$ , a bounded finite-rank operator $F : K \to K$ , and a finite-dimensional $F$ -invariant subspace $E$ containing $ran F$ .

[A1]

The exterior construction defines $Λ^{0} H = C$ and $Λ^{0} S = I_{C}$ , gives the Gram determinant as the wedge inner product, realizes $Λ^{n} H$ as the antisymmetrizing-projection range, and makes the induced operator bounded and functorial with its stated wedge action. In degree one its antisymmetrizer is the identity, so $Λ^{1} S = S$ . (Hilbert exterior powers and induced operators)

[A2]

For trace-class $S$ and $n \geq 1$ , $Λ^{n} S$ is trace class and $∥ Λ^{n} S ∥_{1} \leq ∥ S ∥_{1}^{n} / n!$ ; the degree-zero exterior operator is the identity on $C$ . (Trace-norm bound for exterior powers of trace-class operators)

[A3]

For trace-class $S$ , $∣ tr (S) ∣ \leq ∥ S ∥_{1}$ . (Trace is absolutely convergent and basis independent)

[A4]

The real exponential factorial series $\sum_{n \geq 0} x^{n} / n!$ converges absolutely for every real $x$ . (The exponential series converges absolutely for every real argument)

[A5]

A complex power series converges absolutely and uniformly on every closed subdisc strictly inside its disc of convergence. (A complex power series converges absolutely and uniformly on every closed subdisc strictly inside its disc of convergence)

[A6]

Inside its disc of convergence a complex power series is holomorphic and its derivative is obtained term by term. (Inside its disc of convergence a complex power series is holomorphic and may be differentiated term by term)

[A7]

A function holomorphic on all of $C$ is entire. (Complex differentiability at a point, the complex derivative, holomorphic functions, and entire functions)

[A8]

Every bounded finite-rank operator is compact, and every finite-rank operator is trace class. (Bounded finite rank operators are compact, Trace class operator)

[A9]

A finite-dimensional normed subspace, including the zero subspace, is closed. (A finite-dimensional normed subspace is closed)

[A10]

An invariant subspace $E$ satisfies $F (E) \subseteq E$ and the restriction $F ∣_{E} : E \to E$ is an endomorphism. (Invariant subspaces, restrictions, and induced quotient operators)

[A11]

For a closed subspace $E$ of a Hilbert space, the orthogonal projection $P_{E}$ has $P_{E} x \in E$ and $x - P_{E} x \in E^{⊥}$ ; it is the identity on $E$ and zero on $E^{⊥}$ . (The Hilbert orthogonal projection onto a closed subspace)

[A12]

If $R$ is trace class and $S$ is bounded, cyclicity gives $tr (R S) = tr (S R)$ . (Cyclicity of the trace)

[A13]

Every finite-dimensional inner-product space, including the zero space with its empty basis, has an orthonormal basis. (Every finite-dimensional real or complex inner product space has an orthonormal basis)

[A14]

The trace of an endomorphism of a finite-dimensional vector space is the matrix trace in any ordered basis, and the matrix trace is the sum of its diagonal entries. (The basis-independent trace of an endomorphism of a finite-dimensional vector space, The trace $tr (A)$ as the sum of the diagonal entries)

[A15]

In an ordered basis $B$ , the matrix of an endomorphism has as its $j$ -th column the coordinates of the image of the $j$ -th basis vector. (Coordinate columns $[v]_{B}$ and matrices $[T]_{B}^{C}$ of linear maps relative to ordered bases)

[A16]

In positive dimension, the determinant of a finite-dimensional endomorphism is the determinant of its matrix in an ordered basis; on the zero space it is $1$ . (The determinant of an endomorphism of a finite-dimensional vector space: its matrix determinant in an ordered basis in positive dimension, and $1$ on the zero space)

[A17]

A square matrix determinant is the finite signed permutation sum in the Leibniz formula. (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix)

[A18]

The inner product on a complex Hilbert space is linear in its first argument and conjugate-linear in its second. (Real and complex inner-product spaces and their induced length)

[A19]

A complex Hilbert space is an inner-product space complete in its induced norm. (Hilbert space)

[A20]

A topological space is separable when it has an at most countable dense subset. (Separability: the existence of an at most countable dense subset)

[A21]

Countable Choice is the exact choice assumption declared in the statement. The proof uses its trace-class, trace, cyclicity, and Hilbert-projection suppliers; it selects no basis of the whole space. (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[A22]

The radius of a complex power series is the radius of the real power series formed from the absolute values of its coefficients. (Complex series, absolute convergence, complex power series, and radius of convergence)

[A23]

A bounded linear operator has an operator-norm bound $∥ T x ∥ \leq ∥ T ∥ ∥ x ∥$ . (A bounded linear operator between normed spaces)

[A24]

The Hilbert orthogonal projection is a bounded linear operator and is self-adjoint and idempotent. (Hilbert projections are linear, self-adjoint and contractive)

[A25]

The trace of a trace-class operator is computed by every nuclear representation $S x = \sum_{j} ⟨ x, u_{j} ⟩ v_{j}$ , as $tr (S) = \sum_{j} ⟨ v_{j}, u_{j} ⟩$ . (Trace is absolutely convergent and basis independent)

Source audit: Kostenko's Proposition 3.4.3 gives the exterior-power trace-norm estimate and Corollary 3.4.1 states the entire-function conclusion, but its proof refers to Exercise 3.4.3 for the exterior absolute-value identity. That exercise is not used here; [A2] is the previously proved local exterior-power lemma. Van Neerven's Definition 14.34 gives the same series and factorial bound. Lemma 14.38 proves finite-dimensional reduction only when $T = P T P$ for an orthogonal projection $P$ ; the present argument allows arbitrary invariant $E$ and proves the reduction by exterior projection and trace cyclicity. Dyatlov–Zworski §B.5.2 gives the finite-rank compression determinant by nonzero eigenvalues; it is contextual support, not a substitute for the coefficient calculation below.

Proof

technique · direct

Given: The data in the statement; write $c_{n} : = tr (Λ^{n} T)$ .

1.1A1A2A3A4A20A22

For $n = 0$ , $Λ^{0} T = I_{C}$ , so $c_{0} = 1$ . For $n \geq 1$ , [A2] makes $Λ^{n} T$ trace class and [A3] gives $∣ c_{n} ∣ \leq ∥ Λ^{n} T ∥_{1} \leq ∥ T ∥_{1}^{n} / n!$ . Hence for each real $R \geq 0$ , $\sum_{n \geq 0} ∣ c_{n} ∣ R^{n} \leq \sum_{n \geq 0} \frac{(R ∥ T ∥_{1})^{n}}{n!} < \infty$ by [A4]. Since this holds at every radius, the complex power series has radius $+ \infty$ by [A22]. The separability hypothesis is the dense-subset condition [A20] and is retained, though this estimate uses only trace-class membership.

1.2A1A9A11A13A18A19A24

The finite-dimensional subspace $E$ is closed by [A9], so [A11] supplies its orthogonal projection $P_{E}$ . It is bounded, linear and self-adjoint by [A24]. Its defining decomposition also gives $P_{E}^{2} = P_{E}$ . Choose an orthonormal basis $e_{0}, \dots, e_{d - 1}$ of $E$ by [A13], where $d = \dim E$ and the list is empty if $d = 0$ . For each $n \geq 0$ , put $H_{n} : = Λ^{n} K$ , $G_{n} : = Λ^{n} E \subseteq H_{n}$ , and $Q_{n} : = Λ^{n} P_{E}$ . The increasing wedges $e_{i_{1}} \land \dots \land e_{i_{n}}$ with $i_{1} < \dots < i_{n}$ are orthonormal by the Gram formula [A1]. They span $G_{n}$ : every algebraic tensor in $E^{\otimes n}$ expands in the basis tensors from $(e_{j})$ , and antisymmetrizing sends a repeated-index tensor to zero and every other one to a multiple of an increasing wedge; the algebraic tensors are dense and the projection range is closed. Thus this is a finite orthonormal basis of $G_{n}$ , empty for $n > d$ ; for $n = 0$ , $G_{0} = C$ with basis $1$ . It follows that $G_{n}$ is closed in $H_{n}$ by [A9]. By functoriality in [A1], $Q_{n}^{2} = Q_{n}$ . For $n = 0$ , [A1] gives $Q_{0} = I_{C}$ and $G_{0} = C$ , so $Q_{0}$ is the orthogonal projection onto $G_{0}$ . For $n \geq 1$ , on decomposable wedges the Gram identity and self-adjointness of $P_{E}$ give $⟨ Q_{n} (x_{1} \land \dots \land x_{n}), y_{1} \land \dots \land y_{n} ⟩ = \det [⟨ P_{E} x_{i}, y_{j} ⟩] = \det [⟨ x_{i}, P_{E} y_{j} ⟩] = ⟨ x_{1} \land \dots \land x_{n}, Q_{n} (y_{1} \land \dots \land y_{n}) ⟩ .$ Density of decomposable wedges makes $Q_{n}$ self-adjoint. It maps decomposable wedges into $G_{n}$ and fixes every decomposable wedge in $G_{n}$ ; continuity and density therefore show that its range is exactly $G_{n}$ . Thus $Q_{n}$ is the orthogonal projection onto $G_{n}$ .

2.1A10A14A15A23step 1.2

Let $d : = \dim E$ and use the basis $(e_{j})$ chosen in step 1.2. By [A10], $A : = F ∣_{E}$ is an endomorphism; for $x \in E$ , [A23] gives $∥ A x ∥ = ∥ F x ∥ \leq ∥ F ∥ ∥ x ∥$ , so $A$ is bounded. Write its matrix as $(a_{i j})$ , so $A e_{j} = \sum_{i < d} a_{i j} e_{i}$ by [A15]. For each $0 \leq n \leq d$ , the increasing wedges $e_{I} : = e_{i_{1}} \land \dots \land e_{i_{n}}$ , with $I = (i_{1} < \dots < i_{n})$ , form the orthonormal basis of $G_{n}$ established in step 1.2. Expanding $Λ^{n} A (e_{I}) = A e_{i_{1}} \land \dots \land A e_{i_{n}}$ by multilinearity and antisymmetry shows that its diagonal coefficient at $e_{I}$ is the principal minor $\det A [I, I]$ . Thus [A14] yields $tr (Λ^{n} A) = \sum_{I \subseteq {0, \dots, d - 1}, ∣ I ∣ = n} \det A [I, I],$ with the $n = 0$ term equal to $1$ ; for $n > d$ , $G_{n} = {0}$ and the trace is $0$ . When $d = 0$ this says the sole coefficient is $1$ in degree zero and all positive-degree coefficients vanish.

2.2step 1.1A5A6A7

By [A5], the series converges uniformly on every closed disk of finite radius, and so locally uniformly on $C$ . Its infinite radius from step 1.1 and [A6] make its sum holomorphic on all of $C$ ; therefore $D_{T}$ is entire by [A7].

2.3step 1.1A1A6

The constant coefficient in step 1.1 gives $D_{T} (0) = 1$ . The derivative formula in [A6] gives $D_{T}^{'} (0) = c_{1} = tr (Λ^{1} T) = tr (T)$ by [A1].

3.1A8step 1.1step 2.1step 2.2

Let $F$ be bounded and finite rank. By [A8], it is trace class, so the series defining $D_{F}$ is well-defined and the entire-function conclusion of steps 1.1 and 2.2 applies. Its restriction $A : = F ∣_{E}$ is the bounded endomorphism established in step 2.1.

4.1A1A2A8A12step 1.2step 3.1

Since $ran F \subseteq E$ , the wedge action in [A1] gives $ran (Λ^{n} F) \subseteq G_{n}$ , hence $Q_{n} Λ^{n} F = Λ^{n} F$ . Each $Λ^{n} F$ is trace class by [A2] for $n \geq 1$ ; for $n = 0$ it is the finite-rank identity on $C$ , trace class by [A8]. Cyclicity [A12] therefore gives $tr (Λ^{n} F) = tr ((Λ^{n} F) Q_{n}) .$

5.1A14A18A25step 1.2step 4.1

Let $ι_{n} : G_{n} ↪ H_{n}$ be inclusion and let $A_{n} : = Λ^{n} (F ∣_{E})$ . Use the finite orthonormal basis of $G_{n}$ from step 1.2. Because $Q_{n}$ is its orthogonal projection, $Q_{n} x = \sum_{j} ⟨ x, g_{j} ⟩ g_{j}$ . On $G_{n}$ , functoriality gives $(Λ^{n} F) ι_{n} = ι_{n} A_{n}$ , and therefore $((Λ^{n} F) Q_{n}) x = \sum_{j} ⟨ x, g_{j} ⟩ ι_{n} (A_{n} g_{j}) .$ This is a finite nuclear representation. By [A25] its trace is $tr ((Λ^{n} F) Q_{n}) = \sum_{j} ⟨ ι_{n} (A_{n} g_{j}), g_{j} ⟩ = {tr}_{G_{n}} (A_{n}),$ where the last equality is the finite-dimensional trace formula [A14]. This includes $G_{n} = {0}$ , when both traces are zero. Together with step 4.1, it proves $tr (Λ^{n} F) = tr (Λ^{n} (F ∣_{E}))$ for every $n \geq 0$ .

6.1A16A17step 2.1step 5.1

In the basis $(e_{j})$ , [A16] identifies $\det_{E} (I_{E} + z A)$ with the determinant of the matrix $(δ_{i j} + z a_{i j})$ . Expanding its Leibniz formula [A17] and choosing the $z A$ entry in precisely the columns indexed by a subset $I$ forces the permutation to fix every column outside $I$ ; the remaining signed sum is $z^{∣ I ∣} \det A [I, I]$ . Grouping by $∣ I ∣ = n$ and using step 2.1 gives $\det_{E} (I_{E} + z A) = \sum_{n = 0}^{d} z^{n} tr (Λ^{n} A) .$ By step 5.1, these coefficients equal $tr (Λ^{n} F)$ , and they vanish for $n > d$ . Therefore the right side is exactly the series defining $D_{F} (z)$ , proving the finite-rank identity for every $z \in C$ . If $d = 0$ , step 2.1 makes this identity $1 = 1$ . The proof permits any finite-dimensional invariant $E$ containing $ran F$ ; it never assumes that $E$ reduces $F$ .

7.1A13A21step 1.1step 2.1step 2.3step 6.1∎

The empty exterior degree and $z = 0$ are covered by steps 1.1 and 2.2. If $F = 0$ , then every positive-degree exterior power vanishes and the determinant is $1$ . A zero-dimensional $E$ is handled in step 6.1. When $\dim E = 1$ , step 2.1 gives coefficients $1$ and $tr (F ∣_{E})$ and all higher coefficients vanish, matching the linear determinant; for every $n > d$ , $G_{n} = {0}$ and the trace coefficient vanishes. Countable Choice is the exact declared assumption [A21]; the only bases chosen locally are finite-dimensional orthonormal bases [A13], and no full AC or DC is used.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30Open item page →

Trace-norm continuity, growth and multiplicativity of the local determinant

Statement

Assume the Axiom of Countable Choice. Let $H$ be a separable complex Hilbert space and let $A, B : H \to H$ be trace-class operators. Write $D_{T}$ for the locally constructed determinant of Local separable trace-class determinant construction, and let $(s_{j} (T))_{j \geq 1}$ be the zero-padded singular-value sequence. Then:

For every $z \in C$ , $∣ D_{A} (z) ∣ \leq \prod_{j \geq 1} (1 + ∣ z ∣ s_{j} (A)) \leq e^{∣ z ∣ ∥ A ∥_{1}} .$ Moreover, $D_{A}$ has minimal exponential type: for every $ε > 0$ there is $C_{ε} \geq 0$ such that $∣ D_{A} (z) ∣ \leq C_{ε} e^{ε ∣ z ∣} (z \in C) .$
For every $z \in C$ , $∣ D_{A} (z) - D_{B} (z) ∣ \leq ∣ z ∣ ∥ A - B ∥_{1} e^{1 + ∣ z ∣ ∥ A ∥_{1} + ∣ z ∣ ∥ B ∥_{1}} .$
$A + B + A B$ is trace class and $D_{A + B + A B} (1) = D_{A} (1) D_{B} (1) .$
If $(F_{m})_{m \geq 1}$ is any sequence of finite-rank operators with $∥ F_{m} - A ∥_{1} \to 0$ , then the ordinary determinants $\det_{ran F_{m}} (I_{ran F_{m}} + z F_{m} ∣_{ran F_{m}})$ converge locally uniformly to $D_{A} (z)$ . Their limit is independent of the approximating sequence.

Facts & Assumptions

Given: Countable Choice, a separable complex Hilbert space $H$ , trace-class $A, B$ , and, when claim 4 is considered, a trace-norm convergent finite-rank sequence $(F_{m})$ .

[A1]

For trace-class $T$ , the induced exterior powers are trace class and $∥ Λ^{n} T ∥_{1} = \sum_{j_{1} < \dots < j_{n}} s_{j_{1}} (T) \dots s_{j_{n}} (T) \leq \frac{∥ T ∥_{1}^{n}}{n!}$ for $n \geq 1$ ; $Λ^{0} T = I_{C}$ and its trace is $1$ (Trace-norm bound for exterior powers of trace-class operators).

[A2]

The trace is linear on trace-class operators and satisfies $∣ tr S ∣ \leq ∥ S ∥_{1}$ (Trace is absolutely convergent and basis independent).

[A3]

Trace class means $\sum_{j \geq 1} s_{j} (T) < \infty$ and $∥ T ∥_{1} = \sum_{j \geq 1} s_{j} (T)$ ; its singular-value sequence is zero padded (Trace class operator).

[A4]

For a nonnegative sequence $(p_{j})$ , $\prod_{j} (1 + p_{j})$ converges exactly when $\sum_{j} p_{j}$ converges (For $p_{k} \geq 0$ the product $\prod (1 + p_{k})$ converges iff $\sum p_{k}$ converges, with $1 + \sum_{k < n} p_{k} \leq \prod_{k < n} (1 + p_{k}) \leq 1 / (1 - \sum_{k < n} p_{k})$ when $\sum_{k < n} p_{k} < 1$ ; for $0 \leq p_{k} < 1$ the product $\prod (1 - p_{k})$ converges iff $\sum p_{k}$ converges and its partial products tend to $0$ otherwise; and $\sum ∣ p_{k} ∣$ convergent implies $\prod (1 + p_{k})$ convergent, Infinite products: partial products, and convergence to a nonzero limit after finitely many vanishing factors). Nonnegative sums are determined by suprema of their finite subsums (Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ ), and limits preserve non-strict inequalities (Limits preserve non-strict inequalities).

[A5]

For every real $x$ , $1 + x \leq e^{x}$ ( $1 + x \leq \exp (x)$ for every real $x$ , hence $(1 - p)^{m} \leq \exp (- m p)$ ); the real exponential is increasing and satisfies $e^{u + v} = e^{u} e^{v}$ (The exponential function is strictly increasing, The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ ); and $\sum_{n \geq 0} x^{n} / n!$ converges for every real $x$ (The exponential series converges absolutely for every real argument).

[A6]

The exterior construction realizes $Λ^{n} H$ as the antisymmetric tensor subspace and gives its wedge action; the local determinant is $D_{T} (z) = \sum_{n \geq 0} z^{n} tr (Λ^{n} T)$ , entire, with $D_{T} (0) = 1$ , and for finite-rank $F$ it satisfies $D_{F} (z) = \det_{E} (I_{E} + z F ∣_{E})$ for every finite-dimensional invariant $E \supseteq ran F$ (Hilbert exterior powers and induced operators, Local separable trace-class determinant construction).

[A7]

Trace-class operators form a linear space, their trace norm is a norm, $∥ T ∥ \leq ∥ T ∥_{1}$ , and $∥ S T U ∥_{1} \leq ∥ S ∥ ∥ T ∥_{1} ∥ U ∥$ for bounded $S, U$ (Trace class is a two sided Banach operator ideal).

[A8]

Every supplied sequence of finite-rank orthogonal projections $P_{n} \to I$ strongly on separable $H$ satisfies $∥ P_{n} T P_{n} - T ∥_{1} \to 0$ for trace-class $T$ ; the initial projections of a supplied countable orthonormal basis are an example (Finite-rank orthogonal compressions converge in trace norm).

[A9]

A separable space has an at-most-countable dense subset (Separability: the existence of an at most countable dense subset, Finite, countably infinite, countable, uncountable). If that subset is nonempty and finite, choose a finite listing and repeat its first member periodically; if it is countably infinite, choose a bijection from $N$ . In either case it has a surjective sequence, with no choice beyond fixing the one listing whose existence is asserted by countability. A dense sequence in a Hilbert space yields a finite or countable orthonormal basis by the specified Gram–Schmidt construction (A Hilbert space with a dense sequence has a finite or countable orthonormal basis).

[A10]

Finite-dimensional subspaces are closed; for a closed subspace its Hilbert orthogonal projection is defined by the orthogonal decomposition (A finite-dimensional normed subspace is closed, The Hilbert orthogonal projection onto a closed subspace). The Fourier sums of a supplied orthonormal basis converge in norm to each vector (Fourier expansion in a Hilbert space).

[A11]

The determinant of a composition of endomorphisms of one finite-dimensional vector space is the product of their determinants, including dimension zero (For endomorphisms $S$ and $T$ of one finite-dimensional vector space, $\det (S T) = \det (S) \det (T)$ ).

[A12]

If a function is holomorphic on a disc of radius $S$ , is bounded by $M$ on the concentric circle of radius $R < S$ , then on the centre its derivative is bounded by $M / R$ (Cauchy estimates on a smaller concentric disc).

[A13]

A holomorphic function on an open subset of $C$ is smooth as a map of two real coordinates, with real derivative given by its complex derivative (Holomorphic functions are real analytic and smooth in their two real coordinates). A differentiable map $[a, b] \to R^{2}$ whose derivative norm is at most $M$ satisfies $∥ f (b) - f (a) ∥_{2} \leq M (b - a)$ (The mean value inequality: if $f : [a, b] \to R^{m}$ is continuous and differentiable on $(a, b)$ with $∥ f^{'} ∥_{2} \leq M$ , then $∥ f (b) - f (a) ∥_{2} \leq M (b - a)$ ).

[A14]

A complex polynomial is entire (Complex polynomials are entire with the power-rule derivative, and rational functions are holomorphic wherever their denominator is nonzero). If complex-valued functions are bounded by a summable nonnegative majorant, their series converges uniformly (Weierstrass M-test for complex-valued function series); a locally uniformly convergent series of holomorphic functions is holomorphic (A locally uniformly convergent series of holomorphic functions may be differentiated term by term).

[A15]

A polynomial of degree at most $n$ is determined by its values at any $n + 1$ distinct complex numbers; the root bound for polynomials over an integral domain proves uniqueness, and the Lagrange formula then expresses each coefficient as a finite linear combination of those values (A nonzero polynomial of degree $n$ over an integral domain has at most $n$ distinct roots).

[A16]

Countable Choice is the exact declared choice assumption (The Axiom of Countable Choice ( ${A C}_{ω}$ )). It is used through the AC $_{ω}$ -qualified singular-value definition and exterior trace, trace, ideal, and compression and projection/Fourier suppliers [A1], [A2], [A3], [A7], [A8], and [A10]; the trace-class definition records the concrete countable selections of finite orthonormal bases in singular eigenspaces. The separable-space basis used below is constructed from one dense sequence by the stated Gram–Schmidt process, and the padded enumeration requires no choice by [A9].

Source audit: Kostenko, Trace Ideals with Applications, §3.4.3, Corollary 3.4.1, Theorem 3.4.4 and Corollary 3.4.2 (printed pp. 38–40; PDF pp. 47–49) gives the exterior-product growth, minimal-type, Cauchy continuity and multiplicativity route. The local proof below derives the affine-parameter entire function from its exterior-trace series rather than leaving that dependence implicit. Van Neerven, Functional Analysis, §14.5.a, Lemmas 14.35–14.39 (printed pp. 585–587; PDF pp. 597–599) gives the same bounds and product law; its Lemma 14.37 uses tensor-product trace-norm telescoping, and Lemma 14.38 assumes $T = P T P$ , so neither argument is substituted for the local proof. Dyatlov–Zworski, Appendix B §§B.5.2–B.5.3, Propositions B.27 and B.29 (PDF pp. 509–511) records the continuous finite-rank extension and determinant estimates; that extension construction is contextual only. No source uncertainty remains for this item.

Proof

1.1A1A2A3A4A5A6

Put $c_{n} (T) : = tr (Λ^{n} T)$ and $e_{n} (T, r) : = \sum_{j_{1} < \dots < j_{n}} s_{j_{1}} (T) \dots s_{j_{n}} (T) r^{n}$ for $n \geq 1$ , with $e_{0} (T, r) = 1$ . By [A1] and [A2], $∣ c_{n} (T) ∣ r^{n} \leq e_{n} (T, r)$ for $n \geq 1$ , while $c_{0} (T) = 1$ . For each finite $N$ , distributive expansion gives $\prod_{j = 1}^{N} (1 + r s_{j} (T)) = \sum_{n = 0}^{N} \sum_{1 \leq j_{1} < \dots < j_{n} \leq N} r^{n} s_{j_{1}} (T) \dots s_{j_{n}} (T) .$ All terms are nonnegative; increasing $N$ exhausts the finite subsets of the singular-value index set, so [A4] identifies the limit of these products with $\sum_{n \geq 0} e_{n} (T, r)$ . Since [A3] gives $\sum_{j} s_{j} (T) = ∥ T ∥_{1}$ , [A4] ensures the product exists. This proves $∣ D_{T} (z) ∣ \leq \sum_{n \geq 0} ∣ c_{n} (T) ∣ r^{n} \leq \prod_{j \geq 1} (1 + r s_{j} (T)), r = ∣ z ∣ .$ For finite $N$ , [A5] and the exponential addition law give $\prod_{j = 1}^{N} (1 + r s_{j} (T)) \leq e^{r \sum_{j = 1}^{N} s_{j} (T)} \leq e^{r ∥ T ∥_{1}} .$ Passing to the product limit and using order preservation proves the second bound.

1.2A1A2A6A7A14A15

Suppose $z \neq 0$ and $A \neq B$ . Since the trace norm is a norm by [A7], $∥ A - B ∥_{1} > 0$ . Put $C = (A + B) / 2$ , $G = A - B$ , and $F (t) = D_{C + t G} (z)$ for $t \in C$ . Trace class is a linear space by [A7], so $C + t G$ is trace class. For each $n$ , the tensor-power definition in [A6] shows that $t \mapsto Λ^{n} (C + t G)$ is an operator-valued polynomial of degree at most $n$ : expand $(C + t G)^{\otimes n}$ by the tensor factors. For each power $t^{k}$ , its coefficient is the sum over all $k$ -element subsets of factors in which $G$ is used, with $C$ in the other factors. This sum commutes with every permutation of tensor slots and hence preserves the antisymmetric subspace, so its restriction is a bounded coefficient operator on $Λ^{n} H$ . Write the bounded coefficient operators as $Q_{k}$ , and choose distinct $t_{0}, \dots, t_{n} \in C$ . Define $L_{j} (t) : = \prod_{k \neq j} (t - t_{k}) / (t_{j} - t_{k})$ . For every $m = 0, \dots, n$ , the scalar polynomials $t^{m}$ and $\sum_{j = 0}^{n} t_{j}^{m} L_{j} (t)$ agree at all $t_{k}$ ; their difference has degree at most $n$ and $n + 1$ roots, so [A15] makes the difference zero. Multiplying these identities by $Q_{m}$ and summing gives $Λ^{n} (C + t G) = \sum_{j = 0}^{n} Λ^{n} (C + t_{j} G) L_{j} (t)$ . Expanding the $L_{j}$ shows each coefficient operator is a finite linear combination of the values $Λ^{n} (C + t_{j} G)$ . Those values are trace class by [A1], so all coefficient operators are trace class by [A7]. Hence $p_{n} (t) : = tr (Λ^{n} (C + t G))$ is a scalar polynomial. For $∣ t ∣ \leq M$ , [A1], [A2], and [A7] give $∣ z ∣^{n} ∣ p_{n} (t) ∣ \leq \frac{(∣ z ∣ (∥ C ∥_{1} + M ∥ G ∥_{1}))^{n}}{n!} .$ The majorant series converges by the exponential-series supplier [A5]. Each $z^{n} p_{n} (t)$ is holomorphic by [A14]; the Weierstrass M-test and holomorphic-series theorem [A14] therefore show that $F (t) = \sum_{n \geq 0} z^{n} p_{n} (t)$ is entire in $t$ .

2.1A3A5step 1.1

Fix $ε > 0$ . Choose $N \geq 0$ so that $\sum_{j > N} s_{j} (T) < ε / 2$ , possible by [A3]. The tail product is at most $e^{r \sum_{j > N} s_{j} (T)} \leq e^{ε r / 2}$ because every finite tail product is bounded by the exponential of the corresponding partial tail sum using [A5]; taking its product limit preserves the inequality by [A4]. If $N = 0$ , this already gives $∣ D_{T} (z) ∣ \leq e^{ε r}$ with $C_{ε} : = 1$ . If $N \geq 1$ , then for $j \leq N$ and $r \geq 0$ , $1 + r s_{j} (T) \leq (1 + \frac{2 N s_{j} (T)}{ε}) (1 + \frac{ε r}{2 N}) \leq (1 + \frac{2 N s_{j} (T)}{ε}) e^{ε r / (2 N)}$ by [A5]. Multiplying the first $N$ bounds and the tail estimate, and using step 1.1, gives $∣ D_{T} (z) ∣ \leq C_{ε} e^{ε r}, C_{ε} : = \prod_{j = 1}^{N} (1 + \frac{2 N s_{j} (T)}{ε}) .$ This is minimal exponential type, including finite-rank and zero operators.

2.2A6A7A12A13step 1.1step 1.2

Set $δ = ∣ z ∣ ∥ A - B ∥_{1} > 0$ and $R = 1 / δ$ . For $t \in [- 1 / 2, 1 / 2]$ and $∣ w - t ∣ = R$ , one has $∣ w ∣ \leq R + 1 / 2$ . By step 1.1 and [A7], $∣ F (w) ∣ \leq e^{∣ z ∣ ∥ C + w G ∥_{1}} \leq e^{∣ z ∣ ∥ C ∥_{1} + ∣ z ∣ (R + 1 / 2) ∥ G ∥_{1}} \leq e^{1 + ∣ z ∣ ∥ A ∥_{1} + ∣ z ∣ ∥ B ∥_{1}} .$ For the last inequality, the triangle inequality gives $∥ C ∥_{1} \leq (∥ A ∥_{1} + ∥ B ∥_{1}) / 2$ and $δ = ∣ z ∣ ∥ A - B ∥_{1} \leq ∣ z ∣ (∥ A ∥_{1} + ∥ B ∥_{1})$ ; also $∣ z ∣ R ∥ G ∥_{1} = 1$ and $∣ z ∣ ∥ G ∥_{1} / 2 = δ / 2$ . Apply [A12] to the radius- $R$ circle about $t$ to get $∣ F^{'} (t) ∣ \leq R^{- 1} e^{1 + ∣ z ∣ ∥ A ∥_{1} + ∣ z ∣ ∥ B ∥_{1}} = δ e^{1 + ∣ z ∣ ∥ A ∥_{1} + ∣ z ∣ ∥ B ∥_{1}}$ . By [A13] the coordinate map of $F$ on $[- 1 / 2, 1 / 2]$ is differentiable with real derivative norm $∣ F^{'} (t) ∣$ . The mean-value inequality in [A13] yields $∣ D_{A} (z) - D_{B} (z) ∣ = ∣ F (1 / 2) - F (- 1 / 2) ∣ \leq δ e^{1 + ∣ z ∣ ∥ A ∥_{1} + ∣ z ∣ ∥ B ∥_{1}},$ since $C + G / 2 = A$ and $C - G / 2 = B$ . If $z = 0$ , both determinants equal $1$ by [A6]; if $A = B$ , their difference is zero. This proves the continuity bound in all cases.

3.1A6A7step 2.2

Let $F_{m}$ be finite rank and $∥ F_{m} - A ∥_{1} \to 0$ . With $E_{m} = ran F_{m}$ , the range is finite dimensional and invariant because $F_{m} (H) \subseteq E_{m}$ ; [A6] identifies the ordinary determinant on $E_{m}$ with $D_{F_{m}} (z)$ . The same identity holds for every other permitted $E_{m}$ , so the finite-dimensional determinant value is independent of that choice. For any compact $K \subset C$ , choose $R_{K}$ with $∣ z ∣ \leq R_{K}$ on $K$ . The trace norms $∥ F_{m} ∥_{1}$ are bounded by [A7] and convergence, so step 2.2 gives $\sup_{z \in K} ∣ D_{F_{m}} (z) - D_{A} (z) ∣ \leq R_{K} ∥ F_{m} - A ∥_{1} e^{1 + R_{K} (∥ F_{m} ∥_{1} + ∥ A ∥_{1})} ⟶ 0.$ The limit is $D_{A}$ for every such sequence, hence does not depend on the approximation.

3.2A6A7A8A9A10A11step 2.2algebra

If $H = {0}$ , all determinants in claim 3 are $1$ . Otherwise choose an at-most-countable dense subset of $H$ using [A9]; it is nonempty, so [A9] provides a dense sequence. The Gram–Schmidt supplier in [A9] gives an orthonormal basis that is finite or countably infinite. In the finite case set $P_{n} = I_{H}$ , which is finite rank and converges strongly to $I_{H}$ . In the countably infinite case let $P_{n}$ be the orthogonal projection, defined by [A10], onto the span of the first $n$ basis vectors; that span is closed by [A10], and the Fourier expansion in [A10] gives $P_{n} x \to x$ . Thus in either case $(P_{n})$ is a supplied sequence of finite-rank orthogonal projections converging strongly to $I_{H}$ . Put $A_{n} = P_{n} A P_{n}$ and $B_{n} = P_{n} B P_{n}$ . By [A8], $A_{n} \to A$ and $B_{n} \to B$ in trace norm. Also, $A B$ is trace class by the ideal property in [A7], so $C : = A + B + A B$ is trace class by linearity. The ideal estimate [A7] gives $∥ A_{n} B_{n} - A B ∥_{1} \leq ∥ A_{n} - A ∥_{1} ∥ B_{n} ∥ + ∥ A ∥ ∥ B_{n} - B ∥_{1} ⟶ 0,$ where $∥ B_{n} ∥$ is bounded because $∥ B_{n} ∥ \leq ∥ B_{n} ∥_{1}$ and $∥ B_{n} ∥_{1} \leq ∥ B ∥_{1} + ∥ B_{n} - B ∥_{1}$ . Hence $C_{n} : = A_{n} + B_{n} + A_{n} B_{n} \to C : = A + B + A B$ in trace norm. All three compressed operators have range in the finite-dimensional space $P_{n} H$ , which they leave invariant. By [A6] and [A11], $D_{C_{n}} (1) = \det_{P_{n} H} (I + C_{n} ∣_{P_{n} H}) = \det_{P_{n} H} ((I + A_{n} ∣_{P_{n} H}) (I + B_{n} ∣_{P_{n} H})) = D_{A_{n}} (1) D_{B_{n}} (1) .$ Applying step 2.2 at $z = 1$ to $A_{n} \to A$ , $B_{n} \to B$ , and $C_{n} \to C$ and passing to the limit proves $D_{A + B + A B} (1) = D_{A} (1) D_{B} (1)$ .

4.1

If $A = 0$ , then $D_{A} = 1$ and its singular-value product is empty or all factors are $1$ ; if $z = 0$ , $D_{A} (0) = 1$ . When $H = C$ and $A = a I$ , $D_{A} (z) = 1 + z a$ , so the product and exponential bounds reduce to $∣ 1 + z a ∣ \leq 1 + ∣ z ∣ ∣ a ∣ \leq e^{∣ z ∣ ∣ a ∣}$ , the scalar determinant difference is $∣ z ∣ ∣ a - b ∣$ , which is at most the stated continuity bound by [A5], and multiplicativity is $1 + (a + b + a b) = (1 + a) (1 + b)$ . For finite-rank $A$ , the product has only finitely many nontrivial factors and the tail in step 2.1 is zero after its rank. The Cauchy argument includes both segment endpoints $t = \pm 1 / 2$ ; the special branches $z = 0$ and $A = B$ avoid a zero Cauchy radius denominator. Countable Choice is the exact declared assumption [A16], used through the named trace-class, trace, ideal, compression, and projection/Fourier suppliers; the orthonormal basis used for compressions is built from one dense sequence by Gram–Schmidt. No equivalence is asserted, so both iff directions are inapplicable. [A1, A3, A5, A6, A7, A8, A9, A10, A11, A12, A13, A16, step 1.1, step 2.1, step 2.2, step 3.2] \qed

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30Open item page →

Logarithmic derivative of the local Fredholm determinant

Statement

Assume the Axiom of Countable Choice. Let $H$ be a separable complex Hilbert space and let $T : H \to H$ be trace class. Write $D_{T}$ for the locally constructed determinant of Local separable trace-class determinant construction. For each $z \in C$ for which $I + z T$ has a bounded inverse $R_{z} \in B (H)$ , $D_{T}^{'} (z) = D_{T} (z) tr (T R_{z}) .$ Equivalently, $R_{z} = (I + z T)^{- 1}$ in the displayed formula.

Facts & Assumptions

Given: Countable Choice, a separable complex Hilbert space $H$ , a trace-class operator $T : H \to H$ , and, at the point $z$ under consideration, a bounded two-sided inverse $R_{z}$ of $I + z T$ .

[A1]

Countable Choice, written ${A C}_{ω}$ , is the declared choice assumption (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[A2]

For a trace-class operator $U$ on a separable complex Hilbert space, the local determinant is $D_{U} (w) = \sum_{n \geq 0} w^{n} tr (Λ^{n} U),$ is entire, and satisfies $D_{U} (0) = 1$ and $D_{U}^{'} (0) = tr (U)$ (Local separable trace-class determinant construction).

[A3]

Trace-class operators form a linear space; if $U$ is trace class and $V$ is a bounded operator, then $U V$ and $V U$ are trace class (Trace class operator, Trace class is a two sided Banach operator ideal).

[A4]

For $n \geq 1$ , the tensor definition of exterior powers gives $Λ^{n} (c U) = c^{n} Λ^{n} U$ for $c \in C$ , while $Λ^{0} (c U) = I_{C}$ (Hilbert exterior powers and induced operators).

[A5]

For trace-class $A, B$ on the same separable complex Hilbert space, $D_{A + B + A B} (1) = D_{A} (1) D_{B} (1)$ (Trace-norm continuity, growth and multiplicativity of the local determinant).

[A6]

Membership $R_{z} \in B (H)$ means that $R_{z}$ is a bounded linear operator, as required in the trace-class ideal estimate (A bounded linear operator between normed spaces).

Source audit: Dyatlov–Zworski, Mathematical Theory of Scattering Resonances, Appendix B §B.5.2, Lemma B.26 (PDF p. 509) proves the finite-rank formula for a $C^{1}$ path $A_{t}$ whose ranges lie in one fixed finite-dimensional subspace, assuming $I - A_{t}$ remains invertible along the path. Its proof reduces to Jacobi's finite-dimensional determinant formula. The local proof below does not extend that finite-rank statement by assertion: it derives the trace-class identity from the already proved determinant multiplicativity and the derivative at zero. Van Neerven, Functional Analysis, §14.5.a, Definition 14.34 (printed p. 585; PDF p. 597) gives the entire exterior-trace series and its first-order expansion, and Lemma 14.39 (printed p. 587; PDF p. 599) gives multiplicativity. Kostenko, Trace Ideals with Applications, §3.4.3, Corollary 3.4.2 (printed p. 40; PDF p. 49) also gives the product identity. Those passages were read in full; none states the general infinite-dimensional logarithmic-derivative formula as used here. They inform the audit, while the argument below proves the claim locally. No source uncertainty remains.

Proof

technique · direct

1.1A3A6algebra

Fix such a $z$ , write $R = R_{z}$ , put $M : = I + z T$ , and set $S : = T R$ . Since $M T = T M$ and $R M = M R = I$ , the equality $R (M T) R = R (T M) R$ gives $T R = R T$ , hence $M S = M T R = T M R = T$ . The operator $S$ is trace class by [A3], because $T$ is trace class and $R$ is bounded; therefore the scalar multiples $z T$ and $h S$ are trace class for every $h \in C$ .

1.2A2A4

For every trace-class $U$ and $c \in C$ , [A2] and [A4] give $D_{c U} (1) = \sum_{n \geq 0} tr (Λ^{n} (c U)) = D_{U} (c)$ : the degree-zero term is $1$ on both sides and for $n \geq 1$ the degree- $n$ term is $c^{n} tr (Λ^{n} U)$ , including when $c = 0$ .

2.1step 1.1algebra

For each $h \in C$ , step 1.1 gives $(I + z T) S = T$ , so $I + (z + h) T = (I + z T) (I + h S),$ because the coefficient of $h$ on the right is $S + z T S = (I + z T) S = T$ .

3.1A5step 1.2step 2.1

Apply [A5] to trace-class $z T$ and $h S$ ; by step 2.1, $(z + h) T = z T + h S + z h T S$ , so $D_{(z + h) T} (1) = D_{z T} (1) D_{h S} (1)$ and step 1.2 turns this into $D_{T} (z + h) = D_{T} (z) D_{S} (h) .$

4.1A2step 1.1step 3.1

Subtract $D_{T} (z)$ from step 3.1 and divide by $h \neq 0$ ; as $h \to 0$ , [A2] gives $D_{T}^{'} (z) = D_{T} (z) D_{S}^{'} (0) = D_{T} (z) tr (S)$ , and $S = T R = T (I + z T)^{- 1}$ gives the claimed formula. Taking $h = - z$ in step 3.1 and using $D_{T} (0) = 1$ from [A2] gives $1 = D_{T} (z) D_{S} (- z)$ , so $D_{T} (z) \neq 0$ and the identity is its ordinary logarithmic-derivative formula as well.

5.1

If $T = 0$ , then $S = 0$ , $D_{T} \equiv 1$ , and both sides are zero; this also covers $H = {0}$ . On $H = C$ with $T = t I$ and $1 + z t \neq 0$ , $D_{T} (z) = 1 + z t$ and $R = (1 + z t)^{- 1} I$ , so both sides equal $t$ . At $z = 0$ , $R = I$ and step 4.1 gives $D_{T}^{'} (0) = tr (T)$ . The complex derivative exists on the whole plane by [A2], and the difference quotient uses complex $h$ , so there is no one-sided endpoint case. Countable Choice is exactly [A1], inherited through the trace-class, determinant, ideal, and multiplicativity suppliers; this proof makes no additional choices. The claim is not an equivalence, so both iff directions are inapplicable. [A1, A2, A3, A5, A6, step 1.1, step 3.1, step 4.1] \qed

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30Open item page →

Zeros of the local Fredholm determinant

Statement

Assume the Axiom of Choice. Let $H$ be a separable complex Hilbert space and let $T : H \to H$ be trace class. For every $z \in C$ , $D_{T} (z) = 0 ⟺ I + z T is not boundedly invertible,$ where $D_{T}$ is the locally constructed determinant. For every nonzero eigenvalue $λ$ of $T$ (equivalently, every nonzero spectral value), the zero at $z_{0} = - 1 / λ$ has order $m_{a l g} (λ; T) .$

Facts & Assumptions

Given: AC; a separable complex Hilbert space $H$ ; a trace-class operator $T : H \to H$ ; and, for the multiplicity claim, a nonzero eigenvalue $λ$ of $T$ .

[A1]

AC selects from every family of nonempty sets (The Axiom of Choice).

[A2]

A complex Hilbert space is a Banach space in its induced norm (Hilbert space).

[A3]

In the trace-class definition, $T \in B (H, K)$ is assumed compact (Trace class operator).

[A4]

For a compact operator, every nonzero spectral value is an eigenvalue with finite-dimensional generalized eigenspace (Riesz schauder spectrum of a compact operator).

[A5]

For every $ε > 0$ , a compact operator has only finitely many spectral values with modulus at least $ε$ (Riesz schauder spectrum of a compact operator).

[A6]

A Riesz projection $P_{E}$ is defined for a clopen spectral subset $E \subseteq σ (T)$ (Riesz spectral projection).

[A7]

A Riesz projection satisfies $P^{2} = P$ , commutes with $T$ , and gives the closed invariant splitting $H = ran P \oplus \ker P$ (Riesz spectral projection properties).

[A8]

When the summands are nonzero, the restriction spectra are $E$ on $ran P$ and $σ (T) ∖ E$ on $\ker P$ (Riesz spectral projection properties).

[A9]

For nonzero $λ \in σ (T)$ , the algebraic multiplicity is the finite dimension of $G_{λ} (T) = \ker (T - λ I)^{m_{0}}$ for a stabilized exponent, and $G_{λ} (T) = ran P_{λ}$ (Algebraic multiplicity of a nonzero compact-operator eigenvalue).

[A10]

The local determinant is the entire exterior-trace series $D_{U} (w) = \sum_{n \geq 0} w^{n} tr (Λ^{n} U),$ with $D_{U} (0) = 1$ (Local separable trace-class determinant construction).

[A11]

For bounded finite-rank $F$ and finite-dimensional invariant $E$ with $ran F \subseteq E$ , $D_{F} (w) = \det_{E} (I_{E} + w (F ∣_{E}));$ the determinant on the zero space is $1$ (Local separable trace-class determinant construction).

[A12]

Trace-class operators form a linear space and remain trace class under left or right multiplication by bounded operators (Trace class is a two sided Banach operator ideal).

[A13]

For trace-class $A, B$ on the same separable Hilbert space, $D_{A + B + A B} (1) = D_{A} (1) D_{B} (1)$ (Trace-norm continuity, growth and multiplicativity of the local determinant).

[A14]

The exterior action is given on wedges by $(Λ^{n} U) (x_{1} \land \dots \land x_{n}) = U x_{1} \land \dots \land U x_{n}$ , and $Λ^{0} U = I_{C}$ ; hence $Λ^{n} (c U) = c^{n} Λ^{n} U$ for $n \geq 1$ (Hilbert exterior powers and induced operators).

[A15]

AC implies DC and hence Countable Choice (AC implies DC implies countable choice); this supplies the choice assumptions of [A10]–[A13].

[A16]

Every finite-dimensional nilpotent endomorphism has an ordered basis concatenating Jordan strings (Every finite-dimensional nilpotent endomorphism has a basis of Jordan strings).

[A17]

A finite-dimensional operator determinant is its matrix determinant in an ordered basis (The determinant of an endomorphism of a finite-dimensional vector space: its matrix determinant in an ordered basis in positive dimension, and $1$ on the zero space).

[A18]

That determinant is independent of the ordered basis (The determinant of a linear operator is independent of the chosen ordered basis).

[A19]

The determinant of an upper or lower triangular matrix is the product of its diagonal entries (The determinant of a triangular matrix is the product of its diagonal entries).

[A20]

A holomorphic function has a zero of order $d < \infty$ at $a$ exactly when it factors locally as $(z - a)^{d} g (z)$ with $g (a) \neq 0$ (The order of a zero is the exponent in its local holomorphic factorization).

Source audit: Kostenko, Trace Ideals with Applications, §3.4.4, Theorem 3.4.6 (printed pp. 40–41; PDF pp. 49–50), proves the same criterion and multiplicity claim. Its proof uses determinant multiplicativity for the invertible case, then a commuting Riesz projection, its finite-dimensional factor, and nonvanishing of the complementary determinant. I read that complete argument. The local proof below reconstructs those steps from the local determinant series, the proved local multiplicativity, and the library's Riesz-projection and algebraic-multiplicity suppliers; the cited theorem is not a proof premise. The projection is generally nonorthogonal, so the proof uses its bounded topological direct sum and does not use an orthogonal compression. No source uncertainty remains.

Proof

technique · direct

1.1A11

If $T = 0$ , including when $H = {0}$ , choose $F = T$ and $E = {0}$ in [A11]. Then $D_{T} \equiv 1$ and $I + z T = I$ has its identity as bounded inverse for every $z$ ; there is no nonzero eigenvalue to consider. Hence assume $H \neq {0}$ and $T \neq 0$ .

1.2A1A2A3A5A6

For the multiplicity claim, let $λ \neq 0$ be an eigenvalue of $T$ . By [A2] and [A3], $H$ is a complex Banach space and $T$ is compact, so the Riesz–Schauder suppliers apply. The value $λ$ lies in $σ (T)$ . By [A5], $S = {μ \in σ (T) : ∣ μ ∣ \geq ∣ λ ∣ / 2}$ is finite; every spectral point within distance $∣ λ ∣ / 2$ of $λ$ lies in $S$ . If $S ∖ {λ}$ is empty, take $δ = ∣ λ ∣ / 4$ ; otherwise take $δ$ positive and less than both $∣ λ ∣ / 2$ and the finitely many distances $∣ λ - μ ∣$ for $μ \in S ∖ {λ}$ . Then $δ$ isolates $λ$ , so $E = {λ}$ is clopen in $σ (T)$ and [A1, A6] define its Riesz projection $P$ .

1.3A10A14

For every trace-class $U$ and $c \in C$ , [A10] and [A14] give $D_{c U} (1) = \sum_{n \geq 0} tr (Λ^{n} (c U)) = D_{U} (c),$ because the degree-zero term is $1$ on both sides and the degree- $n$ terms agree for each $n \geq 1$ ; this includes $c = 0$ .

2.1A11A12A13step 1.3algebra

Let $U$ be trace class and suppose $I + w U$ has bounded inverse $R$ . Set $V : = - w U R$ , which is trace class by [A12]. The right-inverse equation $(I + w U) R = I$ gives $w U + V + w U V = w U - w U R - w^{2} U^{2} R = w U - w U (I + w U) R = 0$ . Apply [A13] to $w U, V$ and use $D_{0} (1) = 1$ from [A11] to get $1 = D_{w U} (1) D_{V} (1) = D_{U} (w) D_{V} (1)$ by step 1.3. Thus $D_{U} (w) \neq 0$ .

2.2A7A9A12step 1.2

Put $M = ran P$ and $N = \ker P$ . By [A7], $H = M \oplus N$ is a bounded topological direct sum and both summands are $T$ -invariant. By [A9], $M = G_{λ} (T)$ and $d : = \dim M = m_{a l g} (λ; T) < \infty$ ; since $λ$ is an eigenvalue, $d \geq 1$ . The restriction $J : = (T ∣_{M}) - λ I_{M}$ is nilpotent because $M = \ker (T - λ I)^{m_{0}}$ for a stabilized exponent. Both $T P$ and $T (I - P)$ are trace class by [A12].

3.1A13step 1.3step 2.2algebra

Set $A = z T P$ and $B = z T (I - P)$ . Since $P T = T P$ , $A B = z^{2} T P T (I - P) = z^{2} T^{2} P (I - P) = 0$ , while $A + B = z T$ . Apply [A13] and then step 1.3 to obtain, for every $z \in C$ , $D_{T} (z) = D_{z T} (1) = D_{z T P} (1) D_{z T (I - P)} (1) = D_{T P} (z) D_{T (I - P)} (z) .$

3.2A11A16A17A18A19step 2.2

The operator $T P$ has finite rank and range in $M$ , and $M$ is invariant; since $P ∣_{M} = I_{M}$ , [A11] gives $D_{T P} (z) = \det_{M} (I_{M} + z (T ∣_{M}))$ . A Jordan-string basis from [A16] makes the matrix of the nilpotent $J$ triangular with zero diagonal; hence the matrix of $I_{M} + z (T ∣_{M})$ is triangular with diagonal entries $1 + z λ$ . By [A17] and [A18] its operator determinant is this matrix determinant, and [A19] gives $D_{T P} (z) = (1 + z λ)^{d} .$

3.3A8step 2.1step 2.2

Put $z_{0} = - 1 / λ$ and $Q (z) : = D_{T (I - P)} (z)$ . On $M$ , $T (I - P)$ is zero; on $N$ , it is $T ∣_{N}$ . If $N \neq {0}$ , [A8] excludes $λ$ from $σ (T ∣_{N})$ , so $I_{N} + z_{0} T ∣_{N} = (λ I_{N} - T ∣_{N}) / λ$ has a bounded inverse. Its direct-sum inverse with $I_{M}$ is bounded because the projections $P$ and $I - P$ are bounded. If $N = {0}$ , the complementary operator is just the identity on $M$ . Thus $I + z_{0} T (I - P)$ is boundedly invertible on $H$ . Since $T (I - P)$ is trace class by step 2.2, step 2.1 yields $Q (z_{0}) \neq 0$ .

4.1A10A20step 3.1step 3.2step 3.3

By steps 3.1 and 3.2, $D_{T} (z) = λ^{d} (z - z_{0})^{d} Q (z) .$ The function $Q$ is entire by [A10], and step 3.3 gives $Q (z_{0}) \neq 0$ ; since $λ \neq 0$ , $λ^{d} Q$ is holomorphic and nonzero at $z_{0}$ . Thus [A20] shows that $D_{T}$ has a zero of order $d = m_{a l g} (λ; T)$ at $z_{0}$ .

5.1A2A3A4A10step 1.2step 4.1algebra

If $z \neq 0$ and $I + z T$ is not boundedly invertible, set $λ = - 1 / z$ . Then $I + z T = z (T - λ I)$ , so $λ \in σ (T)$ ; by [A2] and [A3], T is a compact operator on a complex Banach space, and [A4] makes $λ$ an eigenvalue. Step 4.1 applies and gives $D_{T} (z) = 0$ . The case $z = 0$ is invertible and has $D_{T} (0) = 1$ by [A10].

6.1A4step 2.1step 5.1

If $I + z T$ is boundedly invertible, step 2.1 with $U = T$ gives $D_{T} (z) \neq 0$ ; together with step 5.1 this proves both directions of the stated iff. For every nonzero spectral value, [A4] supplies an eigenvalue, so step 4.1 proves the multiplicity claim on the full nonzero spectrum.

7.1

The zero operator and zero Hilbert space are covered by step 1.1; on $H = C$ with $T = t I$ , the determinant is $1 + z t$ , so for $t \neq 0$ its zero is simple and $m_{a l g} (t; T) = 1$ , while $t = 0$ has no zero and every $I + z T$ is invertible. An empty nonzero spectrum yields no noninvertible $I + z T$ by step 5.1. There is no interval parameter or one-sided endpoint. The exact assumption is AC [A1]; it is used through the Riesz–Schauder, Riesz-projection, and algebraic-multiplicity suppliers, and AC supplies the AC $_{ω}$ required by the local determinant and trace-class suppliers through [A15]. The finite Jordan-string argument makes no additional choice. Both iff directions were proved in step 6.1; the multiplicity assertion is a factorization claim, not an iff. [A1, A4, A15, step 1.1, step 4.1, step 5.1, step 6.1] \qed

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30Open item page →

A quasinilpotent trace-class operator has zero trace

Statement

Assume the Axiom of Choice. Let $H$ be a separable complex Hilbert space and let $Q : H \to H$ be trace class with $σ (Q) \subseteq {0}$ . Then $tr (Q) = 0 and D_{Q} (z) = 1 (z \in C),$ where $D_{Q}$ is the locally constructed determinant.

Facts & Assumptions

Given: AC; a separable complex Hilbert space $H$ ; and a trace-class operator $Q : H \to H$ whose spectrum is contained in ${0}$ .

[A1]

AC selects from every family of nonempty sets (The Axiom of Choice).

[A2]

A complex Hilbert space is a Banach space in its induced norm (Hilbert space).

[A3]

A trace-class operator is a compact bounded operator (Trace class operator).

[A4]

The spectrum is the complement of the resolvent set (Spectrum and resolvent of a bounded operator).

[L1]

A scalar is in the resolvent set exactly when $λ I - Q$ is bijective with a bounded inverse (Spectrum and resolvent of a bounded operator).

[A5]

For trace-class $T$ on a separable complex Hilbert space, $D_{T} (z) = 0 ⟺ I + z T is not boundedly invertible$ (Zeros of the local Fredholm determinant).

[A6]

The local exterior-trace series defines an entire determinant (Local separable trace-class determinant construction).

[L2]

It satisfies $D_{T} (0) = 1$ and $D_{T}^{'} (0) = tr (T)$ (Local separable trace-class determinant construction).

[A7]

For bounded finite-rank $F$ and finite-dimensional invariant $E$ with $ran F \subseteq E$ , $D_{F} (z) = \det_{E} (I_{E} + z (F ∣_{E})),$ including the zero-dimensional case (Local separable trace-class determinant construction).

[A8]

For every $ε > 0$ there is $C_{ε} \geq 0$ such that $∣ D_{T} (z) ∣ \leq C_{ε} e^{ε ∣ z ∣} (z \in C)$ (Trace-norm continuity, growth and multiplicativity of the local determinant).

[A10]

For $x > 0$ , $\log x$ is the unique real $y$ with $\exp (y) = x$ (The natural logarithm as the inverse of the exponential function).

[A11]

The real logarithm is strictly increasing (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[L5]

For positive $x, y$ , $\log (x y) = \log x + \log y$ (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[A12]

For real $x, y$ , $∣ \exp (x + i y) ∣ = e^{x}$ ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ).

[A13]

Complex conjugation is involutive (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[L4]

$a \overline{a} = ∣ a ∣^{2}$ and the modulus is nonnegative (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive); applying this also to $\overline{a}$ gives $∣ \overline{a} ∣ = ∣ a ∣$ .

[A14]

AC implies DC and hence Countable Choice (AC implies DC implies countable choice); this supplies the choice assumptions used by the trace-class and determinant inputs.

Source audit: Kostenko, Trace Ideals with Applications, §3.4.4, Theorem 3.4.5 and the proof of Theorem 3.4.7 (printed pp. 40–42; PDF pp. 49–51) were read in full. The displayed proof of the spectral product and trace identity invokes the preceding Hadamard factorization theorem. This item does not use that factorization or the later library lemma on zero-free entire functions: steps 3.1–6.1 give the needed logarithm, disk estimate and Liouville argument locally. The cited source was a comparison, not a premise of this proof.

Proof

technique · direct

1.1A2A3A4L1A5algebra

Let $z \neq 0$ and set $λ = - 1 / z$ . The spectral hypothesis gives $λ \notin σ (Q)$ ; [A2] and [A3] put $Q$ in the bounded-operator spectrum setting. By [A4, L1], $λ I - Q$ has a bounded inverse, and $I + z Q = - z (λ I - Q)$ is boundedly invertible. The local zero criterion [A5] gives $D_{Q} (z) \neq 0$ .

2.1A5A6L2step 1.1

At $z = 0$ , [L2] gives $D_{Q} (0) = 1$ . Thus [A5] and step 1.1 make $D_{Q}$ zero-free on $C$ , while [A6] makes it entire.

3.1A6L2step 2.1

Put $f = D_{Q}$ . The quotient $f^{'} / f$ is entire because $f$ is entire and zero-free, using the local power-series and quotient rules (The sum of a complex power series is analytic throughout its open disc of convergence, A complex power-series sum has complex derivatives of every order, obtained by repeated termwise differentiation, Complex analytic functions are closed under finite linear combinations, products, quotients with nonzero denominator, and composition, A complex function is holomorphic if and only if it is analytic). Cauchy's theorem on the convex plane gives a primitive $h$ of $f^{'} / f$ ; subtract a constant so that $h (0) = 0$ (Cauchy's theorem on a convex complex domain, For a continuous function on a complex domain, endpoint independence, zero closed-contour integrals, and existence of a primitive are equivalent). The product and chain rules, together with $(e^{- h})^{'} = - h^{'} e^{- h}$ , show $(f e^{- h})^{'} = 0$ (Linearity, product, reciprocal, and quotient rules for complex derivatives, The chain rule for complex derivatives, The complex exponential is entire and its complex derivative is itself). Hence $f e^{- h} = f (0) = 1$ and $f = e^{h}$ (A holomorphic function with zero derivative on a domain is constant, $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential).

4.1A8A10A11A12step 3.1

For every $z$ , [A8] with $ε = 1$ gives $∣ f (z) ∣ \leq C_{1} e^{∣ z ∣}$ for some $C_{1} \geq 1$ , since $f (0) = 1$ . The exponential modulus formula [A12] gives $e^{Re h (z)} \leq C_{1} e^{∣ z ∣}$ ; [A10, A11] then imply $Re h (z) \leq A + ∣ z ∣$ , where $A = \log C_{1} \geq 0$ .

5.1step 4.1construct

We prove the required disk estimate. Fix $w \neq 0$ and $0 < t < 1$ , let $R = ∣ w ∣ / t$ and $K = A + R + 1$ . For $∣ ζ ∣ < 1$ , set $u = h (R ζ)$ and $G (ζ) = u / (2 K - u)$ . The bound from step 4.1 gives $Re u \leq A + R$ , so $K - Re u \geq 1$ and $∣ 2 K - u ∣^{2} - ∣ u ∣^{2} = 4 K (K - Re u) > 0.$ Thus $G$ is holomorphic, $G (0) = 0$ , and $∣ G ∣ < 1$ . The local power series of $G$ shows that $G (ζ) / ζ$ extends holomorphically through zero. On every circle $∣ ζ ∣ = r < 1$ , the maximum-modulus principle bounds this quotient by $1 / r$ ; letting $r ↑ 1$ gives $∣ G (ζ) ∣ \leq ∣ ζ ∣$ (The sum of a complex power series is analytic throughout its open disc of convergence, Boundary maximum modulus principle on a bounded domain). Since $∣ G ∣ = ∣ u ∣ / ∣ 2 K - u ∣$ , this implies $∣ u ∣ \leq ∣ ζ ∣ (2 K + ∣ u ∣)$ and hence $∣ u ∣ \leq 2 K ∣ ζ ∣ / (1 - ∣ ζ ∣)$ . Take $ζ = t w / ∣ w ∣$ , so $R ζ = w$ and $∣ ζ ∣ = t$ . Therefore $∣ h (w) ∣ \leq \frac{2 K t}{1 - t} = \frac{2 t (A + 1) + 2 ∣ w ∣}{1 - t} .$ Letting $t ↓ 0$ gives $∣ h (w) ∣ \leq 2 ∣ w ∣$ ; it also holds at $w = 0$ because $h (0) = 0$ .

6.1L2A6step 3.1step 5.1

The quotient $q (z) = h (z) / z$ extends to an entire function by the local power series of $h$ , with $q (0) = h^{'} (0)$ . Step 5.1 gives $∣ q (z) ∣ \leq 2$ for $z \neq 0$ , so continuity bounds it at zero as well. Liouville's theorem (Liouville's theorem: every bounded entire function is constant) makes $q$ constant, hence $h (z) = a z$ with $a = h^{'} (0) = f^{'} (0) / f (0) = D_{Q}^{'} (0) / D_{Q} (0)$ . Thus $D_{Q} (z) = e^{a z}$ .

7.1L2step 6.1

By [L2] and $D_{Q} (0) = 1$ , the coefficient in step 6.1 is $a = D_{Q}^{'} (0) = tr (Q)$ .

7.2L2A8A10A11L5A12A13L4step 6.1algebra

Suppose for contradiction that $a \neq 0$ , and choose $ε = ∣ a ∣ / 2 > 0$ . The bound [A8] has $C_{ε} \geq 1$ by evaluation at zero and [L2]. Set $t = 2 (\log C_{ε} + 1) / ∣ a ∣ > 0$ and $z_{t} = t \overline{a} / ∣ a ∣$ . By [A13, L4], $∣ z_{t} ∣ = t$ and $a z_{t} = t ∣ a ∣$ . Using step 6.1, [A12] and the [A8] bound gives $e^{t ∣ a ∣} = ∣ D_{Q} (z_{t}) ∣ \leq C_{ε} e^{ε t}$ . Apply [A10, A11, L5] to take logarithms: $t ∣ a ∣ \leq \log C_{ε} + ε t$ , hence $t ∣ a ∣ / 2 \leq \log C_{ε}$ . But the definition of $t$ makes the left side $\log C_{ε} + 1$ , a contradiction. Thus $a = 0$ .

7.3A1A4L1L2A7A14step 1.1step 6.1

If $Q = 0$ , [A7] with $E = {0}$ gives $D_{Q} \equiv 1$ , and [L2] then gives $tr (Q) = D_{Q}^{'} (0) = 0$ ; this includes $H = {0}$ . On $H = C$ with $Q = q I$ , the spectral condition forces $q = 0$ . Indeed, if $q \neq 0$ , then $Q 1 = q 1$ and $q I - Q = 0$ is not invertible, so [A4, L1] give $q \in σ (Q)$ . For $q = 0$ , [A7] with $E = H$ calculates $D_{Q} (z) = 1 + z q = 1$ , and [L2] gives trace zero. If $σ (Q) = \emptyset$ , step 1.1 still applies for every nonzero $z$ and no spectral enumeration is used. There is no endpoint parameter. The exact assumption is AC [A1]; it supplies AC $_{ω}$ through [A14] for the trace-class and determinant inputs. The scalar argument uses no further choice. The claim is an implication, not an equivalence, so both iff directions are inapplicable.

8.1

Step 6.1 with $a = 0$ gives $D_{Q} (z) = 1$ for every $z$ ; step 7.1 gives $tr (Q) = 0$ . This proves both conclusions. [step 6.1, step 7.1, step 7.2] \qed

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30Open item page →

Trace decomposition through generalized eigenspaces and the invariant quotient

Statement

Assume the Axiom of Choice. Let $H$ be a separable complex Hilbert space and let $T : H \to H$ be trace class. Write $Λ (T) = {λ \in σ (T) : λ \neq 0}$ , let $G_{λ} (T)$ be the generalized eigenspace and let $m_{a l g} (λ; T) = \dim G_{λ} (T)$ . Define $M : = \overline{span {G_{λ} (T) : λ \in Λ (T)}}, P : = P_{M}, Q : = I - P,$ where $P_{M}$ is the Hilbert orthogonal projection onto $M$ . Put $T_{M} : = T ∣_{M}$ and $D : = (Q T Q) ∣_{M^{⊥}}$ . Then $T_{M}$ and $D$ are trace class, and $D$ has no nonzero spectral values (the assertion is vacuous if $M^{⊥} = {0}$ ). With traces taken on their displayed Hilbert spaces, ${tr}_{H} (T) = {tr}_{M} (T_{M}) + {tr}_{M^{⊥}} (D), {tr}_{M} (T_{M}) = \sum_{λ \in Λ (T)} m_{a l g} (λ; T) λ,$ and the eigenvalue sum is absolutely convergent. The extension $Q T Q : H \to H$ is quasinilpotent and has trace zero.

Facts & Assumptions

Given: AC; a separable complex Hilbert space $H$ ; and a trace-class operator $T : H \to H$ .

[A1]

AC selects from every family of nonempty sets (The Axiom of Choice).

[A2]

In ZF, $A C \Rightarrow D C \Rightarrow {A C}_{ω}$ (AC implies DC implies countable choice).

[A3]

A complex Hilbert space is a Banach space in its induced norm (Hilbert space).

[A4]

A trace-class operator is compact and bounded (Trace class operator).

[A5]

A compact operator on a complex Banach space has finite-dimensional generalized eigenspaces at its nonzero spectral values; every such value is an eigenvalue, and only finitely many spectral values have modulus at least any fixed $ε > 0$ (Riesz schauder spectrum of a compact operator).

[A6]

For each nonzero eigenvalue $λ$ , $G_{λ} (T)$ is the stabilized kernel of $(T - λ I)^{m}$ , is finite dimensional, and $m_{a l g} (λ; T) = \dim G_{λ} (T) = rank P_{λ}$ (Algebraic multiplicity of a nonzero compact-operator eigenvalue).

[A7]

For an isolated spectral value, the Riesz projection is a bounded idempotent commuting with $T$ , its range and kernel are closed invariant subspaces giving a direct sum, and the restriction spectra are the two spectral parts (Riesz spectral projection, Riesz spectral projection properties).

[A8]

A subspace $W$ is $T$ -invariant when $T (W) \subseteq W$ , and this invariance makes $\overset{ˉ}{T} (v + W) : = T (v) + W$ a well-defined linear operator on $H / W$ with canonical projection $π : H \to H / W$ satisfying $π T = \overset{ˉ}{T} π$ (Invariant subspaces, restrictions, and induced quotient operators, The quotient vector space $V / W$ and its canonical projection, Invariance makes the induced quotient operator well defined and linear, with $π T = \overset{ˉ}{T} π$ ).

[A9]

The quotient seminorm is $∥ x + W ∥ = \inf_{w \in W} ∥ x + w ∥$ and is a norm when $W$ is closed (The quotient seminorm (|x+M|{X/M}=\inf{m\in M}|x+m|=\operatorname{dist}(x,M)), The quotient seminorm is a norm exactly when the subspace is closed).

[A10]

Under AC, if $X$ is Banach and $K : X \to X$ is compact, then $I - K$ is injective if and only if it is surjective, and either condition gives a bounded inverse (Fredholm alternative for identity minus compact).

[A11]

A trace-class operator remains trace class after composition on either side with bounded maps between Hilbert spaces (Trace class is a two sided Banach operator ideal).

[A12]

For every supplied Hilbert basis $E$ of a trace-class operator $S$ , its relative trace is ${tr}_{E} (S) = \sum_{e \in E} ⟨ S e, e ⟩$ ; the series is absolutely convergent, and the trace theorem identifies it with the basis-independent trace $tr (S)$ (Trace of a trace class operator, Trace is absolutely convergent and basis independent).

[A13]

A closed subspace of a Hilbert space is Hilbert; an orthogonal projection onto a closed subspace gives $H = M \oplus M^{⊥}$ , is self-adjoint, and is contractive (Orthogonal decomposition by a closed subspace, The Hilbert orthogonal projection onto a closed subspace, Hilbert projections are linear, self-adjoint and contractive).

[A14]

From a supplied dense sequence in a Hilbert space, Gram--Schmidt gives a finite or countable Hilbert basis (A Hilbert space with a dense sequence has a finite or countable orthonormal basis).

[A15]

For a trace-class compact operator, the eigenvalue sequence repeated by algebraic multiplicity can be listed so that $\sum_{j} ∣ λ_{j} (T) ∣ \leq ∥ T ∥_{1}$ (Weyl product and sum inequalities for compact operators).

[A16]

Every finite-dimensional nilpotent endomorphism has an ordered basis concatenating Jordan strings (Every finite-dimensional nilpotent endomorphism has a basis of Jordan strings); on a string $(v_{1}, \dots, v_{m})$ at $λ$ , $(T - λ I) v_{1} = 0$ and $(T - λ I) v_{j} = v_{j - 1}$ for $j \geq 2$ (Jordan blocks, Jordan strings, and their endpoints).

[A17]

If $S$ is trace class on a separable complex Hilbert space and $σ (S) \subseteq {0}$ , then $tr (S) = 0$ (A quasinilpotent trace-class operator has zero trace).

[A18]

The complex inner product is linear in its first argument and conjugate-linear in its second (Real and complex inner-product spaces and their induced length).

[A19]

A closed linear subspace of a Banach space is Banach in its induced norm (A closed subspace of a Banach space is Banach).

[A20]

For a bounded operator on a complex Banach space, $λ \notin σ (T)$ exactly when $λ I - T$ is bijective with bounded inverse (Spectrum and resolvent of a bounded operator).

[A21]

Boundedness of $T$ supplies a constant $C_{T} \geq 0$ with $∥ T x ∥ \leq C_{T} ∥ x ∥$ for every $x \in H$ (A bounded linear operator between normed spaces).

[A22]

Separability of $H$ supplies a dense sequence in $H$ (Separability: the existence of an at most countable dense subset).

Choice accounting: The exact assumption is AC. It supplies DC for Riesz--Schauder/Fredholm suppliers and AC $_{ω}$ for trace, projection and separable-basis suppliers. The Weyl list supplies an enumeration of the nonzero eigenvalue multiset; AC $_{ω}$ permits choosing Jordan-string bases for its countably many finite-dimensional generalized eigenspaces. The basis of $M^{⊥}$ is obtained by projecting a supplied dense sequence of $H$ and applying the choice-free Gram--Schmidt construction. No ambient basis is used without being supplied or constructed.

Source audit: Kostenko's §3.4.4 proof of Theorem 3.4.7 derives the spectral product and trace identity by invoking Theorem 3.4.5, the Hadamard minimal-type product formula. Van Neerven's Theorem 14.33 proof obtains the determinant spectral product from Theorem 14.43, whose proof invokes Lemma 14.42; Proposition 14.22 separately gives the eigenvalue absolute-sum bound and uses finite-dimensional invariant generalized-eigenspace sums. These routes are comparison only. This item proves the trace on $M$ using an adapted orthonormal basis and proves the compressed quotient has no nonzero spectrum using Riesz splitting and the compact Fredholm alternative. Kostenko's Theorem 3.4.7 proof and van Neerven's Proposition 14.22 and Theorem 14.33 arguments were read in full; no source premise is left unverified.

Proof

technique · direct

1.1A3A4algebra

If $H = {0}$ , then $M = M^{⊥} = {0}$ , all operators and traces in the claim are zero, and the eigenvalue sum is empty; hence assume $H \neq {0}$ .

2.1A3A4A6A13step 1.1algebra

Each $G_{λ} (T)$ is $T$ -invariant because $(T - λ I)^{m} T x = T (T - λ I)^{m} x = 0$ for $x \in G_{λ} (T)$ ; boundedness of $T$ then makes its closed span $M$ invariant. By [A13], $P = P_{M}$ and $Q = I - P$ are bounded orthogonal projections, $H = M \oplus N$ with $N = M^{⊥}$ , and both $M, N$ are closed Hilbert subspaces.

3.1A11step 2.1algebra

Let $i_{M} : M ↪ H$ and $i_{N} : N ↪ H$ be inclusions. Invariance gives $T_{M} = P T i_{M}$ , while $D = Q T i_{N}$ and $B : = Q T Q$ on $H$ ; by [A11] all three are trace class, and $B ∣_{M} = 0$ , $B ∣_{N} = D$ .

4.1A1A2A6A12A15A16A18step 3.1algebra

Let $(λ_{j})$ be the finite or countable nonzero eigenvalue list from [A15], repeated by algebraic multiplicity. For each distinct $λ$ , choose a Jordan-string basis of $G_{λ} (T)$ for $(T - λ I) ∣_{G_{λ} (T)}$ using [A6, A16]. These generalized eigenspaces are linearly independent: in a finite relation $\sum_{μ} x_{μ} = 0$ , $x_{μ} \in G_{μ}$ , applying $R_{λ} = \prod_{μ \neq λ} (T - μ I)^{m_{μ}}$ kills every other term, while each factor on $G_{λ}$ is $(λ - μ) I + N_{λ}$ with $N_{λ}$ nilpotent and hence invertible by a finite geometric sum; thus $x_{λ} = 0$ . Order the distinct eigenvalues by their first occurrence in $(λ_{j})$ and concatenate their string bases. Every finite initial span is $T$ -invariant, and its successive one-dimensional quotient acts by the corresponding eigenvalue. Applying Gram--Schmidt preserves these initial spans, so it gives a Hilbert basis $(e_{j})$ of $M$ with $T e_{j} - λ_{j}^{'} e_{j} \in span (e_{1}, \dots, e_{j - 1})$ , where $(λ_{j}^{'})$ is a reordering of $(λ_{j})$ . By [A12], [A18], and [A15], ${tr}_{M} (T_{M}) = \sum_{j} ⟨ T e_{j}, e_{j} ⟩ = \sum_{j} λ_{j}^{'} = \sum_{j} λ_{j}$ , and the sum is absolutely convergent. The empty and finite lists give the empty and finite bases.

4.2A8A9A13A21step 2.1step 3.1algebra

Let $X : = H / M$ with its quotient norm and let $π : H \to X$ be the canonical projection. By [A8, A9], $\overset{ˉ}{T} (x + M) = T x + M$ is well defined. For $m \in M$ , $T x + T m \in T x + M$ , so [A21] gives $∥ \overset{ˉ}{T} (x + M) ∥ \leq C_{T} ∥ x + m ∥$ ; taking the infimum over $m$ shows that $\overset{ˉ}{T}$ is bounded. The map $J : N \to X$ , $J (n) = n + M$ , is an isometric isomorphism: every coset has the representative $Q x \in N$ , and $∥ n + M ∥ = \inf_{m \in M} ∥ n - m ∥ = ∥ n ∥$ by orthogonality. For $D = Q T ∣_{N}$ , $J D = \overset{ˉ}{T} J$ .

5.1A12A13A14A22step 2.1step 3.1

By [A22] take a dense sequence $(h_{j})$ in $H$ . Contractivity of $P, Q$ makes $(P h_{j})$ dense in $M$ and $(Q h_{j})$ dense in $N$ , so [A14] supplies Hilbert bases $E_{M}$ of $M$ and $E_{N}$ of $N$ ; the basis of $M$ may be the adapted one from step 4.1. Their union is a Hilbert basis of $H$ . For $e \in E_{M}$ , $T e = T_{M} e$ ; for $f \in E_{N}$ , $T f - B f = P T f \in M ⊥ f$ , and $B e = 0$ . Summing the absolutely convergent diagonal series from [A12] over these two disjoint basis parts yields ${tr}_{H} (T) = {tr}_{M} (T_{M}) + {tr}_{H} (B)$ and ${tr}_{H} (B) = {tr}_{N} (D)$ .

5.2A3A4A8A10A13A19A20step 2.1step 3.1step 4.2algebra

Fix $λ \neq 0$ with $λ \notin σ (T)$ and set $A = λ I - T$ . By [A20], $A$ has a bounded inverse on $H$ . Its restriction to $M$ is injective; $A ∣_{M} = λ (I_{M} - T_{M} / λ)$ , where $T_{M}$ is compact by [A4, step 3.1], and $M$ is Banach by [A3, A13, A19]. The Fredholm alternative [A10] makes $A ∣_{M}$ surjective with bounded inverse. Consequently $A^{- 1} (M) = M$ and the induced quotient operator $\overset{ˉ}{A} = λ I_{X} - \overset{ˉ}{T}$ has the bounded inverse induced by $A^{- 1}$ .

5.3A3A4A5A6A7A8A9A10A19A20step 2.1step 3.1step 4.2algebra

Fix $λ \neq 0$ with $λ \in σ (T)$ . By [A5], $λ$ is an eigenvalue; the finiteness of every nonzero spectral annulus isolates it, so [A7] gives the Riesz projection $P_{λ}$ , with $G : = G_{λ} (T) = ran P_{λ}$ and $Y : = \ker P_{λ}$ . Put $M_{0} : = M \cap Y$ . For $x \in G_{μ} (T)$ with $μ \neq λ$ , $P_{λ} x \in G$ and $(T - μ I)^{m} P_{λ} x = P_{λ} (T - μ I)^{m} x = 0$ ; on $G$ , $T - μ I = (λ - μ) I + N_{λ}$ is invertible, so $P_{λ} x = 0$ , while $P_{λ}$ is the identity on $G$ . Continuity and the definition of $M$ give $P_{λ} (M) \subseteq G \subseteq M$ , hence $M = G \oplus M_{0}$ . If $Y \neq {0}$ , [A7] gives that $A_{Y} : = λ I_{Y} - T ∣_{Y}$ is boundedly invertible; its restriction to $M_{0}$ is injective. The subspace $M_{0}$ is closed in $M$ , so [A19] makes it Banach. The restriction $T ∣_{M_{0}}$ is compact because a bounded sequence in $M_{0}$ has a subsequence whose $T$ -images converge in $H$ , and the limit lies in $M_{0}$ by closedness. Thus [A10] makes $A ∣_{M_{0}} = λ (I_{M_{0}} - T ∣_{M_{0}} / λ)$ boundedly invertible and $A_{Y}^{- 1} (M_{0}) = M_{0}$ . Thus $A_{Y}$ and its inverse both preserve $M_{0}$ , so they induce mutually inverse bounded operators on $Y / M_{0}$ . The map $Φ : Y / M_{0} \to H / M$ , $y + M_{0} \mapsto y + M$ , is well defined and bounded: changing $y$ by an element of $M_{0}$ does not change its image, and $∥ y + M ∥ \leq ∥ y + M_{0} ∥$ . It is onto because $x + M = (I - P_{λ}) x + M$ and $(I - P_{λ}) x \in Y$ ; it is one-to-one because $Y \cap M = M_{0}$ . Its inverse is therefore $x + M \mapsto (I - P_{λ}) x + M_{0}$ . This inverse is well defined since $(I - P_{λ}) M \subseteq M_{0}$ , and bounded with norm at most $∥ I - P_{λ} ∥$ : for every $m \in M$ , $(I - P_{λ}) (x + m)$ represents the same image modulo $M_{0}$ , so taking the infimum over $m$ gives the bound. The map $Φ$ intertwines the induced operators because $A_{Y} y + M = A y + M$ for $y \in Y$ . Hence $\overset{ˉ}{A} = λ I_{X} - \overset{ˉ}{T}$ is boundedly invertible. If $Y = {0}$ then $P_{λ} = I_{H}$ , so $G = H \subseteq M$ , hence $M = H$ and $X = {0}$ , whose unique endomorphism is bijective, giving the same quotient conclusion.

6.1A20step 4.2step 5.2step 5.3algebra

Steps 5.2--5.3 show that $λ I_{X} - \overset{ˉ}{T}$ is boundedly invertible for every $λ \neq 0$ . By step 4.2, $λ I_{N} - D$ is also boundedly invertible. Since $B = 0_{M} \oplus D$ on the orthogonal sum $H = M \oplus N$ , the operator $λ I_{H} - B = λ I_{M} \oplus (λ I_{N} - D)$ has a bounded inverse for every $λ \neq 0$ . Thus [A20] gives $σ_{H} (B) \subseteq {0}$ ; the compression $D$ has no nonzero spectral values whenever $N \neq {0}$ .

7.1

Apply [A17] to the trace-class quasinilpotent operator $B$ on the original separable $H$ to get ${tr}_{H} (B) = 0$ . Step 5.1 then gives ${tr}_{H} (T) = {tr}_{M} (T_{M})$ , and step 4.1 identifies this with the absolutely convergent eigenvalue sum. If there are no nonzero eigenvalues then $M = 0$ , $B = T$ , and the same argument yields the empty sum $0$ ; this includes $T = 0$ . If $H = C$ and $T = q I$ , then for $q \neq 0$ the sole eigenvalue is $q$ with multiplicity one, $M = H$ , and the two traces are $q$ and $0$ ; for $q = 0$ the eigenvalue list and $M$ are empty/zero and all traces vanish. There is no endpoint parameter, and the statement is not an equivalence, so both iff directions are inapplicable. AC is explicit in [A1] and propagates to AC $_{ω}$ through [A2] for the trace, Weyl, projection and basis suppliers. [A1, A2, A17, step 4.1, step 5.1, step 6.1] \qed

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30Open item page →

Spectral product from traces of powers

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $H$ be a separable complex Hilbert space (Hilbert space) and let $T : H \to H$ be trace class (Trace class operator). List its nonzero eigenvalues $λ_{j} (T)$ , repeated according to algebraic multiplicity (Algebraic multiplicity of a nonzero compact-operator eigenvalue). Then $D_{T} (z) = \prod_{j \geq 1} (1 + z λ_{j} (T)) (z \in C),$ where $D_{T}$ is the locally constructed determinant of Local separable trace-class determinant construction. The product converges locally uniformly; if the nonzero eigenvalue list is empty, the product is one.

Facts & Assumptions

Given: AC, a separable complex Hilbert space $H$ , a trace-class operator $T : H \to H$ , and the eigenvalue list supplied by the Weyl inequality below.

[A1]

AC implies Dependent Choice and Countable Choice; the latter supplies the countable-choice hypotheses of the trace-class, determinant and trace constructions (The Axiom of Choice, AC implies DC implies countable choice).

[A2]

A trace-class operator is compact and bounded (A bounded linear operator between normed spaces); composing a trace-class operator with bounded operators preserves trace class and obeys the two-sided trace-norm ideal estimate (Trace class operator, Trace class is a two sided Banach operator ideal).

[A3]

If $H \neq {0}$ is a complex Hilbert space (Hilbert space), it is Banach; hence $B (H)$ is Banach by If (Y) is Banach then (\mathcal B(X,Y)) is Banach. Composition is associative and its operator norm is submultiplicative (The operator norm as the least bound and as the unit-sphere or unit-ball supremum, Composition satisfies |ST|\le|S|,|T|). The identity has norm $1$ and is nonzero, so this is a nonzero unital complex Banach algebra (Unital Banach algebra).

[A4]

In a unital complex Banach algebra, $∥ a ∥ < 1$ implies that $1 - a$ is invertible with inverse $\sum_{k \geq 0} a^{k}$ (Neumann series).

[A5]

The spectrum of $T$ as an operator is the spectrum of the corresponding element of $B (H)$ ; in a unital complex Banach algebra polynomial spectral mapping gives $σ (T^{n}) = {λ^{n} : λ \in σ (T)}$ (Spectrum and resolvent of a bounded operator, Spectrum and resolvent set in a Banach algebra, Polynomial spectral mapping).

[A6]

Under AC, every nonzero spectral value of a compact operator is an eigenvalue with a finite-dimensional generalized eigenspace, and its generalized eigenspace stabilizes; its dimension is its algebraic multiplicity (Riesz schauder spectrum of a compact operator, Algebraic multiplicity of a nonzero compact-operator eigenvalue).

[A7]

A degree- $n$ complex polynomial has $n$ roots counted with multiplicity; polynomial evaluation at an endomorphism preserves sums and products (A complex polynomial of degree $n$ has exactly $n$ roots counted with multiplicity, Polynomial evaluation at an endomorphism: $p (T) = \sum_{k} a_{k} T^{k}$ ).

[A8]

If coprime polynomials $f, g$ satisfy $(f g) (S) = 0$ for an endomorphism $S$ , then its space is the direct sum $\ker f (S) \oplus \ker g (S)$ (If $\gcd (f, g) = 1$ and $(f g) (T) = 0$ , then $V = \ker f (T) \oplus \ker g (T)$ ).

[A9]

Under AC, for every trace-class $S$ on a separable complex Hilbert space, $tr (S) = \sum_{μ \in σ (S) ∖ {0}} m_{a l g} (μ; S) μ,$ and this eigenvalue sum is absolutely convergent (Trace decomposition through generalized eigenspaces and the invariant quotient).

[A10]

The nonzero eigenvalues of a compact trace-class $T$ , repeated by algebraic multiplicity, can be listed as $λ_{j} (T)$ with $\sum_{j \geq 1} ∣ λ_{j} (T) ∣ \leq ∥ T ∥_{1};$ a finite list may be padded by zeros (Weyl product and sum inequalities for compact operators).

[A11]

The trace is linear and $∣ tr (S) ∣ \leq ∥ S ∥_{1}$ for trace-class $S$ (Trace is absolutely convergent and basis independent).

[A12]

For separable complex $H$ , $D_{T}$ is entire; if $I + z T$ is boundedly invertible, then $D_{T}^{'} (z) = D_{T} (z) tr ⁣ (T (I + z T)^{- 1})$ (Local separable trace-class determinant construction, Logarithmic derivative of the local Fredholm determinant).

[A13]

Complex polynomials are entire; a locally uniform limit of holomorphic functions is holomorphic and the derivatives of the approximants converge locally uniformly to the derivative of the limit (Complex polynomials are entire with the power-rule derivative, and rational functions are holomorphic wherever their denominator is nonzero, Locally uniform limits of holomorphic functions are holomorphic and their derivatives converge locally uniformly).

[A14]

The complex quotient rule holds where the denominator is nonzero; a holomorphic function with identically zero derivative on a domain is constant; holomorphic functions on a domain that agree on a set with an interior accumulation point agree throughout the domain (Linearity, product, reciprocal, and quotient rules for complex derivatives, A complex domain is a nonempty connected open subset of $C$ , A holomorphic function with zero derivative on a domain is constant, Identity theorem for holomorphic functions).

[A15]

The exterior construction has degree-zero operator $I_{C}$ and for $n \geq 1$ sends the induced operator of the zero map to zero (Hilbert exterior powers and induced operators).

[A16]

For the local determinant, $D_{T} (z) = 0$ if and only if $I + z T$ is not boundedly invertible (Zeros of the local Fredholm determinant).

Source-route audit. Kostenko, §3.4.4, Theorem 3.4.7, obtains the spectral product by combining the determinant zero criterion with Theorem 3.4.5, Hadamard's minimal-type product formula, and Weyl summability. Van Neerven, §14.5.a, Theorem 14.43, obtains the same product from Lemma 14.42, which invokes Hadamard factorization. Dyatlov–Zworski, Appendix B §B.6, states the product and trace formula and begins the determinant proof with its zero set and multiplicities. These complete source passages were read as comparison arguments; none is used as proof here. This item derives the equality from the trace-power identity and the local logarithmic derivatives. No Hadamard-factorization premise is used.

Proof

technique · direct

Given: The data in the statement. Write $S : = \sum_{j \geq 1} ∣ λ_{j} (T) ∣$ , which is finite by [A10].

1.1A12A15

If $H = {0}$ or $T = 0$ , then every positive-degree exterior power of $T$ is zero by [A15], so the determinant series gives $D_{T} \equiv 1$ . There are no nonzero eigenvalues, so the product is empty and equals one. We henceforth assume $H \neq {0}$ and $T \neq 0$ .

1.2A1A2A3A4A5

By [A1], AC supplies the Dependent Choice and Countable Choice assumptions used below. By [A2], $T$ is compact and bounded. The algebra result [A3] applies to the nonzero complex Hilbert space $H$ , so the Neumann series [A4] and polynomial spectral mapping [A5] apply in $B (H)$ . The operator spectrum and the algebra spectrum agree by [A5].

1.3A10A13algebra

For each nonzero eigenvalue $λ$ of $T$ , an eigenvector $x \neq 0$ satisfies $∣ λ ∣ ∥ x ∥ = ∥ T x ∥ \leq ∥ T ∥ ∥ x ∥$ . Hence $∣ λ_{j} (T) ∣ \leq ∥ T ∥$ for every $j$ . Let $P_{N} (z) : = \prod_{j = 1}^{N} (1 + z λ_{j} (T))$ , with $P_{0} = 1$ . For $∣ z ∣ \leq R$ and $m < N$ , $∣ \prod_{j = m + 1}^{N} (1 + z λ_{j} (T)) - 1 ∣ \leq \prod_{j = m + 1}^{N} (1 + R ∣ λ_{j} (T) ∣) - 1 \leq e^{R \sum_{j > m} ∣ λ_{j} (T) ∣} - 1.$ Also $∣ P_{m} (z) ∣ \leq e^{R S}$ . Since the right-hand tail tends to zero, $(P_{N})$ is uniformly Cauchy on every closed disk of finite radius. Its limit $Φ (z) : = \lim_{N \to \infty} P_{N} (z)$ is locally uniform, and [A13] makes $Φ$ entire. For a finite eigenvalue list, zero padding makes $P_{N}$ eventually constant; for an empty list, every $P_{N}$ is $1$ .

1.4A3A4A10A16

Since $T \neq 0$ , $∥ T ∥ > 0$ . Choose $r > 0$ with $r ∥ T ∥ < 1$ and $r S < 1 / 2$ (the second condition is automatic when $S = 0$ ). For $∣ z ∣ < r$ , every factor is nonzero, and for every finite $N$ , $∣ P_{N} (z) ∣ \geq \prod_{j = 1}^{N} (1 - ∣ z ∣ ∣ λ_{j} (T) ∣) \geq 1 - ∣ z ∣ \sum_{j = 1}^{N} ∣ λ_{j} (T) ∣ > 1 / 2.$ The finite-product inequality follows by induction from $\prod_{j} (1 - a_{j}) \geq 1 - \sum_{j} a_{j}$ for $0 \leq a_{j} \leq 1$ . Passing to the limit shows $∣ Φ (z) ∣ \geq 1 / 2$ , so $Φ$ has no zeros on this disk. Also $∥ z T ∥ < 1$ , so [A4] makes $I + z T$ invertible; [A16] then gives $D_{T} (z) \neq 0$ there.

1.5A2A9

For every integer $n \geq 1$ , [A2] shows inductively that $T^{n}$ is trace class and $∥ T^{n} ∥_{1} \leq ∥ T ∥_{1} ∥ T ∥^{n - 1} .$ In particular, $T^{n}$ is compact and the trace decomposition [A9] applies to $T^{n}$ .

1.6A5A6A7A8

Fix $n \geq 1$ and $μ \neq 0$ in $σ (T^{n})$ . By [A5], $μ = λ^{n}$ for some $λ \in σ (T)$ . The roots $α$ of $x^{n} - μ$ are all distinct: if $α^{n} = μ \neq 0$ , then the derivative $n α^{n - 1}$ is nonzero. By [A7], $x^{n} - μ = \prod_{α^{n} = μ} (x - α), (T^{n} - μ I)^{k} = \prod_{α^{n} = μ} (T - α I)^{k} .$ The factors $(x - α)^{k}$ are pairwise coprime. Put $V : = \ker \prod_{α^{n} = μ} (T - α I)^{k}$ . Since its defining polynomial commutes with $T$ , $V$ is $T$ -invariant. On $V$ that product annihilates $T ∣_{V}$ . Apply [A8] first to one factor and the product of the rest, then repeat on the remaining product-kernel. A vector in any one factor-kernel is already in $V$ , so this gives $\ker (T^{n} - μ I)^{k} = ⨁_{α^{n} = μ} \ker (T - α I)^{k} .$ Choose $k$ at least the finitely many stabilization exponents for $T^{n}$ at $μ$ and for $T$ at the roots $α$ . By [A6], this proves $G_{μ} (T^{n}) = ⨁_{α^{n} = μ} G_{α} (T), m_{a l g} (μ; T^{n}) = \sum_{\begin{array}{c} α^{n} = μ \\ α \in σ (T) \end{array}} m_{a l g} (α; T) .$ Roots outside $σ (T)$ have zero generalized eigenspace and are omitted. This gives the collision multiplicities for every nonzero eigenvalue of $T^{n}$ .

2.1A9A10step 1.6algebra

Apply [A9] to $T^{n}$ and group by the finitely many roots of each $μ$ . The grouping is legitimate because $\sum_{j \geq 1} ∣ λ_{j} (T) ∣^{n} \leq ∥ T ∥^{n - 1} \sum_{j \geq 1} ∣ λ_{j} (T) ∣ < \infty .$ Using the multiplicity identity established above gives, for every $n \geq 1$ , $tr (T^{n}) = \sum_{μ \in σ (T^{n}) ∖ {0}} m_{a l g} (μ; T^{n}) μ = \sum_{j \geq 1} λ_{j} (T)^{n} .$ If the nonzero eigenvalue list is empty, both sides are zero by [A9].

3.1A2A4A11A12step 1.4step 2.1

On $∣ z ∣ < r$ , the Neumann expansion from [A4] and the ideal estimate [A2] give convergence in trace norm: $T (I + z T)^{- 1} = \sum_{k \geq 0} (- z)^{k} T^{k + 1}, \sum_{k \geq 0} ∥ z^{k} T^{k + 1} ∥_{1} \leq ∥ T ∥_{1} \sum_{k \geq 0} (∣ z ∣ ∥ T ∥)^{k} < \infty .$ Trace linearity and its trace-norm bound [A11] therefore permit taking traces term by term. Dividing the logarithmic-derivative identity [A12] by the nonvanishing determinant established above, and using the trace-power identity already established, yields $\frac{D_{T}^{'} (z)}{D_{T} (z)} = \sum_{k \geq 0} (- 1)^{k} z^{k} tr (T^{k + 1}) = \sum_{k \geq 0} (- 1)^{k} z^{k} \sum_{j \geq 1} λ_{j} (T)^{k + 1} .$

4.1A10A13step 1.4step 2.1step 3.1algebra

For each finite $N$ , the product rule [A13] gives on $∣ z ∣ < r$ $\frac{P_{N}^{'} (z)}{P_{N} (z)} = \sum_{j = 1}^{N} \frac{λ_{j} (T)}{1 + z λ_{j} (T)} .$ The denominators are bounded below by $1 - r ∥ T ∥ > 0$ . On each closed disk $∣ z ∣ \leq ρ < r$ , the right side converges uniformly as $N \to \infty$ , because its tail is bounded by $(1 - ρ ∥ T ∥)^{- 1} \sum_{j > N} ∣ λ_{j} (T) ∣$ . By [A13], $P_{N} \to Φ$ and $P_{N}^{'} \to Φ^{'}$ locally uniformly. Since $Φ$ has no zeros on $∣ z ∣ < r$ , taking the limit gives $\frac{Φ^{'} (z)}{Φ (z)} = \sum_{j \geq 1} \frac{λ_{j} (T)}{1 + z λ_{j} (T)} .$ For $∣ z ∣ \leq ρ < r$ , expand each denominator geometrically. The double series is absolutely convergent because $\sum_{j \geq 1} \sum_{k \geq 0} ρ^{k} ∣ λ_{j} (T) ∣^{k + 1} \leq \frac{S}{1 - ρ ∥ T ∥} < \infty .$ Thus it may be rearranged, and the trace-power identity gives $\frac{Φ^{'} (z)}{Φ (z)} = \sum_{k \geq 0} (- 1)^{k} z^{k} \sum_{j \geq 1} λ_{j} (T)^{k + 1} = \sum_{k \geq 0} (- 1)^{k} z^{k} tr (T^{k + 1}) = \frac{D_{T}^{'} (z)}{D_{T} (z)} .$

5.1A12A14step 1.3step 1.4step 4.1

The disk $U = {z : ∣ z ∣ < r}$ is a complex domain. Since $Φ$ is nonzero there, $Q : = D_{T} / Φ$ is holomorphic on $U$ . The quotient rule [A14] and the derivative equality above give $Q^{'} = 0$ on $U$ . Hence [A14] makes $Q$ constant; as $D_{T} (0) = Φ (0) = 1$ , $Q \equiv 1$ on $U$ . Thus $D_{T} = Φ$ on a nonempty open disk. Both functions are entire by [A12] and the locally uniform product construction. The identity theorem [A14] extends their equality to all of $C$ , and the product convergence is locally uniform by construction.

6.1A1A10A12step 1.1step 1.3step 5.1

If there is exactly one nonzero eigenvalue in the list, the finite product is the single factor $1 + z λ_{1} (T)$ and the product and trace-power calculations above still apply. In particular, on a one-dimensional $H$ with $T = t I$ , the local determinant construction reduces to $\det_{H} (I + z T) = 1 + z t$ , which is exactly the product when $t \neq 0$ , and is the empty product when $t = 0$ . The zero operator and zero-dimensional space were handled above; finite lists stabilize in the product construction; no finite-dimensionality or nonzero-eigenvalue assumption is made for the general case. All disks used above have positive radius and every estimate is on a compact disk strictly inside the chosen radius; global equality includes every complex endpoint. AC is the exact assumption [A1], inherited by the spectral and trace suppliers, with no additional choice made. The conclusion is an equality, not an iff statement, so both iff directions are inapplicable.

\qed

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30Open item page →

Arbitrary-Hilbert Fredholm determinant from a separable reducing support

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $H$ be any complex Hilbert space and let $T : H \to H$ be trace class (Hilbert space, Trace class operator). For a nuclear representation $T x = \sum_{j \geq 1} ⟨ x, u_{j} ⟩ v_{j}, \sum_{j \geq 1} ∥ u_{j} ∥ ∥ v_{j} ∥ < \infty,$ put $M = \overline{{span}_{C} {u_{j}, v_{j} : j \geq 1}} .$ Then $M$ is separable and reducing for $T$ , and under $H = M \oplus M^{⊥}$ one has $T = S \oplus 0$ , where $S = T ∣_{M}$ is trace class. Let $D_{S}$ be the locally constructed separable determinant of Local separable trace-class determinant construction and define $D_{H} (I + z T) : = D_{S} (z) .$ This definition is independent of the nuclear representation and, more generally, of any closed separable support $N$ satisfying $T (H) \subseteq N$ and $T ∣_{N^{⊥}} = 0$ ; such an $N$ reduces $T$ . The result is entire, has value $1$ at $z = 0$ , and satisfies the locally uniform product $D_{H} (I + z T) = \prod_{j} (1 + z λ_{j} (T)),$ where the nonzero eigenvalues are repeated according to algebraic multiplicity (Algebraic multiplicity of a nonzero compact-operator eigenvalue). If $T$ has finite rank, then for every finite-dimensional $E \subseteq H$ containing $ran T$ , $D_{H} (I + z T) = \det_{E} (I_{E} + z (T ∣_{E})),$ with determinant on the zero-dimensional space equal to $1$ (The determinant of an endomorphism of a finite-dimensional vector space: its matrix determinant in an ordered basis in positive dimension, and $1$ on the zero space).

Facts & Assumptions

Given: AC, a complex Hilbert space $H$ , a trace-class operator $T$ , and a nuclear representation as in the statement when one is fixed.

[A1]

AC is the principle that every family of nonempty sets has a choice function. It implies DC and Countable Choice, which are the exact choice strengths used by the Hilbert projection and trace-class/determinant suppliers (The Axiom of Choice, AC implies DC implies countable choice).

[A2]

Under Countable Choice, a trace-class $T$ has a nuclear representation with operator-norm-convergent partial sums and finite sum $\sum_{j} ∥ u_{j} ∥ ∥ v_{j} ∥$ ; this is the nuclear-series characterization (Nuclear series characterizes trace norm).

[A3]

The inner product is linear in its first argument. For a bounded operator, the Hilbert adjoint satisfies $⟨ T x, y ⟩ = ⟨ x, T^{*} y ⟩$ and is uniquely determined by this identity (Real and complex inner-product spaces and their induced length, The Hilbert-space adjoint of a bounded operator). Orthogonality to $M$ means $⟨ x, m ⟩ = 0$ for every $m \in M$ .

[A4]

The operator norm is the unit-ball supremum; scaling a nonzero vector to the unit ball gives $∥ U x ∥ \leq ∥ U ∥ ∥ x ∥$ for each bounded $U$ (A bounded linear operator between normed spaces, The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

[A5]

Every closed subspace $N$ of a Hilbert space has the orthogonal decomposition $H = N \oplus N^{⊥}$ under Countable Choice; its projection $P_{N}$ is bounded with norm at most $1$ (Orthogonal decomposition by a closed subspace, The Hilbert orthogonal projection onto a closed subspace, Hilbert projections are linear, self-adjoint and contractive).

[A6]

If $R$ is trace class and $A, B$ are bounded operators with compatible Hilbert-space domains and ranges, then $A R B$ is trace class (Trace class is a two sided Banach operator ideal).

[A7]

The rationals are in bijection with $N$ ( $Q$ is countably infinite), and there is a bijection $π : N^{2} \to N$ ( $N \times N \approx N$ ). Define $c_{0} (()) = 0$ and $c_{k + 1} (a_{0}, \dots, a_{k}) = π (a_{0}, c_{k} (a_{1}, \dots, a_{k}))$ . Then $c (a_{0}, \dots, a_{k - 1}) = π (k, c_{k} (a_{0}, \dots, a_{k - 1}))$ is injective on all finite sequences: inverse pairing recovers the length and then every entry.

[A8]

The rationals are dense in $R$ (The rationals embed densely in the reals). Each complex number has unique real and imaginary coordinates $a + b i$ and modulus $\sqrt{a^{2} + b^{2}}$ (Real and imaginary parts, complex conjugation, and modulus); hence $Q + i Q$ is dense in $C$ .

[A9]

A space is separable when it has an at most countable dense subset (Separability: the existence of an at most countable dense subset).

[A10]

In this library, countable means at most countable (Finite, countably infinite, countable, uncountable); $N \times N$ is bijective with $N$ ( $N \times N \approx N$ ). A nonempty set is at most countable exactly when there is a surjection from $N$ onto it (A nonempty set is at most countable iff it is a surjective image of $N$ ).

[A11]

Every nonzero spectral value of a compact operator is an eigenvalue with finite-dimensional generalized eigenspace, and $m_{a l g} (λ; T)$ is the dimension of that stabilized generalized eigenspace (Trace class operator, Riesz schauder spectrum of a compact operator, Algebraic multiplicity of a nonzero compact-operator eigenvalue).

[A12]

On a separable complex Hilbert space, the local determinant construction is entire and has $D_{S} (0) = 1$ . For finite-rank $F$ and finite-dimensional $F$ -invariant $E$ containing $ran F$ , it gives $D_{F} (z) = \det_{E} (I_{E} + z (F ∣_{E}))$ , including $\det_{{0}} = 1$ (Local separable trace-class determinant construction).

[A13]

For a trace-class operator on a separable complex Hilbert space, the local determinant equals the locally uniform product of the nonzero eigenvalues, repeated by algebraic multiplicity; the empty product is $1$ (Spectral product from traces of powers).

[A14]

The finite-dimensional operator determinant is the determinant of a matrix in an ordered basis (and is $1$ on the zero space); its value is basis-independent (The determinant of an endomorphism of a finite-dimensional vector space: its matrix determinant in an ordered basis in positive dimension, and $1$ on the zero space, The determinant of a linear operator is independent of the chosen ordered basis).

[A15]

The matrix determinant is given by the finite signed permutation sum (Leibniz formula) (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix).

[A16]

Cauchy--Schwarz gives $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ for vectors in a complex inner-product space (Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs).

[A17]

The induced inner-product norm satisfies the triangle inequality $∥ u + v ∥ \leq ∥ u ∥ + ∥ v ∥$ (The induced length is a norm).

[A18]

The Hilbert norm is complete, so $H$ is Banach; every absolutely convergent series in a Banach space converges (Hilbert space, Series criterion for Banach spaces).

[A19]

The linear span of a set is exactly its finite linear combinations, including the empty sum ( $span (S)$ is exactly the set of linear combinations of finite lists of elements of $S$ , and $span (\emptyset) = {0_{V}}$ ).

[A20]

In a metric space, $x$ is in the closure of $A$ exactly when every positive-radius ball around $x$ meets $A$ (Interior, closure, boundary, limit point, isolated point and dense subset of a metric space).

[A21]

The induced inner-product norm is homogeneous: $∥ λ v ∥ = ∣ λ ∣ ∥ v ∥$ (The induced length is a norm).

Proof

technique · direct

1.1A1A2

By [A1] and the nuclear characterization [A2], a nuclear representation exists. Fix any such representation and let $M$ be the closed complex linear span in the statement. The argument below applies to every representation; this initial choice only constructs one support.

2.1A7A10A19A20step 1.1construct

Let $w_{2 j - 2} = u_{j}$ and $w_{2 j - 1} = v_{j}$ . Let $Q + i Q$ denote the Gaussian rationals. The finite sums $\sum_{k < r} c_{k} w_{n_{k}}$ with $c_{k} \in Q + i Q$ and $n_{k} \in N$ form a subset $D$ of $M$ . This set is at most countable: fix a bijection $η : N \to Q$ from [A7] and a bijection $π : N \times N \to N$ from [A10]. Encode each tuple $(n_{k}, a_{k}, b_{k}) \in N^{3}$ by $π (n_{k}, π (a_{k}, b_{k}))$ , where $c_{k} = η (a_{k}) + i η (b_{k})$ . The injective finite-sequence code in [A7] therefore codes every finite list of such tuples by a natural number. Decode each valid sequence code as the corresponding sum and send a natural number that is not a valid code to $0$ . This defines a surjection $N \to D$ ; $D$ is nonempty because it contains the empty sum $0$ . Thus [A10] makes $D$ at most countable.

2.2A2A3A4A5A16A18A19A20A21step 1.1

Write $T_{n} x = \sum_{j \leq n} ⟨ x, u_{j} ⟩ v_{j}$ for the nuclear partial sums. For each $x \in H$ , $T_{n} x \in M$ , and $T_{n} x \to T x$ by [A2]; operator-norm convergence implies pointwise convergence by the bound in [A4]. Since $M$ is closed, $T x \in M$ . For each $y \in H$ , the series $w_{y} : = \sum_{j \geq 1} ⟨ y, v_{j} ⟩ u_{j}$ converges absolutely in $H$ by [A16] and therefore converges in $H$ by [A18], because $H$ is Banach. Its partial sums lie in $M$ , so $w_{y} \in M$ . Conjugate-linearity in the second argument, the adjoint identity [A3], and inner-product continuity from [A16] give $⟨ x, w_{y} ⟩ = \lim_{n} \sum_{j \leq n} ⟨ x, u_{j} ⟩ ⟨ v_{j}, y ⟩ = \lim_{n} ⟨ T_{n} x, y ⟩ = ⟨ T x, y ⟩ .$ Uniqueness of the adjoint in [A3] yields $T^{*} y = w_{y}$ , so $T^{*} (H) \subseteq M$ . If $x \in M^{⊥}$ , then $⟨ x, u_{j} ⟩ = ⟨ x, v_{j} ⟩ = 0$ for every $j$ , so the nuclear series for both $T x$ and $T^{*} x$ vanish. Consequently $M$ and $M^{⊥}$ are invariant under both $T$ and $T^{*}$ ; therefore $M$ reduces $T$ . The decomposition [A5] now gives $T = S \oplus 0$ on $H = M \oplus M^{⊥}$ , where $S = T ∣_{M}$ .

3.1A8A9A17A19A20A21step 2.1construct

The set $D$ is dense in $M$ . Given $x \in M$ and $ε > 0$ , [A20] gives a point $y$ of the span of the listed vectors with $∥ x - y ∥ < ε / 2$ ; by [A19], write it as a finite complex linear combination $y = \sum_{k < r} c_{k} w_{n_{k}}$ . By density of $Q$ in $R$ and the coordinate/modulus formula in [A8], each $c_{k}$ can be approximated by $q_{k} \in Q + i Q$ closely enough that $\sum_{k < r} ∣ c_{k} - q_{k} ∣ ∥ w_{n_{k}} ∥ < ε / 2$ ; if a listed vector is zero its summand is already zero. Then $d = \sum_{k < r} q_{k} w_{n_{k}} \in D$ and $∥ x - d ∥ \leq ∥ x - y ∥ + \sum_{k < r} ∣ c_{k} - q_{k} ∣ ∥ w_{n_{k}} ∥ < ε .$ Consequently $D$ is a countable dense subset of $M$ , so $M$ is separable by [A9]. This also covers an empty sequence, a finite list, and $M = {0}$ .

3.2A3A5A6step 2.2

More generally, call a closed separable subspace $N \subseteq H$ a support for $T$ when $T (H) \subseteq N$ and $T (N^{⊥}) = {0}$ . By [A5], $H = N \oplus N^{⊥}$ ; hence $T = S_{N} \oplus 0$ for $S_{N} : = T ∣_{N}$ . The adjoint identity [A3] gives $T^{*} = S_{N}^{*} \oplus 0$ , so $N$ is reducing in the standard sense (invariant under both $T$ and $T^{*}$ ). Let $ι_{N} : N ↪ H$ be inclusion and $P_{N}$ the projection of [A5]. Then $S_{N} = P_{N} T ι_{N}$ : on $N$ , $T$ takes values in $N$ and $P_{N}$ is the identity. The inclusion is bounded with its inherited norm, and [A5] makes $P_{N}$ bounded. Thus [A6] shows that $S_{N}$ is trace class. This applies to the representation support $M$ of step 2.2 and to every support used below.

4.1A9A10A17A20step 3.2givenconstruct

Let $N_{1}, N_{2}$ be two reducing supports. If either is zero, the closure of their sum is the other support and is separable. Otherwise choose nonempty dense sets $X_{i} \subseteq N_{i}$ by [A9]. They are countable, so by the surjection criterion in [A10] fix surjections $s_{i} : N \to X_{i}$ . Using the bijection $π$ from [A10] to reindex pairs, the map $(m, n) \mapsto s_{1} (m) + s_{2} (n)$ has countable image $X_{1} + X_{2} = {x_{1} + x_{2} : x_{i} \in X_{i}}$ . It is dense in $N_{1} + N_{2}$ : for $x_{i} \in N_{i}$ and any $ε > 0$ , choose $x_{i}^{'} \in X_{i}$ with $∥ x_{i} - x_{i}^{'} ∥ < ε / 2$ , so $∥ (x_{1} + x_{2}) - (x_{1}^{'} + x_{2}^{'}) ∥ < ε$ . Its closure $L : = \overline{N_{1} + N_{2}}$ is therefore separable. Also $T (H) \subseteq N_{1} \subseteq L$ and $L^{⊥} \subseteq N_{1}^{⊥}$ , so $T (L^{⊥}) = {0}$ . Hence $L$ is a reducing support.

4.2A11step 2.2step 3.2

For any reducing support $N$ , the decomposition $H = N \oplus N^{⊥}$ gives, for every $λ \neq 0$ and integer $k \geq 1$ , $(T - λ I)^{k} = (S_{N} - λ I_{N})^{k} \oplus (- λ)^{k} I_{N^{⊥}} .$ Since $(- λ)^{k} \neq 0$ , $\ker (T - λ I)^{k} = \ker (S_{N} - λ I_{N})^{k} \oplus {0} .$ Thus $T$ and $S_{N}$ have the same nonzero eigenvalues and the same stabilized generalized eigenspaces and algebraic multiplicities. Both are trace class and therefore compact; their nonzero spectral values are eigenvalues by [A11], and the multiplicity is the dimension of the stabilized kernel.

5.1A13step 3.2step 4.1step 4.2

Let $N_{1}, N_{2}$ be arbitrary reducing supports and let $L = \overline{N_{1} + N_{2}}$ from step 4.1. Each of $S_{N_{1}}$ , $S_{N_{2}}$ and $S_{L}$ is trace class by step 3.2 and acts on a separable Hilbert space. Step 4.2 gives the same nonzero eigenvalue list, including algebraic multiplicity, for all three restrictions. The local product theorem [A13] therefore gives $D_{S_{N_{1}}} (z) = D_{S_{L}} (z) = D_{S_{N_{2}}} (z) (z \in C) .$ Taking $N_{1}, N_{2}$ to be supports arising from any two nuclear representations proves representation independence as well as independence from every separable reducing support.

6.1A12A13step 2.2step 4.2step 5.1

Define $D_{H} (I + z T) : = D_{S_{M}} (z)$ using any support $M$ . Step 5.1 makes this well-defined. By [A12], it is entire and equals $1$ at $z = 0$ . By [A13], $D_{S_{M}} (z) = \prod_{j} (1 + z λ_{j} (S_{M}))$ locally uniformly. Step 4.2 identifies the nonzero eigenvalues and their algebraic multiplicities with those of $T$ , so this is the asserted locally uniform product for $T$ . If the eigenvalue list is empty, the product is $1$ ; finite lists are finite products, and the formula also holds for $H = {0}$ and $T = 0$ .

7.1A12step 2.2step 6.1

Suppose $T$ has finite rank and write $R = ran T$ . Then $R \subseteq M$ by step 2.2, $R$ is finite dimensional, and $T (R) \subseteq R$ . Apply the finite-rank clause of [A12] to $S_{M}$ and the invariant subspace $R \subseteq M$ to obtain $D_{H} (I + z T) = D_{S_{M}} (z) = \det_{R} (I_{R} + z (T ∣_{R})) .$ If $R = {0}$ , this is $1 = 1$ by [A12] and the zero-dimensional determinant convention.

8.1A14A15step 7.1construct

Let $E \subseteq H$ be any finite-dimensional subspace containing $R$ . It is $T$ -invariant because $T (E) \subseteq R \subseteq E$ . For $R \neq {0}$ , extend a basis of $R$ to a basis of $E$ . Relative to the resulting decomposition $E = R \oplus F$ , the matrix of $T ∣_{E}$ has block form $(\begin{array}{cc} A & B \\ 0 & 0 \end{array}),$ where $A$ is the matrix of $T ∣_{R}$ . Thus the matrix of $I_{E} + z (T ∣_{E})$ is $(\begin{array}{cc} I_{R} + z A & z B \\ 0 & I_{F} \end{array}) .$ In any nonzero term of the Leibniz formula [A15], each of the $\dim R$ columns from $R$ must use an $R$ row because the lower-left block is zero. Since there are exactly $\dim R$ such rows, they are all occupied, so no $F$ column can use an $R$ row. Each $F$ column must then use its matching identity entry in the $I_{F}$ block, and the remaining permutation sum is the Leibniz determinant of $I_{R} + z A$ . Hence $\det_{E} (I_{E} + z (T ∣_{E})) = \det_{R} (I_{R} + z (T ∣_{R})),$ which with step 7.1 proves the formula for every such $E$ . When $R = 0$ , both operators are identities and both determinants are $1$ . Basis independence of these operator determinants is [A14].

9.1

At $z = 0$ , [A12] gives determinant one and the finite-dimensional formula is the determinant of the identity. The empty nonzero-eigenvalue list has empty product one by step 6.1; a zero operator and a zero-dimensional $H$ are included there. A one-dimensional nonzero range is covered by step 7.1, where the finite-dimensional determinant is the corresponding single linear factor. The proof uses AC exactly as [A1] states: it supplies the Countable Choice needed to obtain the nuclear representation and the Hilbert projection, and AC-qualified spectral multiplicities; the explicit countable coding and the later comparison of supports make no further selections. The conclusion is a direct equality, not a biconditional. [A1, A11, A12, step 2.1, step 4.2, step 6.1, step 7.1] \qed

DefinitionDefinition: AI-adaptedProof: AI-adaptedaudited 2026-09-22Open item page →

Fredholm determinant of a trace-class operator

Definition

Assume the Axiom of Choice (The Axiom of Choice). Let $H$ be a complex Hilbert space and let $T \in S_{1} (H)$ (Trace class operator). Choose a nuclear representation $T x = \sum_{j \geq 1} ⟨ x, u_{j} ⟩ v_{j}, \sum_{j \geq 1} ∥ u_{j} ∥ ∥ v_{j} ∥ < \infty,$ and put $M = \overset{}{span} {u_{j}, v_{j} : j \geq 1}$ and $S = T ∣_{M}$ . The Fredholm determinant of $I + z T$ is

\underset{H}{\det} (I + z T) : = D_{S} (z),

where $D_{S}$ is the locally constructed separable determinant of Local separable trace-class determinant construction, identified across supports by Arbitrary-Hilbert Fredholm determinant from a separable reducing support. If $H = {0}$ , this definition gives $\det_{H} (I + z T) = 1$ .

The well-definedness argument below proves that this restriction preserves the trace, trace norm, nonzero singular values, and nonzero generalized-eigenvalue data, and that the resulting determinant is independent of the nuclear representation and separable reducing support.

Well-definedness

Nuclear representations exist by Nuclear series characterizes trace norm. Finite rational-complex linear combinations of the vectors $u_{j}, v_{j}$ form a countable dense subset of $M$ , so $M$ is separable. If $x \in M^{⊥}$ , every coefficient in the nuclear series vanishes and $T x = 0$ ; if $x \in M$ , every partial sum and hence $T x$ lies in the closed space $M$ . Thus, using Orthogonal decomposition by a closed subspace,

H = M \oplus M^{⊥}, T = S \oplus 0.

The restriction $S$ is bounded and compact. Indeed, a bounded sequence in $M$ is bounded in $H$ . Since $T$ is compact, its images have a norm-convergent subsequence by Sequential characterization of compact operators; the limit lies in the closed space $M$ . The converse direction of that same characterization makes $S : M \to M$ compact. Full AC supplies its DC hypothesis. The same nuclear series, now regarded inside $M$ , therefore makes $S$ trace class by Nuclear series characterizes trace norm. The nuclear trace formula in Trace is absolutely convergent and basis independent gives ${tr}_{M} (S) = {tr}_{H} (T)$ .

The block identity gives $T^{*} T = S^{*} S \oplus 0$ . Hence $∣ S ∣ \oplus 0$ is a compact positive square root of $T^{*} T$ , and uniqueness in Positive square root of a compact positive operator gives $∣ T ∣ = ∣ S ∣ \oplus 0$ . Therefore $S$ and $T$ have the same nonzero singular values, with multiplicities, and $∥ S ∥_{1} = ∥ T ∥_{1}$ .

For every $λ \neq 0$ and $r \geq 1$ ,

(T - λ I)^{r} = (S - λ I_{M})^{r} \oplus (- λ)^{r} I_{M^{⊥}} .

Consequently all generalized $λ$ -eigenvectors lie in $M$ , and $S$ and $T$ have identical nonzero eigenvalues, generalized kernels, stabilization indices, and algebraic multiplicities. The locally proved product formula and support comparison in Arbitrary-Hilbert Fredholm determinant from a separable reducing support therefore make $D_{S}$ independent of the chosen nuclear representation and of every separable closed reducing support on whose orthogonal complement $T$ is zero. No arbitrary invariant subspace is asserted to reduce $T$ .

PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-09-22Open item page →

Fredholm determinant properties for trace-class operators

Statement

Assume the Axiom of Choice. Let $H$ be a complex Hilbert space and $T \in S_{1} (H)$ . The function $D_{T} (z) = \det_{H} (I + z T)$ is entire and, locally uniformly in $z$ ,

D_{T} (z) = \prod_{j} (1 + z λ_{j} (T)),

where all nonzero eigenvalues are listed with their finite algebraic multiplicities, and $\sum_{j} ∣ λ_{j} (T) ∣ \leq ∥ T ∥_{1}$ . It satisfies

D_{T} (0) = 1, D_{T}^{'} (0) = {tr}_{H} (T),

∣ D_{T} (z) ∣ \leq \prod_{j} (1 + ∣ z ∣ s_{j} (T)) \leq e^{∣ z ∣ ∥ T ∥_{1}},

and for every $ε > 0$ there is $C_{ε}$ such that $∣ D_{T} (z) ∣ \leq C_{ε} e^{ε ∣ z ∣}$ . For trace-class $A, B$ , $∣ D_{A} (z) - D_{B} (z) ∣ \leq ∣ z ∣ ∥ A - B ∥_{1} e^{1 + ∣ z ∣ ∥ A ∥_{1} + ∣ z ∣ ∥ B ∥_{1}},$ and

\underset{H}{\det} (I + A + B + A B) = \underset{H}{\det} (I + A) \underset{H}{\det} (I + B) .

Moreover $D_{T} (z) = 0$ exactly when $I + z T$ is not boundedly invertible, and the zero at $- 1 / λ$ has the algebraic multiplicity of $λ \neq 0$ .

If finite-rank $T_{n}$ converge to $T$ in trace norm, their ordinary finite-dimensional determinants converge to $D_{T}$ locally uniformly. Where $I + z T$ is invertible,

D_{T}^{'} (z) = D_{T} (z) {tr}_{H} (T (I + z T)^{- 1}) .

All assertions include $H = {0}$ , finite eigenvalue lists and the empty list.

Facts & Assumptions

Given: The Axiom of Choice, a complex Hilbert space $H$ , and the displayed trace-class operators.

[F1]

The determinant is defined through a separable reducing support; its value is independent of the support, entire and normalized, and equals the locally uniform product over the nonzero eigenvalues with algebraic multiplicity. Finite-rank values are ordinary finite-dimensional determinants (Fredholm determinant of a trace-class operator, Arbitrary-Hilbert Fredholm determinant from a separable reducing support).

[F2]

On a separable complex Hilbert space the local determinant satisfies $D_{S}^{'} (0) = tr (S)$ (Local separable trace-class determinant construction).

[F3]

On a separable complex Hilbert space the eigenvalue absolute sum is at most the trace norm, with algebraic multiplicities (Weyl product and sum inequalities for compact operators).

[F4]

On a separable complex Hilbert space the local determinant satisfies the singular-value product and exponential bounds, minimal exponential type, the displayed trace-norm continuity estimate, multiplicativity at $z = 1$ , and locally uniform convergence of finite-rank determinants in trace norm (Trace-norm continuity, growth and multiplicativity of the local determinant).

[F5]

On a separable complex Hilbert space, the local determinant vanishes exactly when $I + z S$ is not boundedly invertible, and its zero at $- 1 / λ$ has order $m_{a l g} (λ; S)$ (Zeros of the local Fredholm determinant).

[F6]

On a separable complex Hilbert space, at every invertibility point, $D_{S}^{'} (z) = D_{S} (z) tr (S (I + z S)^{- 1})$ (Logarithmic derivative of the local Fredholm determinant).

[F7]

Trace-class operators form a linear two-sided ideal, their trace norm is a norm, and singular values are the positive eigenvalues of $∣ T ∣$ (Trace class is a two sided Banach operator ideal, Absolute value and singular values of a compact operator).

[F8]

The trace is basis-independent and agrees with every nuclear trace sum (Trace is absolutely convergent and basis independent).

Proof

technique · direct

1.1F1F7F8given

Choose a nuclear support $M$ from [F1] and write $H = M \oplus M^{⊥}$ and $T = S \oplus 0$ . The nuclear trace formula gives ${tr}_{H} (T) = {tr}_{M} (S)$ : the same nuclear vectors lie in $M$ , so their scalar inner products are unchanged. The block identity $T^{*} T = S^{*} S \oplus 0$ and uniqueness of the compact positive square root, as established in Fredholm determinant of a trace-class operator, give $∣ T ∣ = ∣ S ∣ \oplus 0$ . Thus $T$ and $S$ have the same nonzero singular values, including multiplicity, and $∥ T ∥_{1} = ∥ S ∥_{1}$ . For each $λ \neq 0$ , $(T - λ I)^{r} = (S - λ I_{M})^{r} \oplus (- λ)^{r} I_{M^{⊥}}$ ; hence their nonzero eigenvalues and algebraic multiplicities agree.

2.1F1F2F3F4step 1.1

By [F1], $D_{T} = D_{S}$ is entire, normalized, and has the stated locally uniform spectral product. Applying [F3] to $S$ and step 1.1 gives $\sum_{j} ∣ λ_{j} (T) ∣ \leq ∥ T ∥_{1}$ . Applying [F2] gives $D_{T}^{'} (0) = D_{S}^{'} (0) = {tr}_{M} (S) = {tr}_{H} (T)$ . The singular-value product, exponential bound and minimal exponential type in [F4] transfer from $S$ using the same singular-value list and trace norm. This also covers finite and empty lists.

2.2F1F5F6F8step 1.1

For each $z$ , $I + z T = (I_{M} + z S) \oplus I_{M^{⊥}}$ . It has a bounded inverse exactly when $I_{M} + z S$ does, because the inverse of a block diagonal operator is the block inverse and restriction of a bounded inverse to the reducing summand is bounded. The generalized kernels in step 1.1 preserve algebraic multiplicity. Hence [F5] gives both directions of the stated zero criterion and the exact zero order at $- 1 / λ$ . If $I + z T$ is invertible, its inverse is $(I_{M} + z S)^{- 1} \oplus I_{M^{⊥}}$ ; consequently $T (I + z T)^{- 1} = S (I_{M} + z S)^{- 1} \oplus 0$ . The same nuclear trace formula as step 1.1 equates these traces, so [F6] gives the displayed logarithmic derivative.

2.3F1F4F7step 1.1

For trace-class $A, B$ on $H$ , take nuclear representations for both and let $N$ be the closed span of all their input and output vectors. The finite union of the two countable vector lists has a countable dense set of finite Gaussian-rational combinations; the support proof in [F1] shows $N$ is separable and reduces both operators, with $A = A_{N} \oplus 0$ and $B = B_{N} \oplus 0$ . By [F7], $C : = A + B + A B$ is trace class and $C = (A_{N} + B_{N} + A_{N} B_{N}) \oplus 0$ ; the same $N$ supports $A - B$ . The block singular-value argument of step 1.1 gives $∥ A - B ∥_{1} = ∥ A_{N} - B_{N} ∥_{1}$ and $∥ A ∥_{1} = ∥ A_{N} ∥_{1}$ , $∥ B ∥_{1} = ∥ B_{N} ∥_{1}$ . Apply the separable continuity estimate and multiplicativity in [F4] on $N$ , and use support independence in [F1] for all three determinants. These are exactly the displayed arbitrary-space formulas, including the same numerical exponential constant.

2.4F1F4step 1.1

Suppose finite-rank $T_{n} \to T$ in trace norm. AC chooses nuclear representations for $T$ and the countable family $(T_{n})$ ; taking the closed span of every input and output vector gives one separable reducing support $N$ for all of them. Their restrictions $S_{n}, S$ obey $∥ S_{n} - S ∥_{1} = ∥ T_{n} - T ∥_{1} \to 0$ by the block singular-value argument of step 1.1. Apply the locally uniform finite-rank approximation in [F4] on $N$ . By [F1], $D_{S_{n}} = D_{T_{n}}$ and each is the ordinary determinant on any finite-dimensional subspace containing $ran T_{n}$ ; the same support lemma shows independence of that subspace. Therefore those ordinary determinants converge locally uniformly to $D_{S} = D_{T}$ .

3.1F1F2F4F5F6step 2.1step 2.2step 2.4∎

If $H = {0}$ or $T = 0$ , [F1] gives $D_{T} \equiv 1$ , its derivative and trace are zero, and the product and singular-value lists are empty. For $z = 0$ , normalization holds, and the logarithmic-derivative formula follows from step 2.1. A finite-rank operator is covered by [F1] and step 2.4. Full AC supplies the separable-support and AC-qualified spectral suppliers and permits the countable family of nuclear representations in step 2.4; its Countable Choice consequence supplies [F2], [F4] and [F6]. Both directions of the zero criterion were established in step 2.2.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-22Open item page →

Lidskii trace formula for trace-class operators

Statement

Assume the Axiom of Choice. Let $H$ be any complex Hilbert space, including $H = {0}$ , and let $T \in S_{1} (H)$ . List all nonzero eigenvalues $(λ_{j} (T))$ with their finite algebraic multiplicities, where the multiplicity of $λ \neq 0$ is the dimension of the stabilized generalized kernel $⋃_{r \geq 1} \ker (T - λ I)^{r}$ . Then $\sum_{j} ∣ λ_{j} (T) ∣ \leq ∥ T ∥_{1}, {tr}_{H} (T) = \sum_{j} λ_{j} (T) .$ The list is finite or countable and may be empty. No normality, self-adjointness, positivity, or separability of $H$ is assumed.

Facts & Assumptions

Given: The Axiom of Choice, a complex Hilbert space $H$ , and a trace-class operator $T$ .

[F1]

The determinant definition preserves the nonzero generalized-eigenvalue data under separable-support reduction (Fredholm determinant of a trace-class operator).

[F2]

The determinant properties give absolute eigenvalue summability, $D_{T} (z) = \prod_{j} (1 + z λ_{j} (T))$ locally uniformly, and $D_{T}^{'} (0) = {tr}_{H} (T)$ (Fredholm determinant properties for trace-class operators).

Proof

technique · direct

1.1F1F2givenalgebra

By [F1] and [F2], the eigenvalue list has the stated algebraic multiplicities and $L : = \sum_{j} ∣ λ_{j} (T) ∣ \leq ∥ T ∥_{1}$ . For a finite initial product $P_{N} (z) = \prod_{j \leq N} (1 + z λ_{j})$ , expansion and the ordered-tuple bound for elementary symmetric sums give $∣ P_{N} (z) - 1 - z \sum_{j \leq N} λ_{j} ∣ \leq \sum_{k = 2}^{N} (∣ z ∣ L)^{k} / k! \leq (∣ z ∣ L)^{2} e^{∣ z ∣ L} / 2$ . Indeed, every unordered product of $k$ distinct absolute eigenvalues occurs $k!$ times among the ordered $k$ -tuples contributing to $L^{k}$ .

2.1F2step 1.1algebra∎

Let $N \to \infty$ . The local product convergence and absolute convergence of $\sum_{j} λ_{j}$ from [F2] preserve the bound in step 1.1, so $\lim_{z \to 0} (D_{T} (z) - 1) / z = \sum_{j} λ_{j} (T)$ . The left side is $D_{T}^{'} (0) = {tr}_{H} (T)$ by [F2]. The same argument applies to finite and empty lists, with the empty sum equal to $0$ and the empty product equal to $1$ .

5 · Examples, counterexamples and false statements

None yet.

Fredholm Determinants and the Lidskii Trace Formula

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

Algebraic multiplicity of a nonzero compact-operator eigenvalue

Definition

Facts & Assumptions

Proof

Finite-rank orthogonal compressions converge in trace norm

Statement

Facts & Assumptions

Proof

Hilbert exterior powers and induced operators

Definition

Facts & Assumptions

Proof

Trace-norm bound for exterior powers of trace-class operators

Statement

Facts & Assumptions

Proof

Weyl product and sum inequalities for compact operators

Statement

Facts & Assumptions

Proof

Diagonal trace-class operators on ℓ2(N,C)ℓ2(N,C)

Statement

Facts & Assumptions

Proof

Local separable trace-class determinant construction

Statement

Facts & Assumptions

Proof

Trace-norm continuity, growth and multiplicativity of the local determinant

Statement

Facts & Assumptions

Proof

Logarithmic derivative of the local Fredholm determinant

Statement

Facts & Assumptions

Proof

Zeros of the local Fredholm determinant

Statement

Facts & Assumptions

Proof

A quasinilpotent trace-class operator has zero trace

Statement

Facts & Assumptions

Proof

Trace decomposition through generalized eigenspaces and the invariant quotient

Statement

Facts & Assumptions

Proof

Spectral product from traces of powers

Statement

Facts & Assumptions

Proof

Arbitrary-Hilbert Fredholm determinant from a separable reducing support

Statement

Facts & Assumptions

Proof

Fredholm determinant of a trace-class operator

Definition

Well-definedness

Fredholm determinant properties for trace-class operators

Statement

Facts & Assumptions

Proof

Lidskii trace formula for trace-class operators

Statement

Facts & Assumptions

Proof

5 · Examples, counterexamples and false statements

Sources

Diagonal trace-class operators on $ℓ^{2} (N, C)$