Alphabeta Math
DefinitionDefinition: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 2026-09-22
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.

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∈S1(H) (Trace class operator). Choose a nuclear representation Tx=∑j≥1⟨x,uj⟩vj,∑j≥1∥uj∥ ∥vj∥<∞, and put M=span⁡‾{uj,vj:j≥1} and S=T∣M. The Fredholm determinant of I+zT is

det⁡H(I+zT):=DS(z),

where DS 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+zT)=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 uj,vj form a countable dense subset of M, so M is separable. If x∈M⊥, every coefficient in the nuclear series vanishes and Tx=0; if x∈M, every partial sum and hence Tx lies in the closed space M. Thus, using Orthogonal decomposition by a closed subspace,

H=M⊕M⊥,T=S⊕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→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⊕0. Hence ∣S∣⊕0 is a compact positive square root of T∗T, and uniqueness in Positive square root of a compact positive operator gives ∣T∣=∣S∣⊕0. Therefore S and T have the same nonzero singular values, with multiplicities, and ∥S∥1=∥T∥1.

For every λ≠0 and r≥1,

(T−λI)r=(S−λIM)r⊕(−λ)rIM⊥.

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 DS 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.

Depends on

Used by

Dependency tree · two levels

102 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