![]() |
Metamath
Proof Explorer Theorem List (p. 314 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ho2coi 31301 | Double composition of Hilbert space operators. (Contributed by NM, 1-Dec-2000.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ด โ โ โ (((๐ โ ๐) โ ๐)โ๐ด) = (๐ โ(๐โ(๐โ๐ด)))) | ||
Theorem | hoaddass 31302 | Associativity of sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ((๐ : โโถ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ ((๐ +op ๐) +op ๐) = (๐ +op (๐ +op ๐))) | ||
Theorem | hoadd32 31303 | Commutative/associative law for Hilbert space operator sum that swaps the second and third terms. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ((๐ : โโถ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ ((๐ +op ๐) +op ๐) = ((๐ +op ๐) +op ๐)) | ||
Theorem | hoadd4 31304 | Rearrangement of 4 terms in a sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข (((๐ : โโถ โ โง ๐: โโถ โ) โง (๐: โโถ โ โง ๐: โโถ โ)) โ ((๐ +op ๐) +op (๐ +op ๐)) = ((๐ +op ๐) +op (๐ +op ๐))) | ||
Theorem | hocsubdir 31305 | Distributive law for Hilbert space operator difference. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
โข ((๐ : โโถ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ ((๐ โop ๐) โ ๐) = ((๐ โ ๐) โop (๐ โ ๐))) | ||
Theorem | hoaddridi 31306 | Sum of a Hilbert space operator with the zero operator. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ โ โข (๐ +op 0hop ) = ๐ | ||
Theorem | hodidi 31307 | Difference of a Hilbert space operator from itself. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
โข ๐: โโถ โ โ โข (๐ โop ๐) = 0hop | ||
Theorem | ho0coi 31308 | Composition of the zero operator and a Hilbert space operator. (Contributed by NM, 9-Aug-2006.) (New usage is discouraged.) |
โข ๐: โโถ โ โ โข ( 0hop โ ๐) = 0hop | ||
Theorem | hoid1i 31309 | Composition of Hilbert space operator with unit identity. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ โ โข (๐ โ Iop ) = ๐ | ||
Theorem | hoid1ri 31310 | Composition of Hilbert space operator with unit identity. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ โ โข ( Iop โ ๐) = ๐ | ||
Theorem | hoaddrid 31311 | Sum of a Hilbert space operator with the zero operator. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ (๐ +op 0hop ) = ๐) | ||
Theorem | hodid 31312 | Difference of a Hilbert space operator from itself. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ (๐ โop ๐) = 0hop ) | ||
Theorem | hon0 31313 | A Hilbert space operator is not empty. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ ยฌ ๐ = โ ) | ||
Theorem | hodseqi 31314 | Subtraction and addition of equal Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ +op (๐ โop ๐)) = ๐ | ||
Theorem | ho0subi 31315 | Subtraction of Hilbert space operators expressed in terms of difference from zero. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ โop ๐) = (๐ +op ( 0hop โop ๐)) | ||
Theorem | honegsubi 31316 | Relationship between Hilbert operator addition and subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ +op (-1 ยทop ๐)) = (๐ โop ๐) | ||
Theorem | ho0sub 31317 | Subtraction of Hilbert space operators expressed in terms of difference from zero. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (๐ โop ๐) = (๐ +op ( 0hop โop ๐))) | ||
Theorem | hosubid1 31318 | The zero operator subtracted from a Hilbert space operator. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ (๐ โop 0hop ) = ๐) | ||
Theorem | honegsub 31319 | Relationship between Hilbert space operator addition and subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (๐ +op (-1 ยทop ๐)) = (๐ โop ๐)) | ||
Theorem | homullid 31320 | An operator equals its scalar product with one. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ (1 ยทop ๐) = ๐) | ||
Theorem | homco1 31321 | Associative law for scalar product and composition of operators. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ ((๐ด ยทop ๐) โ ๐) = (๐ด ยทop (๐ โ ๐))) | ||
Theorem | homulass 31322 | Scalar product associative law for Hilbert space operators. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ) โ ((๐ด ยท ๐ต) ยทop ๐) = (๐ด ยทop (๐ต ยทop ๐))) | ||
Theorem | hoadddi 31323 | Scalar product distributive law for Hilbert space operators. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ (๐ด ยทop (๐ +op ๐)) = ((๐ด ยทop ๐) +op (๐ด ยทop ๐))) | ||
Theorem | hoadddir 31324 | Scalar product reverse distributive law for Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ) โ ((๐ด + ๐ต) ยทop ๐) = ((๐ด ยทop ๐) +op (๐ต ยทop ๐))) | ||
Theorem | homul12 31325 | Swap first and second factors in a nested operator scalar product. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ) โ (๐ด ยทop (๐ต ยทop ๐)) = (๐ต ยทop (๐ด ยทop ๐))) | ||
Theorem | honegneg 31326 | Double negative of a Hilbert space operator. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ (-1 ยทop (-1 ยทop ๐)) = ๐) | ||
Theorem | hosubneg 31327 | Relationship between operator subtraction and negative. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (๐ โop (-1 ยทop ๐)) = (๐ +op ๐)) | ||
Theorem | hosubdi 31328 | Scalar product distributive law for operator difference. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ (๐ด ยทop (๐ โop ๐)) = ((๐ด ยทop ๐) โop (๐ด ยทop ๐))) | ||
Theorem | honegdi 31329 | Distribution of negative over addition. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (-1 ยทop (๐ +op ๐)) = ((-1 ยทop ๐) +op (-1 ยทop ๐))) | ||
Theorem | honegsubdi 31330 | Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (-1 ยทop (๐ โop ๐)) = ((-1 ยทop ๐) +op ๐)) | ||
Theorem | honegsubdi2 31331 | Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (-1 ยทop (๐ โop ๐)) = (๐ โop ๐)) | ||
Theorem | hosubsub2 31332 | Law for double subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ (๐ โop (๐ โop ๐)) = (๐ +op (๐ โop ๐))) | ||
Theorem | hosub4 31333 | Rearrangement of 4 terms in a mixed addition and subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข (((๐ : โโถ โ โง ๐: โโถ โ) โง (๐: โโถ โ โง ๐: โโถ โ)) โ ((๐ +op ๐) โop (๐ +op ๐)) = ((๐ โop ๐) +op (๐ โop ๐))) | ||
Theorem | hosubadd4 31334 | Rearrangement of 4 terms in a mixed addition and subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข (((๐ : โโถ โ โง ๐: โโถ โ) โง (๐: โโถ โ โง ๐: โโถ โ)) โ ((๐ โop ๐) โop (๐ โop ๐)) = ((๐ +op ๐) โop (๐ +op ๐))) | ||
Theorem | hoaddsubass 31335 | Associative-type law for addition and subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ ((๐ +op ๐) โop ๐) = (๐ +op (๐ โop ๐))) | ||
Theorem | hoaddsub 31336 | Law for operator addition and subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ ((๐ +op ๐) โop ๐) = ((๐ โop ๐) +op ๐)) | ||
Theorem | hosubsub 31337 | Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ (๐ โop (๐ โop ๐)) = ((๐ โop ๐) +op ๐)) | ||
Theorem | hosubsub4 31338 | Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ ((๐ โop ๐) โop ๐) = (๐ โop (๐ +op ๐))) | ||
Theorem | ho2times 31339 | Two times a Hilbert space operator. (Contributed by NM, 26-Aug-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ (2 ยทop ๐) = (๐ +op ๐)) | ||
Theorem | hoaddsubassi 31340 | Associativity of sum and difference of Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ +op ๐) โop ๐) = (๐ +op (๐ โop ๐)) | ||
Theorem | hoaddsubi 31341 | Law for sum and difference of Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ +op ๐) โop ๐) = ((๐ โop ๐) +op ๐) | ||
Theorem | hosd1i 31342 | Hilbert space operator sum expressed in terms of difference. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ +op ๐) = (๐ โop ( 0hop โop ๐)) | ||
Theorem | hosd2i 31343 | Hilbert space operator sum expressed in terms of difference. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ +op ๐) = (๐ โop ((๐ โop ๐) โop ๐)) | ||
Theorem | hopncani 31344 | Hilbert space operator cancellation law. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ +op ๐) โop ๐) = ๐ | ||
Theorem | honpcani 31345 | Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ โop ๐) +op ๐) = ๐ | ||
Theorem | hosubeq0i 31346 | If the difference between two operators is zero, they are equal. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ โop ๐) = 0hop โ ๐ = ๐) | ||
Theorem | honpncani 31347 | Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ โop ๐) +op (๐ โop ๐)) = (๐ โop ๐) | ||
Theorem | ho01i 31348* | A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S8) of [Beran] p. 95. (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.) |
โข ๐: โโถ โ โ โข (โ๐ฅ โ โ โ๐ฆ โ โ ((๐โ๐ฅ) ยทih ๐ฆ) = 0 โ ๐ = 0hop ) | ||
Theorem | ho02i 31349* | A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S10) of [Beran] p. 95. (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.) |
โข ๐: โโถ โ โ โข (โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = 0 โ ๐ = 0hop ) | ||
Theorem | hoeq1 31350* | A condition implying that two Hilbert space operators are equal. Lemma 3.2(S9) of [Beran] p. 95. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (โ๐ฅ โ โ โ๐ฆ โ โ ((๐โ๐ฅ) ยทih ๐ฆ) = ((๐โ๐ฅ) ยทih ๐ฆ) โ ๐ = ๐)) | ||
Theorem | hoeq2 31351* | A condition implying that two Hilbert space operators are equal. Lemma 3.2(S11) of [Beran] p. 95. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = (๐ฅ ยทih (๐โ๐ฆ)) โ ๐ = ๐)) | ||
Theorem | adjmo 31352* | Every Hilbert space operator has at most one adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
โข โ*๐ข(๐ข: โโถ โ โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)) | ||
Theorem | adjsym 31353* | Symmetry property of an adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ))) | ||
Theorem | eigrei 31354 | A necessary and sufficient condition (that holds when ๐ is a Hermitian operator) for an eigenvalue ๐ต to be real. Generalization of Equation 1.30 of [Hughes] p. 49. (Contributed by NM, 21-Jan-2005.) (New usage is discouraged.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ) โ ((๐ด ยทih (๐โ๐ด)) = ((๐โ๐ด) ยทih ๐ด) โ ๐ต โ โ)) | ||
Theorem | eigre 31355 | A necessary and sufficient condition (that holds when ๐ is a Hermitian operator) for an eigenvalue ๐ต to be real. Generalization of Equation 1.30 of [Hughes] p. 49. (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ ((๐ด ยทih (๐โ๐ด)) = ((๐โ๐ด) ยทih ๐ด) โ ๐ต โ โ)) | ||
Theorem | eigposi 31356 | A sufficient condition (first conjunct pair, that holds when ๐ is a positive operator) for an eigenvalue ๐ต (second conjunct pair) to be nonnegative. Remark (ii) in [Hughes] p. 137. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((((๐ด ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ (๐ต โ โ โง 0 โค ๐ต)) | ||
Theorem | eigorthi 31357 | A necessary and sufficient condition (that holds when ๐ is a Hermitian operator) for two eigenvectors ๐ด and ๐ต to be orthogonal. Generalization of Equation 1.31 of [Hughes] p. 49. (Contributed by NM, 23-Jan-2005.) (New usage is discouraged.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ & โข ๐ท โ โ โ โข ((((๐โ๐ด) = (๐ถ ยทโ ๐ด) โง (๐โ๐ต) = (๐ท ยทโ ๐ต)) โง ๐ถ โ (โโ๐ท)) โ ((๐ด ยทih (๐โ๐ต)) = ((๐โ๐ด) ยทih ๐ต) โ (๐ด ยทih ๐ต) = 0)) | ||
Theorem | eigorth 31358 | A necessary and sufficient condition (that holds when ๐ is a Hermitian operator) for two eigenvectors ๐ด and ๐ต to be orthogonal. Generalization of Equation 1.31 of [Hughes] p. 49. (Contributed by NM, 23-Mar-2006.) (New usage is discouraged.) |
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (((๐โ๐ด) = (๐ถ ยทโ ๐ด) โง (๐โ๐ต) = (๐ท ยทโ ๐ต)) โง ๐ถ โ (โโ๐ท))) โ ((๐ด ยทih (๐โ๐ต)) = ((๐โ๐ด) ยทih ๐ต) โ (๐ด ยทih ๐ต) = 0)) | ||
Definition | df-nmop 31359* | Define the norm of a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
โข normop = (๐ก โ ( โ โm โ) โฆ sup({๐ฅ โฃ โ๐ง โ โ ((normโโ๐ง) โค 1 โง ๐ฅ = (normโโ(๐กโ๐ง)))}, โ*, < )) | ||
Definition | df-cnop 31360* | Define the set of continuous operators on Hilbert space. For every "epsilon" (๐ฆ) there is a "delta" (๐ง) such that... (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.) |
โข ContOp = {๐ก โ ( โ โm โ) โฃ โ๐ฅ โ โ โ๐ฆ โ โ+ โ๐ง โ โ+ โ๐ค โ โ ((normโโ(๐ค โโ ๐ฅ)) < ๐ง โ (normโโ((๐กโ๐ค) โโ (๐กโ๐ฅ))) < ๐ฆ)} | ||
Definition | df-lnop 31361* | Define the set of linear operators on Hilbert space. (See df-hosum 31250 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
โข LinOp = {๐ก โ ( โ โm โ) โฃ โ๐ฅ โ โ โ๐ฆ โ โ โ๐ง โ โ (๐กโ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐กโ๐ฆ)) +โ (๐กโ๐ง))} | ||
Definition | df-bdop 31362 | Define the set of bounded linear Hilbert space operators. (See df-hosum 31250 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
โข BndLinOp = {๐ก โ LinOp โฃ (normopโ๐ก) < +โ} | ||
Definition | df-unop 31363* | Define the set of unitary operators on Hilbert space. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
โข UniOp = {๐ก โฃ (๐ก: โโontoโ โ โง โ๐ฅ โ โ โ๐ฆ โ โ ((๐กโ๐ฅ) ยทih (๐กโ๐ฆ)) = (๐ฅ ยทih ๐ฆ))} | ||
Definition | df-hmop 31364* | 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.) |
โข HrmOp = {๐ก โ ( โ โm โ) โฃ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐กโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ)} | ||
Definition | df-nmfn 31365* | Define the norm of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
โข normfn = (๐ก โ (โ โm โ) โฆ sup({๐ฅ โฃ โ๐ง โ โ ((normโโ๐ง) โค 1 โง ๐ฅ = (absโ(๐กโ๐ง)))}, โ*, < )) | ||
Definition | df-nlfn 31366 | Define the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
โข null = (๐ก โ (โ โm โ) โฆ (โก๐ก โ {0})) | ||
Definition | df-cnfn 31367* | 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.) |
โข ContFn = {๐ก โ (โ โm โ) โฃ โ๐ฅ โ โ โ๐ฆ โ โ+ โ๐ง โ โ+ โ๐ค โ โ ((normโโ(๐ค โโ ๐ฅ)) < ๐ง โ (absโ((๐กโ๐ค) โ (๐กโ๐ฅ))) < ๐ฆ)} | ||
Definition | df-lnfn 31368* | Define the set of linear functionals on Hilbert space. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
โข LinFn = {๐ก โ (โ โm โ) โฃ โ๐ฅ โ โ โ๐ฆ โ โ โ๐ง โ โ (๐กโ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยท (๐กโ๐ฆ)) + (๐กโ๐ง))} | ||
Definition | df-adjh 31369* | 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 31603) 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 31370* |
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 31464. The reversal of the inner product
arguments not only makes
the bra-ket behavior consistent with physics literature (see comments
under ax-his3 30604) but is also required in order for the
associative law
kbass2 31637 to work.
Our definition of bra and the associated outer product df-kb 31371 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 31371, under the 17-May-2006 entry. (Contributed by NM, 15-May-2006.) (New usage is discouraged.) |
โข bra = (๐ฅ โ โ โฆ (๐ฆ โ โ โฆ (๐ฆ ยทih ๐ฅ))) | ||
Definition | df-kb 31371* | 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 31370, 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 31372* | 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 31373* | Define the eigenvector function. Theorem eleigveccl 31479 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 31374* | Define the eigenvalue function. The range of eigvalโ๐ is the set of eigenvalues of Hilbert space operator ๐. Theorem eigvalcl 31481 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 31375* | 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 31376* | 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 31377* | 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 31378* | 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 31379 | A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
โข (๐ โ LinOp โ ๐: โโถ โ) | ||
Theorem | elbdop 31380 | 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 31381 | A bounded linear Hilbert space operator is a linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
โข (๐ โ BndLinOp โ ๐ โ LinOp) | ||
Theorem | bdopf 31382 | A bounded linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) |
โข (๐ โ BndLinOp โ ๐: โโถ โ) | ||
Theorem | nmopsetretALT 31383* | The set in the supremum of the operator norm definition df-nmop 31359 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
โข (๐: โโถ โ โ {๐ฅ โฃ โ๐ฆ โ โ ((normโโ๐ฆ) โค 1 โง ๐ฅ = (normโโ(๐โ๐ฆ)))} โ โ) | ||
Theorem | nmopsetretHIL 31384* | The set in the supremum of the operator norm definition df-nmop 31359 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ {๐ฅ โฃ โ๐ฆ โ โ ((normโโ๐ฆ) โค 1 โง ๐ฅ = (normโโ(๐โ๐ฆ)))} โ โ) | ||
Theorem | nmopsetn0 31385* | The set in the supremum of the operator norm definition df-nmop 31359 is nonempty. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
โข (normโโ(๐โ0โ)) โ {๐ฅ โฃ โ๐ฆ โ โ ((normโโ๐ฆ) โค 1 โง ๐ฅ = (normโโ(๐โ๐ฆ)))} | ||
Theorem | nmopxr 31386 | The norm of a Hilbert space operator is an extended real. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ (normopโ๐) โ โ*) | ||
Theorem | nmoprepnf 31387 | 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 31388 | The norm of a Hilbert space operator is not minus infinity. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ -โ < (normopโ๐)) | ||
Theorem | nmopreltpnf 31389 | 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 31390 | The norm of a bounded operator is a real number. (Contributed by NM, 29-Jan-2006.) (New usage is discouraged.) |
โข (๐ โ BndLinOp โ (normopโ๐) โ โ) | ||
Theorem | elbdop2 31391 | Property defining a bounded linear Hilbert space operator. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
โข (๐ โ BndLinOp โ (๐ โ LinOp โง (normopโ๐) โ โ)) | ||
Theorem | elunop 31392* | Property defining a unitary Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
โข (๐ โ UniOp โ (๐: โโontoโ โ โง โ๐ฅ โ โ โ๐ฆ โ โ ((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = (๐ฅ ยทih ๐ฆ))) | ||
Theorem | elhmop 31393* | 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 31394 | A Hermitian operator is a Hilbert space operator (mapping). (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.) |
โข (๐ โ HrmOp โ ๐: โโถ โ) | ||
Theorem | hmopex 31395 | The class of Hermitian operators is a set. (Contributed by NM, 17-Aug-2006.) (New usage is discouraged.) |
โข HrmOp โ V | ||
Theorem | nmfnval 31396* | 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 31397* | The set in the supremum of the functional norm definition df-nmfn 31365 is a set of reals. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
โข (๐: โโถโ โ {๐ฅ โฃ โ๐ฆ โ โ ((normโโ๐ฆ) โค 1 โง ๐ฅ = (absโ(๐โ๐ฆ)))} โ โ) | ||
Theorem | nmfnsetn0 31398* | The set in the supremum of the functional norm definition df-nmfn 31365 is nonempty. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
โข (absโ(๐โ0โ)) โ {๐ฅ โฃ โ๐ฆ โ โ ((normโโ๐ฆ) โค 1 โง ๐ฅ = (absโ(๐โ๐ฆ)))} | ||
Theorem | nmfnxr 31399 | The norm of any Hilbert space functional is an extended real. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
โข (๐: โโถโ โ (normfnโ๐) โ โ*) | ||
Theorem | nmfnrepnf 31400 | 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โ๐) โ +โ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |