Email Gateway (Dec 04 2024 at 17:57): Email Gateway (Dec 04 2024 at 17:57):From: Manuel Eberl <manuel@pruvisto.org>
The Tensor Product on Hilbert Spaces
by Dominique Unruh
We formalize the tensor product of Hilbert spaces, and related material.
Specifically, we define the product of vectors in Hilbert spaces, of
operators on Hilbert spaces, and of subspaces of Hilbert spaces, and of
von Neumann algebras, and study their properties. The theory is based on
the AFP entry Complex_Bounded_Operators that introduces Hilbert spaces
and operators and related concepts, but in addition to their work, we
defined and study a number of additional concepts needed for the tensor
product. Specifically: Hilbert-Schmidt and trace-class operators;
compact operators; positive operators; the weak operator, strong
operator, and weak^* topology; the spectral theorem for compact
operators; and the double commutant theorem.
https://www.isa-afp.org/entries/Hilbert_Space_Tensor_Product.html
Enjoy!
Manuel
Last updated: Jan 04 2025 at 20:18 UTC