Home | Metamath
Proof Explorer Theorem List (p. 288 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-bdop 28701 | Define the set of bounded linear Hilbert space operators. (See df-hosum 28589 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
Definition | df-unop 28702* | Define the set of unitary operators on Hilbert space. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
Definition | df-hmop 28703* | Define the set of Hermitian operators on Hilbert space. Some books call these "symmetric operators" and others call them "self-adjoint operators," sometimes with slightly different technical meanings. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
Definition | df-nmfn 28704* | Define the norm of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
Definition | df-nlfn 28705 | Define the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
Definition | df-cnfn 28706* | Define the set of continuous functionals on Hilbert space. For every "epsilon" () there is a "delta" () such that... (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
Definition | df-lnfn 28707* | Define the set of linear functionals on Hilbert space. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
Definition | df-adjh 28708* | Define the adjoint of a Hilbert space operator (if it exists). The domain of is the set of all adjoint operators. Definition of adjoint in [Kalmbach2] p. 8. Unlike Kalmbach (and most authors), we do not demand that the operator be linear, but instead show (in adjbdln 28942) that the adjoint exists for a bounded linear operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
Definition | df-bra 28709* |
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 . 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 ; see
braval 28803. The reversal of the inner product
arguments not only makes
the bra-ket behavior consistent with physics literature (see comments
under ax-his3 27941) but is also required in order for the
associative law
kbass2 28976 to work.
Our definition of bra and the associated outer product df-kb 28710 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, under the 17-May-2006 entry. (Contributed by NM, 15-May-2006.) (New usage is discouraged.) |
Definition | df-kb 28710* | Define a commuted bra and ket juxtaposition used by Dirac notation. In Dirac notation, is an operator known as the outer product of and , which we represent by . Based on Equation 8.1 of [Prugovecki] p. 376. This definition, combined with definition df-bra 28709, allows any legal juxtaposition of bras and kets to make sense formally and also to obey the associative law when mapped back to Dirac notation. (Contributed by NM, 15-May-2006.) (New usage is discouraged.) |
Definition | df-leop 28711* | Define positive operator ordering. Definition VI.1 of [Retherford] p. 49. Note that means that is a positive operator. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
Definition | df-eigvec 28712* | Define the eigenvector function. Theorem eleigveccl 28818 shows that , the set of eigenvectors of Hilbert space operator , are Hilbert space vectors. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
Definition | df-eigval 28713* | Define the eigenvalue function. The range of is the set of eigenvalues of Hilbert space operator . Theorem eigvalcl 28820 shows that , the eigenvalue associated with eigenvector , is a complex number. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
Definition | df-spec 28714* | Define the spectrum of an operator. Definition of spectrum in [Halmos] p. 50. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.) |
Theorem | nmopval 28715* | Value of the norm of a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
Theorem | elcnop 28716* | Property defining a continuous Hilbert space operator. (Contributed by NM, 28-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
Theorem | ellnop 28717* | Property defining a linear Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
Theorem | lnopf 28718 | A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
Theorem | elbdop 28719 | Property defining a bounded linear Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
Theorem | bdopln 28720 | A bounded linear Hilbert space operator is a linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
Theorem | bdopf 28721 | A bounded linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) |
Theorem | nmopsetretALT 28722* | The set in the supremum of the operator norm definition df-nmop 28698 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | nmopsetretHIL 28723* | The set in the supremum of the operator norm definition df-nmop 28698 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) |
Theorem | nmopsetn0 28724* | The set in the supremum of the operator norm definition df-nmop 28698 is nonempty. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
Theorem | nmopxr 28725 | The norm of a Hilbert space operator is an extended real. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
Theorem | nmoprepnf 28726 | The norm of a Hilbert space operator is either real or plus infinity. (Contributed by NM, 5-Feb-2006.) (New usage is discouraged.) |
Theorem | nmopgtmnf 28727 | The norm of a Hilbert space operator is not minus infinity. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) |
Theorem | nmopreltpnf 28728 | The norm of a Hilbert space operator is real iff it is less than infinity. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
Theorem | nmopre 28729 | The norm of a bounded operator is a real number. (Contributed by NM, 29-Jan-2006.) (New usage is discouraged.) |
Theorem | elbdop2 28730 | Property defining a bounded linear Hilbert space operator. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
Theorem | elunop 28731* | Property defining a unitary Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
Theorem | elhmop 28732* | Property defining a Hermitian Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
Theorem | hmopf 28733 | A Hermitian operator is a Hilbert space operator (mapping). (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.) |
Theorem | hmopex 28734 | The class of Hermitian operators is a set. (Contributed by NM, 17-Aug-2006.) (New usage is discouraged.) |
Theorem | nmfnval 28735* | Value of the norm of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
Theorem | nmfnsetre 28736* | The set in the supremum of the functional norm definition df-nmfn 28704 is a set of reals. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
Theorem | nmfnsetn0 28737* | The set in the supremum of the functional norm definition df-nmfn 28704 is nonempty. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
Theorem | nmfnxr 28738 | The norm of any Hilbert space functional is an extended real. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
Theorem | nmfnrepnf 28739 | The norm of a Hilbert space functional is either real or plus infinity. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
Theorem | nlfnval 28740 | Value of the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
Theorem | elcnfn 28741* | Property defining a continuous functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
Theorem | ellnfn 28742* | Property defining a linear functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
Theorem | lnfnf 28743 | A linear Hilbert space functional is a functional. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
Theorem | dfadj2 28744* | Alternate definition of the adjoint of a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
Theorem | funadj 28745 | Functionality of the adjoint function. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
Theorem | dmadjss 28746 | The domain of the adjoint function is a subset of the maps from to . (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
Theorem | dmadjop 28747 | A member of the domain of the adjoint function is a Hilbert space operator. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
Theorem | adjeu 28748* | Elementhood in the domain of the adjoint function. (Contributed by Mario Carneiro, 11-Sep-2015.) (Revised by Mario Carneiro, 24-Dec-2016.) (New usage is discouraged.) |
Theorem | adjval 28749* | Value of the adjoint function for in the domain of . (Contributed by NM, 19-Feb-2006.) (Revised by Mario Carneiro, 24-Dec-2016.) (New usage is discouraged.) |
Theorem | adjval2 28750* | Value of the adjoint function. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
Theorem | cnvadj 28751 | The adjoint function equals its converse. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
Theorem | funcnvadj 28752 | The converse of the adjoint function is a function. (Contributed by NM, 25-Jan-2006.) (New usage is discouraged.) |
Theorem | adj1o 28753 | The adjoint function maps one-to-one onto its domain. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
Theorem | dmadjrn 28754 | The adjoint of an operator belongs to the adjoint function's domain. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
Theorem | eigvecval 28755* | The set of eigenvectors of a Hilbert space operator. (Contributed by NM, 11-Mar-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
Theorem | eigvalfval 28756* | The eigenvalues of eigenvectors of a Hilbert space operator. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
Theorem | specval 28757* | The value of the spectrum of an operator. (Contributed by NM, 11-Apr-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
Theorem | speccl 28758 | The spectrum of an operator is a set of complex numbers. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.) |
Theorem | hhlnoi 28759 | The linear operators of Hilbert space. (Contributed by NM, 19-Nov-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
Theorem | hhnmoi 28760 | The norm of an operator in Hilbert space. (Contributed by NM, 19-Nov-2007.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
Theorem | hhbloi 28761 | A bounded linear operator in Hilbert space. (Contributed by NM, 19-Nov-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
Theorem | hh0oi 28762 | The zero operator in Hilbert space. (Contributed by NM, 7-Dec-2007.) (New usage is discouraged.) |
Theorem | hhcno 28763 | The continuous operators of Hilbert space. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
Theorem | hhcnf 28764 | The continuous functionals of Hilbert space. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
ℂfld | ||
Theorem | dmadjrnb 28765 | The adjoint of an operator belongs to the adjoint function's domain. (Note: the converse is dependent on our definition of function value, since it uses ndmfv 6218.) (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
Theorem | nmoplb 28766 | A lower bound for an operator norm. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
Theorem | nmopub 28767* | An upper bound for an operator norm. (Contributed by NM, 7-Mar-2006.) (New usage is discouraged.) |
Theorem | nmopub2tALT 28768* | An upper bound for an operator norm. (Contributed by NM, 12-Apr-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | nmopub2tHIL 28769* | An upper bound for an operator norm. (Contributed by NM, 13-Dec-2007.) (New usage is discouraged.) |
Theorem | nmopge0 28770 | The norm of any Hilbert space operator is nonnegative. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
Theorem | nmopgt0 28771 | A linear Hilbert space operator that is not identically zero has a positive norm. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
Theorem | cnopc 28772* | Basic continuity property of a continuous Hilbert space operator. (Contributed by NM, 2-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
Theorem | lnopl 28773 | Basic linearity property of a linear Hilbert space operator. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
Theorem | unop 28774 | Basic inner product property of a unitary operator. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
Theorem | unopf1o 28775 | A unitary operator in Hilbert space is one-to-one and onto. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
Theorem | unopnorm 28776 | A unitary operator is idempotent in the norm. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.) |
Theorem | cnvunop 28777 | The inverse (converse) of a unitary operator in Hilbert space is unitary. Theorem in [AkhiezerGlazman] p. 72. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
Theorem | unopadj 28778 | The inverse (converse) of a unitary operator is its adjoint. Equation 2 of [AkhiezerGlazman] p. 72. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
Theorem | unoplin 28779 | A unitary operator is linear. Theorem in [AkhiezerGlazman] p. 72. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
Theorem | counop 28780 | The composition of two unitary operators is unitary. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
Theorem | hmop 28781 | Basic inner product property of a Hermitian operator. (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.) |
Theorem | hmopre 28782 | The inner product of the value and argument of a Hermitian operator is real. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
Theorem | nmfnlb 28783 | A lower bound for a functional norm. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
Theorem | nmfnleub 28784* | An upper bound for the norm of a functional. (Contributed by NM, 24-May-2006.) (Revised by Mario Carneiro, 7-Sep-2014.) (New usage is discouraged.) |
Theorem | nmfnleub2 28785* | An upper bound for the norm of a functional. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
Theorem | nmfnge0 28786 | The norm of any Hilbert space functional is nonnegative. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
Theorem | elnlfn 28787 | Membership in the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
Theorem | elnlfn2 28788 | Membership in the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
Theorem | cnfnc 28789* | Basic continuity property of a continuous functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
Theorem | lnfnl 28790 | Basic linearity property of a linear functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
Theorem | adjcl 28791 | Closure of the adjoint of a Hilbert space operator. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.) |
Theorem | adj1 28792 | Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
Theorem | adj2 28793 | Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
Theorem | adjeq 28794* | A property that determines the adjoint of a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
Theorem | adjadj 28795 | Double adjoint. Theorem 3.11(iv) of [Beran] p. 106. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
Theorem | adjvalval 28796* | Value of the value of the adjoint function. (Contributed by NM, 22-Feb-2006.) (Proof shortened by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
Theorem | unopadj2 28797 | The adjoint of a unitary operator is its inverse (converse). Equation 2 of [AkhiezerGlazman] p. 72. (Contributed by NM, 23-Feb-2006.) (New usage is discouraged.) |
Theorem | hmopadj 28798 | A Hermitian operator is self-adjoint. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
Theorem | hmdmadj 28799 | Every Hermitian operator has an adjoint. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
Theorem | hmopadj2 28800 | An operator is Hermitian iff it is self-adjoint. Definition of Hermitian in [Halmos] p. 41. (Contributed by NM, 9-Apr-2006.) (New usage is discouraged.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |