The absolute value of an operator, trace norm, and operator norm are respectively
The positive square root of an operator makes well defined. Its eigenvalues are the singular values of , so and .
Use the polar decomposition of a bounded operator , with the given unitary operator . In an orthonormal eigenbasis for ,
The operator norm assumption and unitarity imply . The triangle inequality therefore yields the required trace estimate:
Choosing attains equality, which also gives the finite-dimensional trace duality formula . A singular causes no difficulty: in a finite-dimensional square space the polar factor can be extended to a unitary operator on the complementary subspaces.