Description: Define the bra of a
vector used by Dirac notation. Based on definition
of bra in [Prugovecki] p. 186 (p.
180 in 1971 edition). In Dirac
bra-ket notation, β¨π΄ β£ π΅β© is a complex number equal to
the inner
product (π΅ Β·ih π΄). But physicists like
to talk about the
individual components β¨π΄ β£ and β£
π΅β©, called bra
and ket
respectively. In order for their properties to make sense formally, we
define the ket β£ π΅β© as the vector π΅ itself,
and the bra
β¨π΄ β£ as a functional from β to β. We represent the
Dirac notation β¨π΄ β£ π΅β© by ((braβπ΄)βπ΅); see
braval 30928. The reversal of the inner product
arguments not only makes
the bra-ket behavior consistent with physics literature (see comments
under ax-his3 30068) but is also required in order for the
associative law
kbass2 31101 to work.
Our definition of bra and the associated outer product df-kb 30835 differs
from, but is equivalent to, a common approach in the literature that
makes use of mappings to a dual space. Our approach eliminates the need
to have a parallel development of this dual space and instead keeps
everything in Hilbert space.
For an extensive discussion about how our notation maps to the
bra-ket
notation in physics textbooks, see mmnotes.txt 30835, under the 17-May-2006
entry. (Contributed by NM, 15-May-2006.)
(New usage is discouraged.) |