|Hilbert Space Explorer Home Page|| First >
|Mirrors > Home > MPE Home > Th. List > Recent|
|Hilbert space (Wikipedia [external], MathWorld [external]) is a generalization of finite-dimensional 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.|
|Contents of this page||Related pages|
|Symbol||Description||Link to Definition|
|Hilbert space base set||(primitive)|
|inner (scalar) product||(primitive)|
|norm of a vector||df-hnorm|
|set of Cauchy sequences||df-hcau|
|set of subspaces||df-sh|
|set of closed subspaces||df-ch|
definition of "operator"
|operator scalar product||df-homul|
definition of "functional"
|functional scalar product||df-hfmul|
|proj||projection operator (projector)||df-pj|
|normop||norm of an operator||df-nmop|
|ConOp||set of continuous operators||df-cnop|
|LinOp||set of linear operators||df-lnop|
|BndLinOp||set of bounded linear operators||df-bdop|
|UniOp||set of unitary operators||df-unop|
|HrmOp||set of Hermitian operators||df-hmop|
|normfn||norm of a functional||df-nmfn|
|null||null space of a functional||df-nlfn|
|ConFn||set of continuous functionals||df-cnfn|
|LinFn||set of linear functionals||df-lnfn|
|adjh||adjoint of an operator||df-adjh|
|bra||Dirac "bra" of a vector||df-bra|
|ordering relation for positive operators||df-leop|
|ketbra||Dirac "ket-bra" (outer product) of two vectors||df-kb|
|eigvec||eigenvectors of an operator||df-eigvec|
|eigval||eigenvalue of an eigenvector||df-eigval|
|spectrum of an operator||df-spec|
|set of states||df-st|
|CHStates||set of (Mayet's) Hilbert-space-valued states||df-hst|
|set of atoms||df-at|
|modular pair relation||df-md|
|dual modular pair relation||df-dmd|
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 ZFC-derived hlcom with the Hilbert Space Explorer axiom ax-hvcom. 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 ax-hilex. 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 stand-alone 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.
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 "one-and-a-half linear," i.e., antilinear in the first argument and linear in the second.) The symbol in Axiom ax-his1 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 non-standard 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 df-hvsub|
|The norm of a vector df-hnorm|
|The set of all Cauchy sequences df-hcau|
|The limit of a vector sequence df-hlim|
|The set of all subspaces of Hilbert space df-sh|
|The set of all closed subspaces of Hilbert space df-ch|
|The sum of two subspaces df-shsum|
Next we show some basic properties of the special inner product defined for Hilbert space.
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 norm-i, norm-ii (triangle inequality), and norm-iii 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 Bunjakovaskij-Cauchy-Schwarz inequality.
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 ).
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.
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.
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 4-variable orthoarguesian equation or one of the Godowski equations. In addition we recently discovered [MegillPavicic] a family of n-variable 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 5-variable member of this family (expressed as an equivalent 8-variable inference below) and also show the 3-variable Godowski equation, backed by their complete formal proofs.
Photo credit: Norman Megill
Photo copyright: Released to public domain by the photographer (March 2004)
page was last updated on 26-Sep-2017.
Your comments are welcome: Norman Megill
Copyright terms: Public domain
|W3C HTML validation [external]|