Metamath Proof Explorer

Table of Contents - 19. COMPLEX HILBERT SPACE EXPLORER (DEPRECATED)

This part contains the definitions and theorems used by the Hilbert Space Explorer (HSE), mmhil.html. Because it axiomatizes a single complex Hilbert space whose existence is assumed, its usefulness is limited. For example, it cannot work with real or quaternion Hilbert spaces and it cannot study relationships between two Hilbert spaces. More information can be found on the Hilbert Space Explorer page.

Future development should instead work with general Hilbert spaces as defined by df-hil; note that df-hil uses extensible structures.

The intent is for this deprecated section to be deleted once all its theorems have been translated into extensible structure versions (or are not useful). Many of the theorems in this section have already been translated to extensible structure versions, but there is still a lot in this section that might be useful for future reference. It is much easier to translate these by hand from this section than to start from scratch from textbook proofs, since the HSE omits no details.

1. Axiomatization of complex pre-Hilbert spaces
   1. Basic Hilbert space definitions
   2. Preliminary ZFC lemmas
   3. Derive the Hilbert space axioms from ZFC set theory
   4. Introduce the vector space axioms for a Hilbert space
   5. Vector operations
   6. Inner product postulates for a Hilbert space
2. Inner product and norms
   1. Inner product
   2. Norms
   3. Relate Hilbert space to normed complex vector spaces
   4. Bunjakovaskij-Cauchy-Schwarz inequality
3. Cauchy sequences and completeness axiom
   1. Cauchy sequences and limits
   2. Derivation of the completeness axiom from ZF set theory
   3. Completeness postulate for a Hilbert space
   4. Relate Hilbert space to ZFC pre-Hilbert and Hilbert spaces
4. Subspaces and projections
   1. Subspaces
   2. Closed subspaces
   3. Orthocomplements
   4. Subspace sum, span, lattice join, lattice supremum
   5. Projection theorem
   6. Projectors
5. Properties of Hilbert subspaces
   1. Orthomodular law
   2. Projectors (cont.)
   3. Hilbert lattice operations
   4. Span (cont.) and one-dimensional subspaces
   5. Commutes relation for Hilbert lattice elements
   6. Foulis-Holland theorem
   7. Quantum Logic Explorer axioms
   8. Orthogonal subspaces
   9. Orthoarguesian laws 5OA and 3OA
   10. Projectors (cont.)
   11. Mayet's equation E_3
6. Operators on Hilbert spaces
   1. Operator sum, difference, and scalar multiplication
   2. Zero and identity operators
   3. Operations on Hilbert space operators
   4. Linear, continuous, bounded, Hermitian, unitary operators and norms
   5. Theorems about operators and functionals
   6. Adjoints (cont.)
   7. Quantum computation error bound theorem
   8. Dirac bra-ket notation (cont.)
   9. Projectors as operators
7. States on a Hilbert lattice and Godowski's equation
   1. States on a Hilbert lattice
   2. Godowski's equation
8. Cover relation, atoms, exchange axiom, and modular symmetry
   1. Covers relation; modular pairs
   2. Atoms
   3. Superposition principle
   4. Atoms, exchange and covering properties, atomicity
   5. Irreducibility
   6. Atoms (cont.)
   7. Modular symmetry