LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30

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.

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

Depends on

Used by

Dependency tree · two levels

193 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

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) (standard reference, not scraped)
van Neerven, Functional Analysis, §14.5.a, Lemmas 14.35–14.39, printed pp. 585–587 (PDF pp. 597–599) (standard reference, not scraped)
Dyatlov–Zworski, Mathematical Theory of Scattering Resonances, Appendix B §§B.5.2–B.5.3, Propositions B.27 and B.29, PDF pp. 509–511 (standard reference, not scraped)