PropositionStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-22‡ rests on unproved material

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.

‡ Rests on 1 statement not proved in this library. Every dependency marked ‡ below is recorded with a citation but is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Fredholm determinant properties for trace-class operators

Statement

proof uses external results not yet established in this library

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 arbitrary-space determinant is well defined through a separable reducing support and preserves trace, trace norm, nonzero singular values, and nonzero generalized-eigenvalue data (Fredholm determinant of a trace-class operator).

‡ [F2]

The separable determinant has the absolute eigenvalue bound $\sum_{j} ∣ λ_{j} ∣ \leq ∥ T ∥_{1}$ , spectral product, growth, continuity, multiplicativity, derivative-at-zero and zero-multiplicity properties recorded externally (Separable trace-class determinant theorem recorded externally ‡).

[F3]

Trace-class operators form a two-sided ideal (Trace class is a two sided Banach operator ideal).

[F4]

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

Proof

technique · direct

1.1

Choose the separable reducing support from [F1]. Its restriction has the same trace, trace norm, nonzero singular values and algebraic eigenvalue data as $T$ . Every single-operator assertion in the first paragraph, including the zero criterion and zero order, therefore transfers term by term from [F2]. The block identity $I + z T = (I_{M} + z S) \oplus I_{M^{⊥}}$ also proves the equivalence of bounded invertibility.

F1‡ F2F4given

1.2

For trace-class $A, B$ , take one separable closed span of nuclear vectors for both. It reduces $A$ , $B$ , $A + B + A B$ and all three operators vanish on its orthogonal complement; [F3] supplies the trace-class hypotheses. Apply the external multiplicativity and continuity formulas on this common support and then [F1] to obtain the displayed arbitrary-space formulas.

F1‡ F2F3givenalgebra

1.3

If finite-rank $T_{n} \to T$ in trace norm, full AC chooses nuclear representations for the countable family. The closed span of all their input and output vectors and those for $T$ is a common separable reducing support. The block argument in [F1] preserves the trace norm of every difference $T_{n} - T$ , so the locally uniform finite-rank limit in [F2] applies. For a finite-rank $F$ , any finite-dimensional $E \supseteq ran F$ is invariant under $I + z F$ , and enlargement adds an identity diagonal block; hence the ordinary determinant is independent of $E$ .

F1‡ F2F3givenalgebra

2.1

Fix $z_{0}$ with $I + z_{0} T$ invertible and put $B = (I + z_{0} T)^{- 1} T$ , which is trace class by [F3]. Since $I + (z_{0} + h) T = (I + z_{0} T) (I + h B)$ , step 1.2 gives $D_{T} (z_{0} + h) = D_{T} (z_{0}) D_{B} (h)$ . Steps 1.1 and [F2] give $D_{B} (h) = 1 + h {tr}_{H} (B) + o (h)$ . Dividing by $h$ and taking the limit gives $D_{T}^{'} (z_{0}) = D_{T} (z_{0}) {tr}_{H} (B)$ . The operator $T$ commutes with $I + z_{0} T$ and its inverse, so $B = T (I + z_{0} T)^{- 1}$ . The zero-space and empty-list conventions follow from [F1] and [F2].

F1‡ F2F3F4step 1.1step 1.2algebra∎

Depends on

Used by

Lidskii trace formula for trace-class operators Theorem

Dependency tree · two levels

45 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Aleksey Kostenko, Trace Ideals with Applications — Sections 3.4–3.5, printed pp. 34–45 (standard reference, not scraped)