Physlib

PhyslibAlpha.AlgebraicFramework.HilbertSpace.TraceClass.GeneralIdeal

The unconditional trace, for arbitrary (not necessarily self-adjoint) trace-class operators

Ported from `unbounded-alpha-public`'s `TraceClass/GeneralIdeal.lean`. `Basic.lean` already proves basis-independence of the trace for positive and self-adjoint trace-class operators without polar decomposition; this file crosses the general non-self-adjoint boundary: `√|T|` is Hilbert–Schmidt, so `T = polarFactor T * √|T| * √|T|` factors `T`'s diagonal series as a Hilbert–Schmidt product, and `HilbertSchmidt.tsum_diagonal_mul_eq_tsum_diagonal_swap` (the Fubini swap on that product) upgrades this to full basis-independence of `trace T` for *every* trace-class `T`.

5 declarations

theorem

∣T∣\sqrt{|T|} is Hilbert-Schmidt for any trace-class operator TT

Let HH be a complex Hilbert space and T:H→HT: H \to H be a bounded linear operator. If TT is a trace-class operator, then the square root of its absolute value, ∣T∣\sqrt{|T|}, is a Hilbert-Schmidt operator, where ∣T∣=T∗T|T| = \sqrt{T^* T}.

theorem

Summability of the diagonal series for trace-class operators

Let HH be a complex Hilbert space and T:H→HT: H \to H be a trace-class operator. For any Hilbert basis {ei}i∈I\{e_i\}_{i \in I} of HH, the series of diagonal terms ∑i∈I⟨ei,Tei⟩\sum_{i \in I} \langle e_i, T e_i \rangle is summable.

theorem

Basis-Independence of the Diagonal Sum for Trace-Class Operators

Let HH be a complex Hilbert space and T:H→HT: H \to H be a trace-class operator. For any two Hilbert bases {bi}i∈I\{b_i\}_{i \in I} and {cj}j∈J\{c_j\}_{j \in J} of HH, the sum of the diagonal entries with respect to each basis is equal: ∑i∈I⟨bi,Tbi⟩=∑j∈J⟨cj,Tcj⟩ \sum_{i \in I} \langle b_i, T b_i \rangle = \sum_{j \in J} \langle c_j, T c_j \rangle

theorem

Tr T=∑i∈I⟨bi,Tbi⟩\text{Tr } T = \sum_{i \in I} \langle b_i, T b_i \rangle for any Hilbert Basis

Let HH be a complex Hilbert space and T:H→HT: H \to H be a trace-class operator. For any Hilbert basis {bi}i∈I\{b_i\}_{i \in I} of HH, the trace of TT, denoted Tr T\text{Tr } T, is equal to the sum of the diagonal inner products: Tr T=∑i∈I⟨bi,Tbi⟩ \text{Tr } T = \sum_{i \in I} \langle b_i, T b_i \rangle

theorem

Tr T=∑i⟨bi,Tbi⟩\text{Tr } T = \sum_i \langle b_i, T b_i \rangle for any Hilbert basis {bi}\{b_i\} of a trace-class operator TT

Let HH be a complex Hilbert space and T:H→HT: H \to H be a trace-class bounded linear operator. For any Hilbert basis {bi}i∈I\{b_i\}_{i \in I} of HH, the trace of TT is equal to the sum of the diagonal inner products: Tr T=∑i∈I⟨bi,Tbi⟩\text{Tr } T = \sum_{i \in I} \langle b_i, T b_i \rangle This evaluation of the trace is independent of the choice of Hilbert basis and does not require TT to be self-adjoint or positive.