Hilbert Space Explorer Home Page  First > Last > 

Mirrors > Home > MPE Home > Th. List > Recent 
Hilbert space (Wikipedia [external], MathWorld [external]) is a generalization of finitedimensional vector spaces to include vector spaces with infinite dimensions. It provides a foundation of quantum mechanics, and there is a strong physical and philosophical motivation to study its properties. For example, the properties of Hilbert space ultimately determine what kinds of operations are theoretically possible in quantum computation.  
Calcite 
Contents of this page  Related pages 
Symbol  Description  Link to Definition 

Hilbert space base set  (primitive)  
vector addition  (primitive)  
scalar multiplication  (primitive)  
zero vector  (primitive)  
inner (scalar) product  (primitive)  
vector subtraction  dfhvsub  
norm of a vector  dfhnorm  
set of Cauchy sequences  dfhcau  
convergence relation  dfhlim  
set of subspaces  dfsh  
set of closed subspaces  dfch  
orthocomplement  dfoc  
subspace sum  dfshs  
subspace span  dfspan  
join  dfchj  
supremum  dfchsup  
zero subspace  dfch0  
commutes relation  dfcm  
operator sum; definition of "operator" 
dfhosum  
operator scalar product  dfhomul  
operator difference  dfhodif  
functional sum; definition of "functional" 
dfhfsum  
functional scalar product  dfhfmul  
0_{hop}  zero operator  dfh0op 
identity operator  dfiop  
proj  projection operator (projector)  dfpj 
norm_{op}  norm of an operator  dfnmop 
ConOp  set of continuous operators  dfcnop 
LinOp  set of linear operators  dflnop 
BndLinOp  set of bounded linear operators  dfbdop 
UniOp  set of unitary operators  dfunop 
HrmOp  set of Hermitian operators  dfhmop 
norm_{fn}  norm of a functional  dfnmfn 
null  null space of a functional  dfnlfn 
ConFn  set of continuous functionals  dfcnfn 
LinFn  set of linear functionals  dflnfn 
adj_{h}  adjoint of an operator  dfadjh 
bra  Dirac "bra" of a vector  dfbra 
ordering relation for positive operators  dfleop  
ketbra  Dirac "ketbra" (outer product) of two vectors  dfkb 
eigvec  eigenvectors of an operator  dfeigvec 
eigval  eigenvalue of an eigenvector  dfeigval 
spectrum of an operator  dfspec  
set of states  dfst  
CHStates  set of (Mayet's) Hilbertspacevalued states  dfhst 
set of atoms  dfat  
covering relation  dfcv  
modular pair relation  dfmd  
dual modular pair relation  dfdmd 
However, we chose separate axioms for the Hilbert Space Explorer for several reasons. A practical problem with the pure ZFC approach is that theorems becomes somewhat awkward to state and prove, since they usually need additional hypotheses. Compare, for example, the ZFCderived hlcom with the Hilbert Space Explorer axiom axhvcom. Another advantage for a newcomer is that the Hilbert Space Explorer states outright all of its axioms, so there is nothing else to learn (aside from standard set theory tools to manipulate them). In the Metamath Proof Explorer, on the other hand, one needs to become familiar with the hierarchy of groups, topologies, vector spaces, metric spaces, normed vector spaces, and Banach spaces that leads to Hilbert spaces.
If we want to use the Hilbert Space Explorer with any fixed Hilbert space, such as the set of complex numbers (which, as it turns out, is an example of a Hilbert space  see theorem cnhl), a simple change to the axiomatization will convert all theorems in the Hilbert Space Explorer to pure ZFC theorems. A description of how this can be done is given in the comment for axiom axhilex. On the other hand, if we want to prove theorems involving relationships between Hilbert spaces, the Hilbert Space Explorer may not be not suitable, but rewriting its proofs for the general ZFC approach as needed is relatively straightforward. (Actually, many such theorems can still be done in the Hilbert Space Explorer itself using subspaces, each of which acts like a standalone Hilbert Space.)
The page for each axiom below is accompanied by a precise breakdown of its syntax. You can break the syntax down into as much detail as you want by using the hyperlinks in the syntax breakdown chart. Note our use of the notation " " instead of the more common notation "" for inner products; the latter would conflict with our notation for ordered pairs cop.
axhilex  
axhfvadd  
axhvcom  
axhvass  
axhv0cl  
axhvaddid  
axhfvmul  
axhvmulid  
axhvmulass  
axhvdistr1  
axhvdistr2  
axhvmul0  
axhfi  
axhis1  
axhis2  
axhis3  
axhis4  
axhcompl 
Comments on the axioms. The first axiom just says that the primitive class exists (is a member of the universe of sets V). The next 11 axioms are the axioms for any vector space with an unspecified dimension; they are the same as those you would find in any linear algebra book, except for the notation and possibly their precise form.
The next 5 axioms show the properties of the special inner product . The official name for this inner product is a "sesquilinear Hermitian mapping". (Sesquilinear means "oneandahalf linear," i.e., antilinear in the first argument and linear in the second.) The symbol in Axiom axhis1 is the complex conjugate (cjval). See Notation for Function Values for an explanation of why we use this notation rather than the standard superscript asterisk used in textbooks; this will help you understand some of our other nonstandard notation as well.
The last axiom, which is the most important and also the most complicated, is called the Completeness Axiom, and is shown above using abbreviations. You can click on its links to expand the abbreviations. It basically says that the limit of any converging ("Cauchy") sequence of vectors in Hilbert space converges to a vector in Hilbert space. To understand what completeness means, consider this analogy: the sequence 3, 3.1, 3.14, 3.1415, 3.14159... converges to pi. This is a converging sequence of rational numbers, but it converges to something that is not a rational number, meaning the set of rational numbers is not complete. The set of real numbers, on the other hand, is complete, because all converging sequences of real numbers converge to a real number.
The vector subtraction operation dfhvsub  
The norm of a vector dfhnorm  
The set of all Cauchy sequences dfhcau  
The limit of a vector sequence dfhlim  
The set of all subspaces of Hilbert space dfsh  
The set of all closed subspaces of Hilbert space dfch  
The sum of two subspaces dfshsum 
hvsubcl  
hvnegid  
hvmul0  
hvsubid  
hvsubeq0 
Next we show some basic properties of the special inner product defined for Hilbert space.
his5  
his6  
his7 
Next we show some theorems involving norms. Note our use of the notation "" instead of the more common notation ""  see Notation for Function Values.
Theorems normi, normii (triangle inequality), and normiii show that the basic properties expected of any norm hold for the norm we defined for Hilbert space. Theorem normpyth is an analogy to the Pythagorean theorem, and theorem normpar is the parallellogram law. Theorem bcs is the BunjakovaskijCauchySchwarz inequality.
normi  
normii  
normiii  
normpyth  
normpar  
bcs 
Next we show some basic theorems about sequences. Theorem hlimcaui shows any converging sequence is a Cauchy sequence and hlimunii shows that the limit of a converging sequence is unique. The theorem pjth is the important Projection Theorem; it shows any vector can be decomposed into a pair of "projections" on a subspace and the orthocomplement of the subspace (see below for the definition of the orthocomplement ).
hlimcaui  
hlimunii  
pjth 
The set of closed subspaces of Hilbert space obey the laws of a simple equational algebra called "orthomodular lattice algebra." This algebra is sometimes called "quantum logic," and it can be used as the basis for a propositional calculus that resembles but is somewhat weaker than standard (classical) propositional calculus. This is explained in greater detail in the Quantum Logic Explorer. Our purpose here is to show that the orthomodular lattice laws hold in Hilbert space. This provides a rigorous justification for the axioms of the Quantum Logic Explorer. (By the way, theorem nonbooli shows why classical logic, i.e. Boolean algebra, does not hold in Hilbert space.)
The advantage of the Quantum Logic Explorer is that it lets us work with a simpler axiomatic structure. But in principle, all the theorems of the Quantum Logic Explorer could be proved directly in Hilbert space, using the theorems below as the starting point. In fact in a few cases we do this, because sometimes we need the Hilbert space version to help prove theorems that exploit Hilbert space properties beyond those provided by the orthomodular lattice laws alone. For example, compare the proofs of the Hilbert Space Explorer theorem fh3i and the Quantum Logic Explorer version fh3. If you ignore the steps with an "" in the Hilbert space version, you'll see the proofs are almost identical except for notation; in fact, any differences beyond that just result from the proofs having been developed somewhat independently. You can see why the Quantum Logic Explorer is simpler to work with for these kinds of things: we don't need the " " hypotheses, and we don't have to keep proving operation closure over and over.
To derive the orthomodular lattice postulates, first we define two new operations on members of (the set of closed subspaces of Hilbert space). The orthocomplement of a subspace is the set of vectors orthogonal to all vectors in the subpace. It is analogous to logical NOT. The join of two subspaces is the closure (i.e. the double orthocomplement) of their union. It is analogous to logical OR.
Orthocomplement chocvali  
Join chjval 
Next we show that with these operations, we can derive the Hilbert space versions of the axioms for the Quantum Logic Explorer. You can see that these axioms correspond directly to the 10 theorems below. This provides a physical justification for the study of quantum logic (since quantum physics is based on Hilbert space) and gives us a rigorous mathematical link for quantum logic all the way from the axioms of ZFC set theory and Hilbert space. If you think of the logical OR / logical NOT analogy, you can see that these laws are a subset of the laws that hold in a Boolean algebra. They provide us with a rich and very challenging logical structure to study.
qlax1i  
qlax2i  
qlax3i  
qlax4i  
qlax5i  
qlaxr1i  
qlaxr2i  
qlaxr4i  
qlaxr5i  
qlaxr3i 
Recently myself and M. Pavicic [MegillPavicic] have proved that all equations appearing in the literature that are stronger than orthomodularity but valid in can be derived from either the 4variable orthoarguesian equation or one of the Godowski equations. In addition we recently discovered [MegillPavicic] a family of nvariable equations generalizing the orthoarguesian equation (which can be expressed with 4 variables) that are strictly stronger than it for all members with 5 or more variables. Below we show the 5variable member of this family (expressed as an equivalent 8variable inference below) and also show the 3variable Godowski equation, backed by their complete formal proofs.
5oai 
goeqi 
Photo credit: Norman Megill
Photo copyright: Released to public domain by
the photographer (March 2004)
This
page was last updated on 26Sep2017. Your comments are welcome: Norman Megill Copyright terms: Public domain 
W3C HTML validation [external] 