Physlib

PhyslibAlpha.AlgebraicFramework.HilbertSpace.TraceClass.TraceAlgebra

Elementary algebra of the unconditional trace

Ported from `unbounded-alpha-public`'s `TraceClass/TraceAlgebra.lean` (only the three facts actually needed downstream by the concrete `B(H)` trace-pairing construction: `trace_smul`, `trace_add`, and the bounded-factor cyclicity `trace_mul_cycle`; the source file's Hilbert–Schmidt cycle and `trace_star`/`traceNorm_add_le_via_diagonal` facts are not needed here and are not ported — this repo's `IdealNorm.lean` already supplies `traceNorm_add_le` by a different route).

The witness proof in `IsTraceClass` is proof-irrelevant, while the diagonal trace itself is now known to be basis independent (`GeneralIdeal.lean`'s `trace_eq_of_hilbertBasis`). This file records the linear scalar law and cyclicity in a form the trace-pairing construction can use without reopening the witness basis.

Additivity and cyclicity

3 declarations

theorem

Scalar Homogeneity of the Trace: Tr(cT)=cTr(T)\text{Tr}(c T) = c \text{Tr}(T)

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 for any complex scalar c∈Cc \in \mathbb{C}, the trace of the scaled operator cTc T is equal to cc multiplied by the trace of TT: Tr(cT)=cTr(T)\text{Tr}(c T) = c \text{Tr}(T) Note that here Tr\text{Tr} denotes the trace of a trace-class operator, defined as the sum of diagonal inner products ∑i∈I⟨ei,Tei⟩\sum_{i \in I} \langle e_i, T e_i \rangle for a Hilbert basis {ei}i∈I\{e_i\}_{i \in I}.

theorem

Additivity of the trace: Tr(T+T′)=Tr T+Tr T′\text{Tr}(T + T') = \text{Tr } T + \text{Tr } T'

Let HH be a complex Hilbert space and let TT and T′T' be bounded linear operators on HH that are trace-class. Then the trace of their sum is equal to the sum of their individual traces: Tr(T+T′)=Tr T+Tr T′ \text{Tr}(T + T') = \text{Tr } T + \text{Tr } T'

theorem

Tr(AT)=Tr(TA)\text{Tr}(AT) = \text{Tr}(TA) for bounded AA and trace-class TT

Let HH be a complex Hilbert space, and let AA and TT be bounded linear operators on HH. If TT is a trace-class operator, then the trace of their products satisfies the cyclic property Tr(AT)=Tr(TA). \text{Tr}(AT) = \text{Tr}(TA).