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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hoeqi 30501* | Equality of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (โ๐ฅ โ โ (๐โ๐ฅ) = (๐โ๐ฅ) โ ๐ = ๐) | ||
Theorem | hoscli 30502 | Closure of Hilbert space operator sum. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ด โ โ โ ((๐ +op ๐)โ๐ด) โ โ) | ||
Theorem | hodcli 30503 | Closure of Hilbert space operator difference. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ด โ โ โ ((๐ โop ๐)โ๐ด) โ โ) | ||
Theorem | hocoi 30504 | Composition of Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ด โ โ โ ((๐ โ ๐)โ๐ด) = (๐โ(๐โ๐ด))) | ||
Theorem | hococli 30505 | Closure of composition of Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ด โ โ โ ((๐ โ ๐)โ๐ด) โ โ) | ||
Theorem | hocofi 30506 | Mapping of composition of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ โ ๐): โโถ โ | ||
Theorem | hocofni 30507 | Functionality of composition of Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ โ ๐) Fn โ | ||
Theorem | hoaddcli 30508 | Mapping of sum of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ +op ๐): โโถ โ | ||
Theorem | hosubcli 30509 | Mapping of difference of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ โop ๐): โโถ โ | ||
Theorem | hoaddfni 30510 | Functionality of sum of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ +op ๐) Fn โ | ||
Theorem | hosubfni 30511 | Functionality of difference of Hilbert space operators. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ โop ๐) Fn โ | ||
Theorem | hoaddcomi 30512 | Commutativity of sum of Hilbert space operators. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ +op ๐) = (๐ +op ๐) | ||
Theorem | hosubcl 30513 | Mapping of difference of Hilbert space operators. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (๐ โop ๐): โโถ โ) | ||
Theorem | hoaddcom 30514 | Commutativity of sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (๐ +op ๐) = (๐ +op ๐)) | ||
Theorem | hodsi 30515 | Relationship between Hilbert space operator difference and sum. (Contributed by NM, 17-Nov-2000.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ โop ๐) = ๐ โ (๐ +op ๐) = ๐ ) | ||
Theorem | hoaddassi 30516 | Associativity of sum of Hilbert space operators. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ +op ๐) +op ๐) = (๐ +op (๐ +op ๐)) | ||
Theorem | hoadd12i 30517 | 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 30518 | 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 30519 | Distributive law for Hilbert space operator sum. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ +op ๐) โ ๐) = ((๐ โ ๐) +op (๐ โ ๐)) | ||
Theorem | hocsubdiri 30520 | Distributive law for Hilbert space operator difference. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ โop ๐) โ ๐) = ((๐ โ ๐) โop (๐ โ ๐)) | ||
Theorem | ho2coi 30521 | Double composition of Hilbert space operators. (Contributed by NM, 1-Dec-2000.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ด โ โ โ (((๐ โ ๐) โ ๐)โ๐ด) = (๐ โ(๐โ(๐โ๐ด)))) | ||
Theorem | hoaddass 30522 | Associativity of sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ((๐ : โโถ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ ((๐ +op ๐) +op ๐) = (๐ +op (๐ +op ๐))) | ||
Theorem | hoadd32 30523 | 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 30524 | 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 30525 | Distributive law for Hilbert space operator difference. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
โข ((๐ : โโถ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ ((๐ โop ๐) โ ๐) = ((๐ โ ๐) โop (๐ โ ๐))) | ||
Theorem | hoaddid1i 30526 | Sum of a Hilbert space operator with the zero operator. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ โ โข (๐ +op 0hop ) = ๐ | ||
Theorem | hodidi 30527 | Difference of a Hilbert space operator from itself. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
โข ๐: โโถ โ โ โข (๐ โop ๐) = 0hop | ||
Theorem | ho0coi 30528 | Composition of the zero operator and a Hilbert space operator. (Contributed by NM, 9-Aug-2006.) (New usage is discouraged.) |
โข ๐: โโถ โ โ โข ( 0hop โ ๐) = 0hop | ||
Theorem | hoid1i 30529 | Composition of Hilbert space operator with unit identity. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ โ โข (๐ โ Iop ) = ๐ | ||
Theorem | hoid1ri 30530 | Composition of Hilbert space operator with unit identity. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ โ โข ( Iop โ ๐) = ๐ | ||
Theorem | hoaddid1 30531 | Sum of a Hilbert space operator with the zero operator. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ (๐ +op 0hop ) = ๐) | ||
Theorem | hodid 30532 | Difference of a Hilbert space operator from itself. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ (๐ โop ๐) = 0hop ) | ||
Theorem | hon0 30533 | A Hilbert space operator is not empty. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ ยฌ ๐ = โ ) | ||
Theorem | hodseqi 30534 | Subtraction and addition of equal Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ +op (๐ โop ๐)) = ๐ | ||
Theorem | ho0subi 30535 | 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 30536 | Relationship between Hilbert operator addition and subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ +op (-1 ยทop ๐)) = (๐ โop ๐) | ||
Theorem | ho0sub 30537 | 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 30538 | The zero operator subtracted from a Hilbert space operator. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ (๐ โop 0hop ) = ๐) | ||
Theorem | honegsub 30539 | Relationship between Hilbert space operator addition and subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (๐ +op (-1 ยทop ๐)) = (๐ โop ๐)) | ||
Theorem | homulid2 30540 | An operator equals its scalar product with one. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ (1 ยทop ๐) = ๐) | ||
Theorem | homco1 30541 | Associative law for scalar product and composition of operators. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ ((๐ด ยทop ๐) โ ๐) = (๐ด ยทop (๐ โ ๐))) | ||
Theorem | homulass 30542 | Scalar product associative law for Hilbert space operators. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ) โ ((๐ด ยท ๐ต) ยทop ๐) = (๐ด ยทop (๐ต ยทop ๐))) | ||
Theorem | hoadddi 30543 | 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 30544 | 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 30545 | 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 30546 | Double negative of a Hilbert space operator. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ (-1 ยทop (-1 ยทop ๐)) = ๐) | ||
Theorem | hosubneg 30547 | Relationship between operator subtraction and negative. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (๐ โop (-1 ยทop ๐)) = (๐ +op ๐)) | ||
Theorem | hosubdi 30548 | Scalar product distributive law for operator difference. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ (๐ด ยทop (๐ โop ๐)) = ((๐ด ยทop ๐) โop (๐ด ยทop ๐))) | ||
Theorem | honegdi 30549 | 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 30550 | Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (-1 ยทop (๐ โop ๐)) = ((-1 ยทop ๐) +op ๐)) | ||
Theorem | honegsubdi2 30551 | Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (-1 ยทop (๐ โop ๐)) = (๐ โop ๐)) | ||
Theorem | hosubsub2 30552 | Law for double subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ (๐ โop (๐ โop ๐)) = (๐ +op (๐ โop ๐))) | ||
Theorem | hosub4 30553 | 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 30554 | 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 30555 | 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 30556 | 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 30557 | Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ (๐ โop (๐ โop ๐)) = ((๐ โop ๐) +op ๐)) | ||
Theorem | hosubsub4 30558 | Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ ((๐ โop ๐) โop ๐) = (๐ โop (๐ +op ๐))) | ||
Theorem | ho2times 30559 | Two times a Hilbert space operator. (Contributed by NM, 26-Aug-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ (2 ยทop ๐) = (๐ +op ๐)) | ||
Theorem | hoaddsubassi 30560 | 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 30561 | 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 30562 | 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 30563 | 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 30564 | Hilbert space operator cancellation law. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ +op ๐) โop ๐) = ๐ | ||
Theorem | honpcani 30565 | Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ โop ๐) +op ๐) = ๐ | ||
Theorem | hosubeq0i 30566 | 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 30567 | Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ โop ๐) +op (๐ โop ๐)) = (๐ โop ๐) | ||
Theorem | ho01i 30568* | 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 30569* | 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 30570* | 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 30571* | 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 30572* | Every Hilbert space operator has at most one adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
โข โ*๐ข(๐ข: โโถ โ โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)) | ||
Theorem | adjsym 30573* | Symmetry property of an adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ))) | ||
Theorem | eigrei 30574 | 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 30575 | 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 30576 | 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 30577 | 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 30578 | 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 30579* | 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 30580* | 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 30581* | Define the set of linear operators on Hilbert space. (See df-hosum 30470 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
โข LinOp = {๐ก โ ( โ โm โ) โฃ โ๐ฅ โ โ โ๐ฆ โ โ โ๐ง โ โ (๐กโ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐กโ๐ฆ)) +โ (๐กโ๐ง))} | ||
Definition | df-bdop 30582 | Define the set of bounded linear Hilbert space operators. (See df-hosum 30470 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
โข BndLinOp = {๐ก โ LinOp โฃ (normopโ๐ก) < +โ} | ||
Definition | df-unop 30583* | 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 30584* | 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 30585* | 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 30586 | 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 30587* | 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 30588* | Define the set of linear functionals on Hilbert space. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
โข LinFn = {๐ก โ (โ โm โ) โฃ โ๐ฅ โ โ โ๐ฆ โ โ โ๐ง โ โ (๐กโ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยท (๐กโ๐ฆ)) + (๐กโ๐ง))} | ||
Definition | df-adjh 30589* | 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 30823) 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 30590* |
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 30684. The reversal of the inner product
arguments not only makes
the bra-ket behavior consistent with physics literature (see comments
under ax-his3 29824) but is also required in order for the
associative law
kbass2 30857 to work.
Our definition of bra and the associated outer product df-kb 30591 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 30591, under the 17-May-2006 entry. (Contributed by NM, 15-May-2006.) (New usage is discouraged.) |
โข bra = (๐ฅ โ โ โฆ (๐ฆ โ โ โฆ (๐ฆ ยทih ๐ฅ))) | ||
Definition | df-kb 30591* | 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 30590, 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 30592* | 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 30593* | Define the eigenvector function. Theorem eleigveccl 30699 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 30594* | Define the eigenvalue function. The range of eigvalโ๐ is the set of eigenvalues of Hilbert space operator ๐. Theorem eigvalcl 30701 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 30595* | 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 30596* | 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 30597* | 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 30598* | 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 30599 | A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
โข (๐ โ LinOp โ ๐: โโถ โ) | ||
Theorem | elbdop 30600 | 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โ๐) < +โ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |