![]() |
Metamath
Proof Explorer Theorem List (p. 312 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-lnfn 31101* | Define the set of linear functionals on Hilbert space. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
β’ LinFn = {π‘ β (β βm β) β£ βπ₯ β β βπ¦ β β βπ§ β β (π‘β((π₯ Β·β π¦) +β π§)) = ((π₯ Β· (π‘βπ¦)) + (π‘βπ§))} | ||
Definition | df-adjh 31102* | Define the adjoint of a Hilbert space operator (if it exists). The domain of adjβ 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 31336) that the adjoint exists for a bounded linear operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
β’ adjβ = {β¨π‘, π’β© β£ (π‘: ββΆ β β§ π’: ββΆ β β§ βπ₯ β β βπ¦ β β ((π‘βπ₯) Β·ih π¦) = (π₯ Β·ih (π’βπ¦)))} | ||
Definition | df-bra 31103* |
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 31197. The reversal of the inner product
arguments not only makes
the bra-ket behavior consistent with physics literature (see comments
under ax-his3 30337) but is also required in order for the
associative law
kbass2 31370 to work.
Our definition of bra and the associated outer product df-kb 31104 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 31104, under the 17-May-2006 entry. (Contributed by NM, 15-May-2006.) (New usage is discouraged.) |
β’ bra = (π₯ β β β¦ (π¦ β β β¦ (π¦ Β·ih π₯))) | ||
Definition | df-kb 31104* | 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 (π΄ ketbra π΅). Based on Equation 8.1 of [Prugovecki] p. 376. This definition, combined with Definition df-bra 31103, 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.) |
β’ ketbra = (π₯ β β, π¦ β β β¦ (π§ β β β¦ ((π§ Β·ih π¦) Β·β π₯))) | ||
Definition | df-leop 31105* | Define positive operator ordering. Definition VI.1 of [Retherford] p. 49. Note that ( β Γ 0β) β€op π means that π is a positive operator. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
β’ β€op = {β¨π‘, π’β© β£ ((π’ βop π‘) β HrmOp β§ βπ₯ β β 0 β€ (((π’ βop π‘)βπ₯) Β·ih π₯))} | ||
Definition | df-eigvec 31106* | Define the eigenvector function. Theorem eleigveccl 31212 shows that eigvecβπ, the set of eigenvectors of Hilbert space operator π, are Hilbert space vectors. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
β’ eigvec = (π‘ β ( β βm β) β¦ {π₯ β ( β β 0β) β£ βπ§ β β (π‘βπ₯) = (π§ Β·β π₯)}) | ||
Definition | df-eigval 31107* | Define the eigenvalue function. The range of eigvalβπ is the set of eigenvalues of Hilbert space operator π. Theorem eigvalcl 31214 shows that (eigvalβπ)βπ΄, the eigenvalue associated with eigenvector π΄, is a complex number. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
β’ eigval = (π‘ β ( β βm β) β¦ (π₯ β (eigvecβπ‘) β¦ (((π‘βπ₯) Β·ih π₯) / ((normββπ₯)β2)))) | ||
Definition | df-spec 31108* | Define the spectrum of an operator. Definition of spectrum in [Halmos] p. 50. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.) |
β’ Lambda = (π‘ β ( β βm β) β¦ {π₯ β β β£ Β¬ (π‘ βop (π₯ Β·op ( I βΎ β))): ββ1-1β β}) | ||
Theorem | nmopval 31109* | 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.) |
β’ (π: ββΆ β β (normopβπ) = sup({π₯ β£ βπ¦ β β ((normββπ¦) β€ 1 β§ π₯ = (normββ(πβπ¦)))}, β*, < )) | ||
Theorem | elcnop 31110* | Property defining a continuous Hilbert space operator. (Contributed by NM, 28-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
β’ (π β ContOp β (π: ββΆ β β§ βπ₯ β β βπ¦ β β+ βπ§ β β+ βπ€ β β ((normββ(π€ ββ π₯)) < π§ β (normββ((πβπ€) ββ (πβπ₯))) < π¦))) | ||
Theorem | ellnop 31111* | Property defining a linear Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
β’ (π β LinOp β (π: ββΆ β β§ βπ₯ β β βπ¦ β β βπ§ β β (πβ((π₯ Β·β π¦) +β π§)) = ((π₯ Β·β (πβπ¦)) +β (πβπ§)))) | ||
Theorem | lnopf 31112 | A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
β’ (π β LinOp β π: ββΆ β) | ||
Theorem | elbdop 31113 | 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.) |
β’ (π β BndLinOp β (π β LinOp β§ (normopβπ) < +β)) | ||
Theorem | bdopln 31114 | A bounded linear Hilbert space operator is a linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
β’ (π β BndLinOp β π β LinOp) | ||
Theorem | bdopf 31115 | A bounded linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) |
β’ (π β BndLinOp β π: ββΆ β) | ||
Theorem | nmopsetretALT 31116* | The set in the supremum of the operator norm definition df-nmop 31092 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (π: ββΆ β β {π₯ β£ βπ¦ β β ((normββπ¦) β€ 1 β§ π₯ = (normββ(πβπ¦)))} β β) | ||
Theorem | nmopsetretHIL 31117* | The set in the supremum of the operator norm definition df-nmop 31092 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) |
β’ (π: ββΆ β β {π₯ β£ βπ¦ β β ((normββπ¦) β€ 1 β§ π₯ = (normββ(πβπ¦)))} β β) | ||
Theorem | nmopsetn0 31118* | The set in the supremum of the operator norm definition df-nmop 31092 is nonempty. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
β’ (normββ(πβ0β)) β {π₯ β£ βπ¦ β β ((normββπ¦) β€ 1 β§ π₯ = (normββ(πβπ¦)))} | ||
Theorem | nmopxr 31119 | The norm of a Hilbert space operator is an extended real. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
β’ (π: ββΆ β β (normopβπ) β β*) | ||
Theorem | nmoprepnf 31120 | The norm of a Hilbert space operator is either real or plus infinity. (Contributed by NM, 5-Feb-2006.) (New usage is discouraged.) |
β’ (π: ββΆ β β ((normopβπ) β β β (normopβπ) β +β)) | ||
Theorem | nmopgtmnf 31121 | The norm of a Hilbert space operator is not minus infinity. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) |
β’ (π: ββΆ β β -β < (normopβπ)) | ||
Theorem | nmopreltpnf 31122 | 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.) |
β’ (π: ββΆ β β ((normopβπ) β β β (normopβπ) < +β)) | ||
Theorem | nmopre 31123 | The norm of a bounded operator is a real number. (Contributed by NM, 29-Jan-2006.) (New usage is discouraged.) |
β’ (π β BndLinOp β (normopβπ) β β) | ||
Theorem | elbdop2 31124 | Property defining a bounded linear Hilbert space operator. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ (π β BndLinOp β (π β LinOp β§ (normopβπ) β β)) | ||
Theorem | elunop 31125* | Property defining a unitary Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
β’ (π β UniOp β (π: ββontoβ β β§ βπ₯ β β βπ¦ β β ((πβπ₯) Β·ih (πβπ¦)) = (π₯ Β·ih π¦))) | ||
Theorem | elhmop 31126* | Property defining a Hermitian Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
β’ (π β HrmOp β (π: ββΆ β β§ βπ₯ β β βπ¦ β β (π₯ Β·ih (πβπ¦)) = ((πβπ₯) Β·ih π¦))) | ||
Theorem | hmopf 31127 | A Hermitian operator is a Hilbert space operator (mapping). (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.) |
β’ (π β HrmOp β π: ββΆ β) | ||
Theorem | hmopex 31128 | The class of Hermitian operators is a set. (Contributed by NM, 17-Aug-2006.) (New usage is discouraged.) |
β’ HrmOp β V | ||
Theorem | nmfnval 31129* | 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.) |
β’ (π: ββΆβ β (normfnβπ) = sup({π₯ β£ βπ¦ β β ((normββπ¦) β€ 1 β§ π₯ = (absβ(πβπ¦)))}, β*, < )) | ||
Theorem | nmfnsetre 31130* | The set in the supremum of the functional norm definition df-nmfn 31098 is a set of reals. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ (π: ββΆβ β {π₯ β£ βπ¦ β β ((normββπ¦) β€ 1 β§ π₯ = (absβ(πβπ¦)))} β β) | ||
Theorem | nmfnsetn0 31131* | The set in the supremum of the functional norm definition df-nmfn 31098 is nonempty. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ (absβ(πβ0β)) β {π₯ β£ βπ¦ β β ((normββπ¦) β€ 1 β§ π₯ = (absβ(πβπ¦)))} | ||
Theorem | nmfnxr 31132 | The norm of any Hilbert space functional is an extended real. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
β’ (π: ββΆβ β (normfnβπ) β β*) | ||
Theorem | nmfnrepnf 31133 | The norm of a Hilbert space functional is either real or plus infinity. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
β’ (π: ββΆβ β ((normfnβπ) β β β (normfnβπ) β +β)) | ||
Theorem | nlfnval 31134 | Value of the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
β’ (π: ββΆβ β (nullβπ) = (β‘π β {0})) | ||
Theorem | elcnfn 31135* | Property defining a continuous functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
β’ (π β ContFn β (π: ββΆβ β§ βπ₯ β β βπ¦ β β+ βπ§ β β+ βπ€ β β ((normββ(π€ ββ π₯)) < π§ β (absβ((πβπ€) β (πβπ₯))) < π¦))) | ||
Theorem | ellnfn 31136* | Property defining a linear functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
β’ (π β LinFn β (π: ββΆβ β§ βπ₯ β β βπ¦ β β βπ§ β β (πβ((π₯ Β·β π¦) +β π§)) = ((π₯ Β· (πβπ¦)) + (πβπ§)))) | ||
Theorem | lnfnf 31137 | A linear Hilbert space functional is a functional. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
β’ (π β LinFn β π: ββΆβ) | ||
Theorem | dfadj2 31138* | Alternate definition of the adjoint of a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
β’ adjβ = {β¨π‘, π’β© β£ (π‘: ββΆ β β§ π’: ββΆ β β§ βπ₯ β β βπ¦ β β (π₯ Β·ih (π‘βπ¦)) = ((π’βπ₯) Β·ih π¦))} | ||
Theorem | funadj 31139 | Functionality of the adjoint function. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
β’ Fun adjβ | ||
Theorem | dmadjss 31140 | The domain of the adjoint function is a subset of the maps from β to β. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
β’ dom adjβ β ( β βm β) | ||
Theorem | dmadjop 31141 | A member of the domain of the adjoint function is a Hilbert space operator. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
β’ (π β dom adjβ β π: ββΆ β) | ||
Theorem | adjeu 31142* | 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.) |
β’ (π: ββΆ β β (π β dom adjβ β β!π’ β ( β βm β)βπ₯ β β βπ¦ β β (π₯ Β·ih (πβπ¦)) = ((π’βπ₯) Β·ih π¦))) | ||
Theorem | adjval 31143* | Value of the adjoint function for π in the domain of adjβ. (Contributed by NM, 19-Feb-2006.) (Revised by Mario Carneiro, 24-Dec-2016.) (New usage is discouraged.) |
β’ (π β dom adjβ β (adjββπ) = (β©π’ β ( β βm β)βπ₯ β β βπ¦ β β (π₯ Β·ih (πβπ¦)) = ((π’βπ₯) Β·ih π¦))) | ||
Theorem | adjval2 31144* | Value of the adjoint function. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
β’ (π β dom adjβ β (adjββπ) = (β©π’ β ( β βm β)βπ₯ β β βπ¦ β β ((πβπ₯) Β·ih π¦) = (π₯ Β·ih (π’βπ¦)))) | ||
Theorem | cnvadj 31145 | The adjoint function equals its converse. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
β’ β‘adjβ = adjβ | ||
Theorem | funcnvadj 31146 | The converse of the adjoint function is a function. (Contributed by NM, 25-Jan-2006.) (New usage is discouraged.) |
β’ Fun β‘adjβ | ||
Theorem | adj1o 31147 | The adjoint function maps one-to-one onto its domain. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
β’ adjβ:dom adjββ1-1-ontoβdom adjβ | ||
Theorem | dmadjrn 31148 | The adjoint of an operator belongs to the adjoint function's domain. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
β’ (π β dom adjβ β (adjββπ) β dom adjβ) | ||
Theorem | eigvecval 31149* | 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.) |
β’ (π: ββΆ β β (eigvecβπ) = {π₯ β ( β β 0β) β£ βπ¦ β β (πβπ₯) = (π¦ Β·β π₯)}) | ||
Theorem | eigvalfval 31150* | The eigenvalues of eigenvectors of a Hilbert space operator. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
β’ (π: ββΆ β β (eigvalβπ) = (π₯ β (eigvecβπ) β¦ (((πβπ₯) Β·ih π₯) / ((normββπ₯)β2)))) | ||
Theorem | specval 31151* | 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.) |
β’ (π: ββΆ β β (Lambdaβπ) = {π₯ β β β£ Β¬ (π βop (π₯ Β·op ( I βΎ β))): ββ1-1β β}) | ||
Theorem | speccl 31152 | The spectrum of an operator is a set of complex numbers. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.) |
β’ (π: ββΆ β β (Lambdaβπ) β β) | ||
Theorem | hhlnoi 31153 | The linear operators of Hilbert space. (Contributed by NM, 19-Nov-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ πΏ = (π LnOp π) β β’ LinOp = πΏ | ||
Theorem | hhnmoi 31154 | 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.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π = (π normOpOLD π) β β’ normop = π | ||
Theorem | hhbloi 31155 | A bounded linear operator in Hilbert space. (Contributed by NM, 19-Nov-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π΅ = (π BLnOp π) β β’ BndLinOp = π΅ | ||
Theorem | hh0oi 31156 | The zero operator in Hilbert space. (Contributed by NM, 7-Dec-2007.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π = (π 0op π) β β’ 0hop = π | ||
Theorem | hhcno 31157 | The continuous operators of Hilbert space. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
β’ π· = (normβ β ββ ) & β’ π½ = (MetOpenβπ·) β β’ ContOp = (π½ Cn π½) | ||
Theorem | hhcnf 31158 | The continuous functionals of Hilbert space. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
β’ π· = (normβ β ββ ) & β’ π½ = (MetOpenβπ·) & β’ πΎ = (TopOpenββfld) β β’ ContFn = (π½ Cn πΎ) | ||
Theorem | dmadjrnb 31159 | 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 6927.) (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
β’ (π β dom adjβ β (adjββπ) β dom adjβ) | ||
Theorem | nmoplb 31160 | A lower bound for an operator norm. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
β’ ((π: ββΆ β β§ π΄ β β β§ (normββπ΄) β€ 1) β (normββ(πβπ΄)) β€ (normopβπ)) | ||
Theorem | nmopub 31161* | An upper bound for an operator norm. (Contributed by NM, 7-Mar-2006.) (New usage is discouraged.) |
β’ ((π: ββΆ β β§ π΄ β β*) β ((normopβπ) β€ π΄ β βπ₯ β β ((normββπ₯) β€ 1 β (normββ(πβπ₯)) β€ π΄))) | ||
Theorem | nmopub2tALT 31162* | An upper bound for an operator norm. (Contributed by NM, 12-Apr-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ ((π: ββΆ β β§ (π΄ β β β§ 0 β€ π΄) β§ βπ₯ β β (normββ(πβπ₯)) β€ (π΄ Β· (normββπ₯))) β (normopβπ) β€ π΄) | ||
Theorem | nmopub2tHIL 31163* | An upper bound for an operator norm. (Contributed by NM, 13-Dec-2007.) (New usage is discouraged.) |
β’ ((π: ββΆ β β§ (π΄ β β β§ 0 β€ π΄) β§ βπ₯ β β (normββ(πβπ₯)) β€ (π΄ Β· (normββπ₯))) β (normopβπ) β€ π΄) | ||
Theorem | nmopge0 31164 | The norm of any Hilbert space operator is nonnegative. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
β’ (π: ββΆ β β 0 β€ (normopβπ)) | ||
Theorem | nmopgt0 31165 | A linear Hilbert space operator that is not identically zero has a positive norm. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
β’ (π: ββΆ β β ((normopβπ) β 0 β 0 < (normopβπ))) | ||
Theorem | cnopc 31166* | 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.) |
β’ ((π β ContOp β§ π΄ β β β§ π΅ β β+) β βπ₯ β β+ βπ¦ β β ((normββ(π¦ ββ π΄)) < π₯ β (normββ((πβπ¦) ββ (πβπ΄))) < π΅)) | ||
Theorem | lnopl 31167 | Basic linearity property of a linear Hilbert space operator. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
β’ (((π β LinOp β§ π΄ β β) β§ (π΅ β β β§ πΆ β β)) β (πβ((π΄ Β·β π΅) +β πΆ)) = ((π΄ Β·β (πβπ΅)) +β (πβπΆ))) | ||
Theorem | unop 31168 | Basic inner product property of a unitary operator. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
β’ ((π β UniOp β§ π΄ β β β§ π΅ β β) β ((πβπ΄) Β·ih (πβπ΅)) = (π΄ Β·ih π΅)) | ||
Theorem | unopf1o 31169 | A unitary operator in Hilbert space is one-to-one and onto. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
β’ (π β UniOp β π: ββ1-1-ontoβ β) | ||
Theorem | unopnorm 31170 | A unitary operator is idempotent in the norm. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.) |
β’ ((π β UniOp β§ π΄ β β) β (normββ(πβπ΄)) = (normββπ΄)) | ||
Theorem | cnvunop 31171 | 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.) |
β’ (π β UniOp β β‘π β UniOp) | ||
Theorem | unopadj 31172 | 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.) |
β’ ((π β UniOp β§ π΄ β β β§ π΅ β β) β ((πβπ΄) Β·ih π΅) = (π΄ Β·ih (β‘πβπ΅))) | ||
Theorem | unoplin 31173 | A unitary operator is linear. Theorem in [AkhiezerGlazman] p. 72. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
β’ (π β UniOp β π β LinOp) | ||
Theorem | counop 31174 | The composition of two unitary operators is unitary. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
β’ ((π β UniOp β§ π β UniOp) β (π β π) β UniOp) | ||
Theorem | hmop 31175 | Basic inner product property of a Hermitian operator. (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.) |
β’ ((π β HrmOp β§ π΄ β β β§ π΅ β β) β (π΄ Β·ih (πβπ΅)) = ((πβπ΄) Β·ih π΅)) | ||
Theorem | hmopre 31176 | The inner product of the value and argument of a Hermitian operator is real. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
β’ ((π β HrmOp β§ π΄ β β) β ((πβπ΄) Β·ih π΄) β β) | ||
Theorem | nmfnlb 31177 | A lower bound for a functional norm. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ ((π: ββΆβ β§ π΄ β β β§ (normββπ΄) β€ 1) β (absβ(πβπ΄)) β€ (normfnβπ)) | ||
Theorem | nmfnleub 31178* | 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.) |
β’ ((π: ββΆβ β§ π΄ β β*) β ((normfnβπ) β€ π΄ β βπ₯ β β ((normββπ₯) β€ 1 β (absβ(πβπ₯)) β€ π΄))) | ||
Theorem | nmfnleub2 31179* | An upper bound for the norm of a functional. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
β’ ((π: ββΆβ β§ (π΄ β β β§ 0 β€ π΄) β§ βπ₯ β β (absβ(πβπ₯)) β€ (π΄ Β· (normββπ₯))) β (normfnβπ) β€ π΄) | ||
Theorem | nmfnge0 31180 | The norm of any Hilbert space functional is nonnegative. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
β’ (π: ββΆβ β 0 β€ (normfnβπ)) | ||
Theorem | elnlfn 31181 | 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.) |
β’ (π: ββΆβ β (π΄ β (nullβπ) β (π΄ β β β§ (πβπ΄) = 0))) | ||
Theorem | elnlfn2 31182 | 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.) |
β’ ((π: ββΆβ β§ π΄ β (nullβπ)) β (πβπ΄) = 0) | ||
Theorem | cnfnc 31183* | Basic continuity property of a continuous functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
β’ ((π β ContFn β§ π΄ β β β§ π΅ β β+) β βπ₯ β β+ βπ¦ β β ((normββ(π¦ ββ π΄)) < π₯ β (absβ((πβπ¦) β (πβπ΄))) < π΅)) | ||
Theorem | lnfnl 31184 | Basic linearity property of a linear functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
β’ (((π β LinFn β§ π΄ β β) β§ (π΅ β β β§ πΆ β β)) β (πβ((π΄ Β·β π΅) +β πΆ)) = ((π΄ Β· (πβπ΅)) + (πβπΆ))) | ||
Theorem | adjcl 31185 | Closure of the adjoint of a Hilbert space operator. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.) |
β’ ((π β dom adjβ β§ π΄ β β) β ((adjββπ)βπ΄) β β) | ||
Theorem | adj1 31186 | Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
β’ ((π β dom adjβ β§ π΄ β β β§ π΅ β β) β (π΄ Β·ih (πβπ΅)) = (((adjββπ)βπ΄) Β·ih π΅)) | ||
Theorem | adj2 31187 | Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
β’ ((π β dom adjβ β§ π΄ β β β§ π΅ β β) β ((πβπ΄) Β·ih π΅) = (π΄ Β·ih ((adjββπ)βπ΅))) | ||
Theorem | adjeq 31188* | A property that determines the adjoint of a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
β’ ((π: ββΆ β β§ π: ββΆ β β§ βπ₯ β β βπ¦ β β ((πβπ₯) Β·ih π¦) = (π₯ Β·ih (πβπ¦))) β (adjββπ) = π) | ||
Theorem | adjadj 31189 | Double adjoint. Theorem 3.11(iv) of [Beran] p. 106. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
β’ (π β dom adjβ β (adjββ(adjββπ)) = π) | ||
Theorem | adjvalval 31190* | 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.) |
β’ ((π β dom adjβ β§ π΄ β β) β ((adjββπ)βπ΄) = (β©π€ β β βπ₯ β β ((πβπ₯) Β·ih π΄) = (π₯ Β·ih π€))) | ||
Theorem | unopadj2 31191 | 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.) |
β’ (π β UniOp β (adjββπ) = β‘π) | ||
Theorem | hmopadj 31192 | A Hermitian operator is self-adjoint. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
β’ (π β HrmOp β (adjββπ) = π) | ||
Theorem | hmdmadj 31193 | Every Hermitian operator has an adjoint. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
β’ (π β HrmOp β π β dom adjβ) | ||
Theorem | hmopadj2 31194 | 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.) |
β’ (π β dom adjβ β (π β HrmOp β (adjββπ) = π)) | ||
Theorem | hmoplin 31195 | A Hermitian operator is linear. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
β’ (π β HrmOp β π β LinOp) | ||
Theorem | brafval 31196* | The bra of a vector, expressed as β¨π΄ β£ in Dirac notation. See df-bra 31103. (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
β’ (π΄ β β β (braβπ΄) = (π₯ β β β¦ (π₯ Β·ih π΄))) | ||
Theorem | braval 31197 | A bra-ket juxtaposition, expressed as β¨π΄ β£ π΅β© in Dirac notation, equals the inner product of the vectors. Based on definition of bra in [Prugovecki] p. 186. (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β ((braβπ΄)βπ΅) = (π΅ Β·ih π΄)) | ||
Theorem | braadd 31198 | Linearity property of bra for addition. (Contributed by NM, 23-May-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((braβπ΄)β(π΅ +β πΆ)) = (((braβπ΄)βπ΅) + ((braβπ΄)βπΆ))) | ||
Theorem | bramul 31199 | Linearity property of bra for multiplication. (Contributed by NM, 23-May-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((braβπ΄)β(π΅ Β·β πΆ)) = (π΅ Β· ((braβπ΄)βπΆ))) | ||
Theorem | brafn 31200 | The bra function is a functional. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
β’ (π΄ β β β (braβπ΄): ββΆβ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |