2.3 The trace of a positive operator
Let \(H\) be a complex Hilbert space with a Hilbert basis \(e = (e_k)_{k \in \kappa }\).
(a) For every \(x \in H\) the family \(\bigl( |\langle e_k, x \rangle |^2 \bigr)_k\) has sum \(\| x\| ^2\).
(b) For every bounded operator \(T\) on \(H\),
and the family on the left is summable if and only if the one on the right is.
(c) For every bounded operator \(T\) on \(H\) and every second Hilbert basis \(e' = (e'_j)_{j \in \kappa '}\) of \(H\),
(a) Take real parts in Mathlib’s Parseval identity \(\sum _k \langle x, e_k \rangle \langle e_k, x \rangle = \langle x, x \rangle \).
(c) Expanding \(\| T e_k\| ^2\) by (a) along \(e'\) and \(\| T^* e'_j\| ^2\) along \(e\) gives the same double series \(\sum _{j,k} |\langle e'_j, T e_k \rangle |^2\) with the two summations exchanged. The rearrangement is carried out in \([0, \infty ]\), where every sum is defined and the interchange needs no hypothesis. For a self-adjoint \(T\) it says that the Hilbert–Schmidt sum does not depend on the basis.
(b) The case \(e' = e\) of (c); summability is read off the value being finite.
Part (b) is the hinge of the whole trace layer: it is what supplies the summability of \(P^{1/2} Q\) in Lemma 2.6(b), whose adjoint \(Q P^{1/2}\) is visibly Hilbert–Schmidt.
Let \(H\) be a complex Hilbert space, let \(T\) be a positive operator on \(H\), and let \(e = (e_k)_{k \in \kappa }\) be a Hilbert basis of \(H\). The trace of \(T\) is
and \(T\) is of finite trace if \(\operatorname {Tr}T {\lt} \infty \).
The terms are nonnegative, because \(\operatorname {Re}\langle x, T x \rangle = \| T^{1/2} x\| ^2\), so \(\operatorname {Tr}T = \sum _k \| T^{1/2} e_k\| ^2\) is the squared Hilbert–Schmidt norm of \(T^{1/2}\). Lemma 2.4(c) for the self-adjoint operator \(T^{1/2}\) gives the same value in \([0, \infty ]\) along every Hilbert basis, so the trace does not depend on \(e\). For a positive operator \(P\) of finite trace and a positive operator \(Q\) write \(\operatorname {Tr}(P Q) = \sum _k \operatorname {Re}\langle e_k, P Q e_k \rangle \); by Lemma 2.6(b) this is the trace of the positive operator \(P^{1/2} Q P^{1/2}\), so it does not depend on \(e\) either.
In Lean the trace is a real number, ContinuousLinearMap.trace, computed along a Hilbert basis chosen once and for all (HilbertBasis.chosen). The sum is taken to be \(0\) when the family is not summable; every statement assumes finite trace, so this convention never enters. The same sum along a given basis \(e\) is traceAlong e, and for a positive operator the two agree (ContinuousLinearMap.trace_eq_traceAlong). The chosen basis is countable when \(H\) is separable and nonempty when \(H\) is nonzero. IsFiniteTracePos J bundles three properties of \(J\): positive, of finite trace, and injective.
Let \(H\) be a complex Hilbert space.
(a) Every positive operator \(T\) on \(H\) of finite trace satisfies \(T \preceq \operatorname {Tr}T \cdot 1\).
(b) Let \(P\) be positive and of finite trace, let \(Q\) be positive, and let \(e = (e_k)_k\) be a Hilbert basis of \(H\). Then
and the value is positive as soon as \(Q\) is invertible and \(P \neq 0\).
(c) Let \(P \preceq P'\) be positive and of finite trace, and let \(Q\) be positive. Then \(\operatorname {Tr}(P Q) \leq \operatorname {Tr}(P' Q)\).
(a) For \(x \in H\), writing \(x\) in a Hilbert basis and applying the Cauchy–Schwarz inequality to each term gives \(\operatorname {Re}\langle x, T x \rangle \leq \operatorname {Tr}T \cdot \| x\| ^2\). This is the operator analogue of Lemma 2.1(b), and unlike the matrix proof it uses no diagonalisation.
(b) The identity is the cyclicity \(\operatorname {Tr}(PQ) = \operatorname {Tr}(P^{1/2} Q P^{1/2})\), read as a symmetry of the pairing \(\sum _k \langle S e_k, T e_k \rangle \) under passing to adjoints; the required summability is Lemma 2.4(b). Every term on the right is nonnegative. For the strict inequality, invertibility of \(Q\) makes \(Q^{1/2}\) injective, so a vanishing trace would force \(P^{1/2}\) to annihilate the whole basis.
(c) The difference \(\operatorname {Tr}(P' Q) - \operatorname {Tr}(P Q)\) is the sum of (b) for the positive operator \(P' - P\) of finite trace, hence nonnegative.
Invertibility of \(Q\) here is what replaces positive definiteness. A positive operator of finite trace on an infinite-dimensional space is compact, hence never bounded away from zero, so positive definiteness is unavailable and the hypotheses on the two operators have to be chosen differently: injectivity for \(J\), and invertibility for the operator the construction moves.