Home | Metamath
Proof Explorer Theorem List (p. 306 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hosubcl 30501 | Mapping of difference of Hilbert space operators. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (๐ โop ๐): โโถ โ) | ||
Theorem | hoaddcom 30502 | Commutativity of sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (๐ +op ๐) = (๐ +op ๐)) | ||
Theorem | hodsi 30503 | Relationship between Hilbert space operator difference and sum. (Contributed by NM, 17-Nov-2000.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ โop ๐) = ๐ โ (๐ +op ๐) = ๐ ) | ||
Theorem | hoaddassi 30504 | Associativity of sum of Hilbert space operators. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ +op ๐) +op ๐) = (๐ +op (๐ +op ๐)) | ||
Theorem | hoadd12i 30505 | Commutative/associative law for Hilbert space operator sum that swaps the first two terms. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ +op (๐ +op ๐)) = (๐ +op (๐ +op ๐)) | ||
Theorem | hoadd32i 30506 | Commutative/associative law for Hilbert space operator sum that swaps the second and third terms. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ +op ๐) +op ๐) = ((๐ +op ๐) +op ๐) | ||
Theorem | hocadddiri 30507 | Distributive law for Hilbert space operator sum. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ +op ๐) โ ๐) = ((๐ โ ๐) +op (๐ โ ๐)) | ||
Theorem | hocsubdiri 30508 | Distributive law for Hilbert space operator difference. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ โop ๐) โ ๐) = ((๐ โ ๐) โop (๐ โ ๐)) | ||
Theorem | ho2coi 30509 | Double composition of Hilbert space operators. (Contributed by NM, 1-Dec-2000.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ด โ โ โ (((๐ โ ๐) โ ๐)โ๐ด) = (๐ โ(๐โ(๐โ๐ด)))) | ||
Theorem | hoaddass 30510 | Associativity of sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ((๐ : โโถ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ ((๐ +op ๐) +op ๐) = (๐ +op (๐ +op ๐))) | ||
Theorem | hoadd32 30511 | 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 30512 | 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 30513 | Distributive law for Hilbert space operator difference. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
โข ((๐ : โโถ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ ((๐ โop ๐) โ ๐) = ((๐ โ ๐) โop (๐ โ ๐))) | ||
Theorem | hoaddid1i 30514 | Sum of a Hilbert space operator with the zero operator. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ โ โข (๐ +op 0hop ) = ๐ | ||
Theorem | hodidi 30515 | Difference of a Hilbert space operator from itself. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
โข ๐: โโถ โ โ โข (๐ โop ๐) = 0hop | ||
Theorem | ho0coi 30516 | Composition of the zero operator and a Hilbert space operator. (Contributed by NM, 9-Aug-2006.) (New usage is discouraged.) |
โข ๐: โโถ โ โ โข ( 0hop โ ๐) = 0hop | ||
Theorem | hoid1i 30517 | Composition of Hilbert space operator with unit identity. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ โ โข (๐ โ Iop ) = ๐ | ||
Theorem | hoid1ri 30518 | Composition of Hilbert space operator with unit identity. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ โ โข ( Iop โ ๐) = ๐ | ||
Theorem | hoaddid1 30519 | Sum of a Hilbert space operator with the zero operator. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ (๐ +op 0hop ) = ๐) | ||
Theorem | hodid 30520 | Difference of a Hilbert space operator from itself. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ (๐ โop ๐) = 0hop ) | ||
Theorem | hon0 30521 | A Hilbert space operator is not empty. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ ยฌ ๐ = โ ) | ||
Theorem | hodseqi 30522 | Subtraction and addition of equal Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ +op (๐ โop ๐)) = ๐ | ||
Theorem | ho0subi 30523 | 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 30524 | Relationship between Hilbert operator addition and subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ +op (-1 ยทop ๐)) = (๐ โop ๐) | ||
Theorem | ho0sub 30525 | 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 30526 | The zero operator subtracted from a Hilbert space operator. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ (๐ โop 0hop ) = ๐) | ||
Theorem | honegsub 30527 | Relationship between Hilbert space operator addition and subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (๐ +op (-1 ยทop ๐)) = (๐ โop ๐)) | ||
Theorem | homulid2 30528 | An operator equals its scalar product with one. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ (1 ยทop ๐) = ๐) | ||
Theorem | homco1 30529 | Associative law for scalar product and composition of operators. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ ((๐ด ยทop ๐) โ ๐) = (๐ด ยทop (๐ โ ๐))) | ||
Theorem | homulass 30530 | Scalar product associative law for Hilbert space operators. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ) โ ((๐ด ยท ๐ต) ยทop ๐) = (๐ด ยทop (๐ต ยทop ๐))) | ||
Theorem | hoadddi 30531 | 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 30532 | 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 30533 | 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 30534 | Double negative of a Hilbert space operator. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ (-1 ยทop (-1 ยทop ๐)) = ๐) | ||
Theorem | hosubneg 30535 | Relationship between operator subtraction and negative. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (๐ โop (-1 ยทop ๐)) = (๐ +op ๐)) | ||
Theorem | hosubdi 30536 | Scalar product distributive law for operator difference. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ (๐ด ยทop (๐ โop ๐)) = ((๐ด ยทop ๐) โop (๐ด ยทop ๐))) | ||
Theorem | honegdi 30537 | 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 30538 | Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (-1 ยทop (๐ โop ๐)) = ((-1 ยทop ๐) +op ๐)) | ||
Theorem | honegsubdi2 30539 | Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (-1 ยทop (๐ โop ๐)) = (๐ โop ๐)) | ||
Theorem | hosubsub2 30540 | Law for double subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ (๐ โop (๐ โop ๐)) = (๐ +op (๐ โop ๐))) | ||
Theorem | hosub4 30541 | 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 30542 | 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 30543 | 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 30544 | 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 30545 | Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ (๐ โop (๐ โop ๐)) = ((๐ โop ๐) +op ๐)) | ||
Theorem | hosubsub4 30546 | Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ ((๐ โop ๐) โop ๐) = (๐ โop (๐ +op ๐))) | ||
Theorem | ho2times 30547 | Two times a Hilbert space operator. (Contributed by NM, 26-Aug-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ (2 ยทop ๐) = (๐ +op ๐)) | ||
Theorem | hoaddsubassi 30548 | 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 30549 | 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 30550 | 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 30551 | 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 30552 | Hilbert space operator cancellation law. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ +op ๐) โop ๐) = ๐ | ||
Theorem | honpcani 30553 | Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ โop ๐) +op ๐) = ๐ | ||
Theorem | hosubeq0i 30554 | 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 30555 | Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ โop ๐) +op (๐ โop ๐)) = (๐ โop ๐) | ||
Theorem | ho01i 30556* | 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 30557* | 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 30558* | 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 30559* | 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 30560* | Every Hilbert space operator has at most one adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
โข โ*๐ข(๐ข: โโถ โ โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)) | ||
Theorem | adjsym 30561* | Symmetry property of an adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ))) | ||
Theorem | eigrei 30562 | 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 30563 | 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 30564 | 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 30565 | 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 30566 | 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 30567* | 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 30568* | 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 30569* | Define the set of linear operators on Hilbert space. (See df-hosum 30458 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
โข LinOp = {๐ก โ ( โ โm โ) โฃ โ๐ฅ โ โ โ๐ฆ โ โ โ๐ง โ โ (๐กโ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐กโ๐ฆ)) +โ (๐กโ๐ง))} | ||
Definition | df-bdop 30570 | Define the set of bounded linear Hilbert space operators. (See df-hosum 30458 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
โข BndLinOp = {๐ก โ LinOp โฃ (normopโ๐ก) < +โ} | ||
Definition | df-unop 30571* | 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 30572* | 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 30573* | 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 30574 | 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 30575* | 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 30576* | Define the set of linear functionals on Hilbert space. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
โข LinFn = {๐ก โ (โ โm โ) โฃ โ๐ฅ โ โ โ๐ฆ โ โ โ๐ง โ โ (๐กโ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยท (๐กโ๐ฆ)) + (๐กโ๐ง))} | ||
Definition | df-adjh 30577* | 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 30811) 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 30578* |
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 30672. The reversal of the inner product
arguments not only makes
the bra-ket behavior consistent with physics literature (see comments
under ax-his3 29812) but is also required in order for the
associative law
kbass2 30845 to work.
Our definition of bra and the associated outer product df-kb 30579 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 30579, under the 17-May-2006 entry. (Contributed by NM, 15-May-2006.) (New usage is discouraged.) |
โข bra = (๐ฅ โ โ โฆ (๐ฆ โ โ โฆ (๐ฆ ยทih ๐ฅ))) | ||
Definition | df-kb 30579* | 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 30578, 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 30580* | 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 30581* | Define the eigenvector function. Theorem eleigveccl 30687 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 30582* | Define the eigenvalue function. The range of eigvalโ๐ is the set of eigenvalues of Hilbert space operator ๐. Theorem eigvalcl 30689 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 30583* | 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 30584* | 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 30585* | 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 30586* | 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 30587 | A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
โข (๐ โ LinOp โ ๐: โโถ โ) | ||
Theorem | elbdop 30588 | 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 30589 | A bounded linear Hilbert space operator is a linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
โข (๐ โ BndLinOp โ ๐ โ LinOp) | ||
Theorem | bdopf 30590 | A bounded linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) |
โข (๐ โ BndLinOp โ ๐: โโถ โ) | ||
Theorem | nmopsetretALT 30591* | The set in the supremum of the operator norm definition df-nmop 30567 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
โข (๐: โโถ โ โ {๐ฅ โฃ โ๐ฆ โ โ ((normโโ๐ฆ) โค 1 โง ๐ฅ = (normโโ(๐โ๐ฆ)))} โ โ) | ||
Theorem | nmopsetretHIL 30592* | The set in the supremum of the operator norm definition df-nmop 30567 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ {๐ฅ โฃ โ๐ฆ โ โ ((normโโ๐ฆ) โค 1 โง ๐ฅ = (normโโ(๐โ๐ฆ)))} โ โ) | ||
Theorem | nmopsetn0 30593* | The set in the supremum of the operator norm definition df-nmop 30567 is nonempty. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
โข (normโโ(๐โ0โ)) โ {๐ฅ โฃ โ๐ฆ โ โ ((normโโ๐ฆ) โค 1 โง ๐ฅ = (normโโ(๐โ๐ฆ)))} | ||
Theorem | nmopxr 30594 | The norm of a Hilbert space operator is an extended real. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ (normopโ๐) โ โ*) | ||
Theorem | nmoprepnf 30595 | 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 30596 | The norm of a Hilbert space operator is not minus infinity. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ -โ < (normopโ๐)) | ||
Theorem | nmopreltpnf 30597 | 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 30598 | The norm of a bounded operator is a real number. (Contributed by NM, 29-Jan-2006.) (New usage is discouraged.) |
โข (๐ โ BndLinOp โ (normopโ๐) โ โ) | ||
Theorem | elbdop2 30599 | Property defining a bounded linear Hilbert space operator. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
โข (๐ โ BndLinOp โ (๐ โ LinOp โง (normopโ๐) โ โ)) | ||
Theorem | elunop 30600* | Property defining a unitary Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
โข (๐ โ UniOp โ (๐: โโontoโ โ โง โ๐ฅ โ โ โ๐ฆ โ โ ((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = (๐ฅ ยทih ๐ฆ))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |