![]() |
Metamath
Proof Explorer Theorem List (p. 319 of 481) | < 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-30640) |
![]() (30641-32163) |
![]() (32164-48040) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cnlnadj 31801* | Every continuous linear operator has an adjoint. Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
β’ (π β (LinOp β© ContOp) β βπ‘ β (LinOp β© ContOp)βπ₯ β β βπ¦ β β ((πβπ₯) Β·ih π¦) = (π₯ Β·ih (π‘βπ¦))) | ||
Theorem | cnlnssadj 31802 | Every continuous linear Hilbert space operator has an adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
β’ (LinOp β© ContOp) β dom adjβ | ||
Theorem | bdopssadj 31803 | Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
β’ BndLinOp β dom adjβ | ||
Theorem | bdopadj 31804 | Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
β’ (π β BndLinOp β π β dom adjβ) | ||
Theorem | adjbdln 31805 | The adjoint of a bounded linear operator is a bounded linear operator. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
β’ (π β BndLinOp β (adjββπ) β BndLinOp) | ||
Theorem | adjbdlnb 31806 | An operator is bounded and linear iff its adjoint is. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
β’ (π β BndLinOp β (adjββπ) β BndLinOp) | ||
Theorem | adjbd1o 31807 | The mapping of adjoints of bounded linear operators is one-to-one onto. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
β’ (adjβ βΎ BndLinOp):BndLinOpβ1-1-ontoβBndLinOp | ||
Theorem | adjlnop 31808 | The adjoint of an operator is linear. Proposition 1 of [AkhiezerGlazman] p. 80. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.) |
β’ (π β dom adjβ β (adjββπ) β LinOp) | ||
Theorem | adjsslnop 31809 | Every operator with an adjoint is linear. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.) |
β’ dom adjβ β LinOp | ||
Theorem | nmopadjlei 31810 | Property of the norm of an adjoint. Part of proof of Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
β’ π β BndLinOp β β’ (π΄ β β β (normββ((adjββπ)βπ΄)) β€ ((normopβπ) Β· (normββπ΄))) | ||
Theorem | nmopadjlem 31811 | Lemma for nmopadji 31812. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
β’ π β BndLinOp β β’ (normopβ(adjββπ)) β€ (normopβπ) | ||
Theorem | nmopadji 31812 | Property of the norm of an adjoint. Theorem 3.11(v) of [Beran] p. 106. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
β’ π β BndLinOp β β’ (normopβ(adjββπ)) = (normopβπ) | ||
Theorem | adjeq0 31813 | An operator is zero iff its adjoint is zero. Theorem 3.11(i) of [Beran] p. 106. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
β’ (π = 0hop β (adjββπ) = 0hop ) | ||
Theorem | adjmul 31814 | The adjoint of the scalar product of an operator. Theorem 3.11(ii) of [Beran] p. 106. (Contributed by NM, 21-Feb-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π β dom adjβ) β (adjββ(π΄ Β·op π)) = ((ββπ΄) Β·op (adjββπ))) | ||
Theorem | adjadd 31815 | The adjoint of the sum of two operators. Theorem 3.11(iii) of [Beran] p. 106. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
β’ ((π β dom adjβ β§ π β dom adjβ) β (adjββ(π +op π)) = ((adjββπ) +op (adjββπ))) | ||
Theorem | nmoptrii 31816 | Triangle inequality for the norms of bounded linear operators. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ π β BndLinOp & β’ π β BndLinOp β β’ (normopβ(π +op π)) β€ ((normopβπ) + (normopβπ)) | ||
Theorem | nmopcoi 31817 | Upper bound for the norm of the composition of two bounded linear operators. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ π β BndLinOp & β’ π β BndLinOp β β’ (normopβ(π β π)) β€ ((normopβπ) Β· (normopβπ)) | ||
Theorem | bdophsi 31818 | The sum of two bounded linear operators is a bounded linear operator. (Contributed by NM, 9-Mar-2006.) (New usage is discouraged.) |
β’ π β BndLinOp & β’ π β BndLinOp β β’ (π +op π) β BndLinOp | ||
Theorem | bdophdi 31819 | The difference between two bounded linear operators is bounded. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ π β BndLinOp & β’ π β BndLinOp β β’ (π βop π) β BndLinOp | ||
Theorem | bdopcoi 31820 | The composition of two bounded linear operators is bounded. (Contributed by NM, 9-Mar-2006.) (New usage is discouraged.) |
β’ π β BndLinOp & β’ π β BndLinOp β β’ (π β π) β BndLinOp | ||
Theorem | nmoptri2i 31821 | Triangle-type inequality for the norms of bounded linear operators. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ π β BndLinOp & β’ π β BndLinOp β β’ ((normopβπ) β (normopβπ)) β€ (normopβ(π +op π)) | ||
Theorem | adjcoi 31822 | The adjoint of a composition of bounded linear operators. Theorem 3.11(viii) of [Beran] p. 106. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ π β BndLinOp & β’ π β BndLinOp β β’ (adjββ(π β π)) = ((adjββπ) β (adjββπ)) | ||
Theorem | nmopcoadji 31823 | The norm of an operator composed with its adjoint. Part of Theorem 3.11(vi) of [Beran] p. 106. (Contributed by NM, 8-Mar-2006.) (New usage is discouraged.) |
β’ π β BndLinOp β β’ (normopβ((adjββπ) β π)) = ((normopβπ)β2) | ||
Theorem | nmopcoadj2i 31824 | The norm of an operator composed with its adjoint. Part of Theorem 3.11(vi) of [Beran] p. 106. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ π β BndLinOp β β’ (normopβ(π β (adjββπ))) = ((normopβπ)β2) | ||
Theorem | nmopcoadj0i 31825 | An operator composed with its adjoint is zero iff the operator is zero. Theorem 3.11(vii) of [Beran] p. 106. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ π β BndLinOp β β’ ((π β (adjββπ)) = 0hop β π = 0hop ) | ||
Theorem | unierri 31826 | If we approximate a chain of unitary transformations (quantum computer gates) πΉ, πΊ by other unitary transformations π, π, the error increases at most additively. Equation 4.73 of [NielsenChuang] p. 195. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ πΉ β UniOp & β’ πΊ β UniOp & β’ π β UniOp & β’ π β UniOp β β’ (normopβ((πΉ β πΊ) βop (π β π))) β€ ((normopβ(πΉ βop π)) + (normopβ(πΊ βop π))) | ||
Theorem | branmfn 31827 | The norm of the bra function. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
β’ (π΄ β β β (normfnβ(braβπ΄)) = (normββπ΄)) | ||
Theorem | brabn 31828 | The bra of a vector is a bounded functional. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
β’ (π΄ β β β (normfnβ(braβπ΄)) β β) | ||
Theorem | rnbra 31829 | The set of bras equals the set of continuous linear functionals. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
β’ ran bra = (LinFn β© ContFn) | ||
Theorem | bra11 31830 | The bra function maps vectors one-to-one onto the set of continuous linear functionals. (Contributed by NM, 26-May-2006.) (Proof shortened by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
β’ bra: ββ1-1-ontoβ(LinFn β© ContFn) | ||
Theorem | bracnln 31831 | A bra is a continuous linear functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ (π΄ β β β (braβπ΄) β (LinFn β© ContFn)) | ||
Theorem | cnvbraval 31832* | Value of the converse of the bra function. Based on the Riesz Lemma riesz4 31786, this very important theorem not only justifies the Dirac bra-ket notation, but allows to extract a unique vector from any continuous linear functional from which the functional can be recovered; i.e. a single vector can "store" all of the information contained in any entire continuous linear functional (mapping from β to β). (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
β’ (π β (LinFn β© ContFn) β (β‘braβπ) = (β©π¦ β β βπ₯ β β (πβπ₯) = (π₯ Β·ih π¦))) | ||
Theorem | cnvbracl 31833 | Closure of the converse of the bra function. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
β’ (π β (LinFn β© ContFn) β (β‘braβπ) β β) | ||
Theorem | cnvbrabra 31834 | The converse bra of the bra of a vector is the vector itself. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ (π΄ β β β (β‘braβ(braβπ΄)) = π΄) | ||
Theorem | bracnvbra 31835 | The bra of the converse bra of a continuous linear functional. (Contributed by NM, 31-May-2006.) (New usage is discouraged.) |
β’ (π β (LinFn β© ContFn) β (braβ(β‘braβπ)) = π) | ||
Theorem | bracnlnval 31836* | The vector that a continuous linear functional is the bra of. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
β’ (π β (LinFn β© ContFn) β π = (braβ(β©π¦ β β βπ₯ β β (πβπ₯) = (π₯ Β·ih π¦)))) | ||
Theorem | cnvbramul 31837 | Multiplication property of the converse bra function. (Contributed by NM, 31-May-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π β (LinFn β© ContFn)) β (β‘braβ(π΄ Β·fn π)) = ((ββπ΄) Β·β (β‘braβπ))) | ||
Theorem | kbass1 31838 | Dirac bra-ket associative law ( β£ π΄β©β¨π΅ β£ ) β£ πΆβ© = β£ π΄β©(β¨π΅ β£ πΆβ©), i.e., the juxtaposition of an outer product with a ket equals a bra juxtaposed with an inner product. Since β¨π΅ β£ πΆβ© is a complex number, it is the first argument in the inner product Β·β that it is mapped to, although in Dirac notation it is placed after the ket. (Contributed by NM, 15-May-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ketbra π΅)βπΆ) = (((braβπ΅)βπΆ) Β·β π΄)) | ||
Theorem | kbass2 31839 | Dirac bra-ket associative law (β¨π΄ β£ π΅β©)β¨πΆ β£ = β¨π΄ β£ ( β£ π΅β©β¨πΆ β£ ), i.e., the juxtaposition of an inner product with a bra equals a ket juxtaposed with an outer product. (Contributed by NM, 23-May-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (((braβπ΄)βπ΅) Β·fn (braβπΆ)) = ((braβπ΄) β (π΅ ketbra πΆ))) | ||
Theorem | kbass3 31840 | Dirac bra-ket associative law β¨π΄ β£ π΅β©β¨πΆ β£ π·β© = (β¨π΄ β£ π΅β©β¨πΆ β£ ) β£ π·β©. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β (((braβπ΄)βπ΅) Β· ((braβπΆ)βπ·)) = ((((braβπ΄)βπ΅) Β·fn (braβπΆ))βπ·)) | ||
Theorem | kbass4 31841 | Dirac bra-ket associative law β¨π΄ β£ π΅β©β¨πΆ β£ π·β© = β¨π΄ β£ ( β£ π΅β©β¨πΆ β£ π·β©). (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β (((braβπ΄)βπ΅) Β· ((braβπΆ)βπ·)) = ((braβπ΄)β(((braβπΆ)βπ·) Β·β π΅))) | ||
Theorem | kbass5 31842 | Dirac bra-ket associative law ( β£ π΄β©β¨π΅ β£ )( β£ πΆβ©β¨π· β£ ) = (( β£ π΄β©β¨π΅ β£ ) β£ πΆβ©)β¨π· β£. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ ketbra π΅) β (πΆ ketbra π·)) = (((π΄ ketbra π΅)βπΆ) ketbra π·)) | ||
Theorem | kbass6 31843 | Dirac bra-ket associative law ( β£ π΄β©β¨π΅ β£ )( β£ πΆβ©β¨π· β£ ) = β£ π΄β©(β¨π΅ β£ ( β£ πΆβ©β¨π· β£ )). (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ ketbra π΅) β (πΆ ketbra π·)) = (π΄ ketbra (β‘braβ((braβπ΅) β (πΆ ketbra π·))))) | ||
Theorem | leopg 31844* | Ordering relation for positive operators. Definition of positive operator ordering in [Kreyszig] p. 470. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
β’ ((π β π΄ β§ π β π΅) β (π β€op π β ((π βop π) β HrmOp β§ βπ₯ β β 0 β€ (((π βop π)βπ₯) Β·ih π₯)))) | ||
Theorem | leop 31845* | Ordering relation for operators. Definition of positive operator ordering in [Kreyszig] p. 470. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
β’ ((π β HrmOp β§ π β HrmOp) β (π β€op π β βπ₯ β β 0 β€ (((π βop π)βπ₯) Β·ih π₯))) | ||
Theorem | leop2 31846* | Ordering relation for operators. Definition of operator ordering in [Young] p. 141. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
β’ ((π β HrmOp β§ π β HrmOp) β (π β€op π β βπ₯ β β ((πβπ₯) Β·ih π₯) β€ ((πβπ₯) Β·ih π₯))) | ||
Theorem | leop3 31847 | Operator ordering in terms of a positive operator. Definition of operator ordering in [Retherford] p. 49. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
β’ ((π β HrmOp β§ π β HrmOp) β (π β€op π β 0hop β€op (π βop π))) | ||
Theorem | leoppos 31848* | Binary relation defining a positive operator. Definition VI.1 of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
β’ (π β HrmOp β ( 0hop β€op π β βπ₯ β β 0 β€ ((πβπ₯) Β·ih π₯))) | ||
Theorem | leoprf2 31849 | The ordering relation for operators is reflexive. (Contributed by NM, 24-Jul-2006.) (New usage is discouraged.) |
β’ (π: ββΆ β β π β€op π) | ||
Theorem | leoprf 31850 | The ordering relation for operators is reflexive. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
β’ (π β HrmOp β π β€op π) | ||
Theorem | leopsq 31851 | The square of a Hermitian operator is positive. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
β’ (π β HrmOp β 0hop β€op (π β π)) | ||
Theorem | 0leop 31852 | The zero operator is a positive operator. (The literature calls it "positive", even though in some sense it is really "nonnegative".) Part of Example 12.2(i) in [Young] p. 142. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
β’ 0hop β€op 0hop | ||
Theorem | idleop 31853 | The identity operator is a positive operator. Part of Example 12.2(i) in [Young] p. 142. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
β’ 0hop β€op Iop | ||
Theorem | leopadd 31854 | The sum of two positive operators is positive. Exercise 1(i) of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
β’ (((π β HrmOp β§ π β HrmOp) β§ ( 0hop β€op π β§ 0hop β€op π)) β 0hop β€op (π +op π)) | ||
Theorem | leopmuli 31855 | The scalar product of a nonnegative real and a positive operator is a positive operator. Exercise 1(ii) of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π β HrmOp) β§ (0 β€ π΄ β§ 0hop β€op π)) β 0hop β€op (π΄ Β·op π)) | ||
Theorem | leopmul 31856 | The scalar product of a positive real and a positive operator is a positive operator. Exercise 1(ii) of [Retherford] p. 49. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π β HrmOp β§ 0 < π΄) β ( 0hop β€op π β 0hop β€op (π΄ Β·op π))) | ||
Theorem | leopmul2i 31857 | Scalar product applied to operator ordering. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π β HrmOp β§ π β HrmOp) β§ (0 β€ π΄ β§ π β€op π)) β (π΄ Β·op π) β€op (π΄ Β·op π)) | ||
Theorem | leoptri 31858 | The positive operator ordering relation satisfies trichotomy. Exercise 1(iii) of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
β’ ((π β HrmOp β§ π β HrmOp) β ((π β€op π β§ π β€op π) β π = π)) | ||
Theorem | leoptr 31859 | The positive operator ordering relation is transitive. Exercise 1(iv) of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
β’ (((π β HrmOp β§ π β HrmOp β§ π β HrmOp) β§ (π β€op π β§ π β€op π)) β π β€op π) | ||
Theorem | leopnmid 31860 | A bounded Hermitian operator is less than or equal to its norm times the identity operator. (Contributed by NM, 11-Aug-2006.) (New usage is discouraged.) |
β’ ((π β HrmOp β§ (normopβπ) β β) β π β€op ((normopβπ) Β·op Iop )) | ||
Theorem | nmopleid 31861 | A nonzero, bounded Hermitian operator divided by its norm is less than or equal to the identity operator. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
β’ ((π β HrmOp β§ (normopβπ) β β β§ π β 0hop ) β ((1 / (normopβπ)) Β·op π) β€op Iop ) | ||
Theorem | opsqrlem1 31862* | Lemma for opsqri . (Contributed by NM, 9-Aug-2006.) (New usage is discouraged.) |
β’ π β HrmOp & β’ (normopβπ) β β & β’ 0hop β€op π & β’ π = ((1 / (normopβπ)) Β·op π) & β’ (π β 0hop β βπ’ β HrmOp ( 0hop β€op π’ β§ (π’ β π’) = π )) β β’ (π β 0hop β βπ£ β HrmOp ( 0hop β€op π£ β§ (π£ β π£) = π)) | ||
Theorem | opsqrlem2 31863* | Lemma for opsqri . πΉβπ is the recursive function An (starting at n=1 instead of 0) of Theorem 9.4-2 of [Kreyszig] p. 476. (Contributed by NM, 17-Aug-2006.) (New usage is discouraged.) |
β’ π β HrmOp & β’ π = (π₯ β HrmOp, π¦ β HrmOp β¦ (π₯ +op ((1 / 2) Β·op (π βop (π₯ β π₯))))) & β’ πΉ = seq1(π, (β Γ { 0hop })) β β’ (πΉβ1) = 0hop | ||
Theorem | opsqrlem3 31864* | Lemma for opsqri . (Contributed by NM, 22-Aug-2006.) (New usage is discouraged.) |
β’ π β HrmOp & β’ π = (π₯ β HrmOp, π¦ β HrmOp β¦ (π₯ +op ((1 / 2) Β·op (π βop (π₯ β π₯))))) & β’ πΉ = seq1(π, (β Γ { 0hop })) β β’ ((πΊ β HrmOp β§ π» β HrmOp) β (πΊππ») = (πΊ +op ((1 / 2) Β·op (π βop (πΊ β πΊ))))) | ||
Theorem | opsqrlem4 31865* | Lemma for opsqri . (Contributed by NM, 17-Aug-2006.) (New usage is discouraged.) |
β’ π β HrmOp & β’ π = (π₯ β HrmOp, π¦ β HrmOp β¦ (π₯ +op ((1 / 2) Β·op (π βop (π₯ β π₯))))) & β’ πΉ = seq1(π, (β Γ { 0hop })) β β’ πΉ:ββΆHrmOp | ||
Theorem | opsqrlem5 31866* | Lemma for opsqri . (Contributed by NM, 17-Aug-2006.) (New usage is discouraged.) |
β’ π β HrmOp & β’ π = (π₯ β HrmOp, π¦ β HrmOp β¦ (π₯ +op ((1 / 2) Β·op (π βop (π₯ β π₯))))) & β’ πΉ = seq1(π, (β Γ { 0hop })) β β’ (π β β β (πΉβ(π + 1)) = ((πΉβπ) +op ((1 / 2) Β·op (π βop ((πΉβπ) β (πΉβπ)))))) | ||
Theorem | opsqrlem6 31867* | Lemma for opsqri . (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
β’ π β HrmOp & β’ π = (π₯ β HrmOp, π¦ β HrmOp β¦ (π₯ +op ((1 / 2) Β·op (π βop (π₯ β π₯))))) & β’ πΉ = seq1(π, (β Γ { 0hop })) & β’ π β€op Iop β β’ (π β β β (πΉβπ) β€op Iop ) | ||
Theorem | pjhmopi 31868 | A projector is a Hermitian operator. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
β’ π» β Cβ β β’ (projββπ») β HrmOp | ||
Theorem | pjlnopi 31869 | A projector is a linear operator. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
β’ π» β Cβ β β’ (projββπ») β LinOp | ||
Theorem | pjnmopi 31870 | The operator norm of a projector on a nonzero closed subspace is one. Part of Theorem 26.1 of [Halmos] p. 43. (Contributed by NM, 9-Apr-2006.) (New usage is discouraged.) |
β’ π» β Cβ β β’ (π» β 0β β (normopβ(projββπ»)) = 1) | ||
Theorem | pjbdlni 31871 | A projector is a bounded linear operator. (Contributed by NM, 3-Jun-2006.) (New usage is discouraged.) |
β’ π» β Cβ β β’ (projββπ») β BndLinOp | ||
Theorem | pjhmop 31872 | A projection is a Hermitian operator. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
β’ (π» β Cβ β (projββπ») β HrmOp) | ||
Theorem | hmopidmchi 31873 | An idempotent Hermitian operator generates a closed subspace. Part of proof of Theorem of [AkhiezerGlazman] p. 64. (Contributed by NM, 21-Apr-2006.) (Proof shortened by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
β’ π β HrmOp & β’ (π β π) = π β β’ ran π β Cβ | ||
Theorem | hmopidmpji 31874 | An idempotent Hermitian operator is a projection operator. Theorem 26.4 of [Halmos] p. 44. (Halmos seems to omit the proof that π» is a closed subspace, which is not trivial as hmopidmchi 31873 shows.) (Contributed by NM, 22-Apr-2006.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
β’ π β HrmOp & β’ (π β π) = π β β’ π = (projββran π) | ||
Theorem | hmopidmch 31875 | An idempotent Hermitian operator generates a closed subspace. Part of proof of Theorem of [AkhiezerGlazman] p. 64. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
β’ ((π β HrmOp β§ (π β π) = π) β ran π β Cβ ) | ||
Theorem | hmopidmpj 31876 | An idempotent Hermitian operator is a projection operator. Theorem 26.4 of [Halmos] p. 44. (Contributed by NM, 22-Apr-2006.) (New usage is discouraged.) |
β’ ((π β HrmOp β§ (π β π) = π) β π = (projββran π)) | ||
Theorem | pjsdii 31877 | Distributive law for Hilbert space operator sum. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
β’ π» β Cβ & β’ π: ββΆ β & β’ π: ββΆ β β β’ ((projββπ») β (π +op π)) = (((projββπ») β π) +op ((projββπ») β π)) | ||
Theorem | pjddii 31878 | Distributive law for Hilbert space operator difference. (Contributed by NM, 24-Nov-2000.) (New usage is discouraged.) |
β’ π» β Cβ & β’ π: ββΆ β & β’ π: ββΆ β β β’ ((projββπ») β (π βop π)) = (((projββπ») β π) βop ((projββπ») β π)) | ||
Theorem | pjsdi2i 31879 | Chained distributive law for Hilbert space operator difference. (Contributed by NM, 30-Nov-2000.) (New usage is discouraged.) |
β’ π» β Cβ & β’ π : ββΆ β & β’ π: ββΆ β & β’ π: ββΆ β β β’ ((π β (π +op π)) = ((π β π) +op (π β π)) β (((projββπ») β π ) β (π +op π)) = ((((projββπ») β π ) β π) +op (((projββπ») β π ) β π))) | ||
Theorem | pjcoi 31880 | Composition of projections. (Contributed by NM, 16-Aug-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (π΄ β β β (((projββπΊ) β (projββπ»))βπ΄) = ((projββπΊ)β((projββπ»)βπ΄))) | ||
Theorem | pjcocli 31881 | Closure of composition of projections. (Contributed by NM, 29-Nov-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (π΄ β β β (((projββπΊ) β (projββπ»))βπ΄) β πΊ) | ||
Theorem | pjcohcli 31882 | Closure of composition of projections. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (π΄ β β β (((projββπΊ) β (projββπ»))βπ΄) β β) | ||
Theorem | pjadjcoi 31883 | Adjoint of composition of projections. Special case of Theorem 3.11(viii) of [Beran] p. 106. (Contributed by NM, 6-Oct-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ ((π΄ β β β§ π΅ β β) β ((((projββπΊ) β (projββπ»))βπ΄) Β·ih π΅) = (π΄ Β·ih (((projββπ») β (projββπΊ))βπ΅))) | ||
Theorem | pjcofni 31884 | Functionality of composition of projections. (Contributed by NM, 1-Oct-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ ((projββπΊ) β (projββπ»)) Fn β | ||
Theorem | pjss1coi 31885 | Subset relationship for projections. Theorem 4.5(i)<->(iii) of [Beran] p. 112. (Contributed by NM, 1-Oct-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ β π» β ((projββπ») β (projββπΊ)) = (projββπΊ)) | ||
Theorem | pjss2coi 31886 | Subset relationship for projections. Theorem 4.5(i)<->(ii) of [Beran] p. 112. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ β π» β ((projββπΊ) β (projββπ»)) = (projββπΊ)) | ||
Theorem | pjssmi 31887 | Projection meet property. Remark in [Kalmbach] p. 66. Also Theorem 4.5(i)->(iv) of [Beran] p. 112. (Contributed by NM, 26-Sep-2001.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (π΄ β β β (π» β πΊ β (((projββπΊ)βπ΄) ββ ((projββπ»)βπ΄)) = ((projββ(πΊ β© (β₯βπ»)))βπ΄))) | ||
Theorem | pjssge0i 31888 | Theorem 4.5(iv)->(v) of [Beran] p. 112. (Contributed by NM, 26-Sep-2001.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (π΄ β β β ((((projββπΊ)βπ΄) ββ ((projββπ»)βπ΄)) = ((projββ(πΊ β© (β₯βπ»)))βπ΄) β 0 β€ ((((projββπΊ)βπ΄) ββ ((projββπ»)βπ΄)) Β·ih π΄))) | ||
Theorem | pjdifnormi 31889 | Theorem 4.5(v)<->(vi) of [Beran] p. 112. (Contributed by NM, 26-Sep-2001.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (π΄ β β β (0 β€ ((((projββπΊ)βπ΄) ββ ((projββπ»)βπ΄)) Β·ih π΄) β (normββ((projββπ»)βπ΄)) β€ (normββ((projββπΊ)βπ΄)))) | ||
Theorem | pjnormssi 31890* | Theorem 4.5(i)<->(vi) of [Beran] p. 112. (Contributed by NM, 26-Sep-2001.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ β π» β βπ₯ β β (normββ((projββπΊ)βπ₯)) β€ (normββ((projββπ»)βπ₯))) | ||
Theorem | pjorthcoi 31891 | Composition of projections of orthogonal subspaces. Part (i)->(iia) of Theorem 27.4 of [Halmos] p. 45. (Contributed by NM, 6-Nov-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ β (β₯βπ») β ((projββπΊ) β (projββπ»)) = 0hop ) | ||
Theorem | pjscji 31892 | The projection of orthogonal subspaces is the sum of the projections. (Contributed by NM, 11-Nov-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ β (β₯βπ») β (projββ(πΊ β¨β π»)) = ((projββπΊ) +op (projββπ»))) | ||
Theorem | pjssumi 31893 | The projection on a subspace sum is the sum of the projections. (Contributed by NM, 11-Nov-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ β (β₯βπ») β (projββ(πΊ +β π»)) = ((projββπΊ) +op (projββπ»))) | ||
Theorem | pjssposi 31894* | Projector ordering can be expressed by the subset relationship between their projection subspaces. (i)<->(iii) of Theorem 29.2 of [Halmos] p. 48. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (βπ₯ β β 0 β€ ((((projββπ») βop (projββπΊ))βπ₯) Β·ih π₯) β πΊ β π») | ||
Theorem | pjordi 31895* | The definition of projector ordering in [Halmos] p. 42 is equivalent to the definition of projector ordering in [Beran] p. 110. (We will usually express projector ordering with the even simpler equivalent πΊ β π»; see pjssposi 31894). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (βπ₯ β β 0 β€ ((((projββπ») βop (projββπΊ))βπ₯) Β·ih π₯) β ((projββπΊ) β β) β ((projββπ») β β)) | ||
Theorem | pjssdif2i 31896 | The projection subspace of the difference between two projectors. Part 2 of Theorem 29.3 of [Halmos] p. 48 (shortened with pjssposi 31894). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ β π» β ((projββπ») βop (projββπΊ)) = (projββ(π» β© (β₯βπΊ)))) | ||
Theorem | pjssdif1i 31897 | A necessary and sufficient condition for the difference between two projectors to be a projector. Part 1 of Theorem 29.3 of [Halmos] p. 48 (shortened with pjssposi 31894). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ β π» β ((projββπ») βop (projββπΊ)) β ran projβ) | ||
Theorem | pjimai 31898 | The image of a projection. Lemma 5 in Daniel Lehmann, "A presentation of Quantum Logic based on an and then connective", https://doi.org/10.48550/arXiv.quant-ph/0701113. (Contributed by NM, 20-Jan-2007.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Cβ β β’ ((projββπ΅) β π΄) = ((π΄ +β (β₯βπ΅)) β© π΅) | ||
Theorem | pjidmcoi 31899 | A projection is idempotent. Property (ii) of [Beran] p. 109. (Contributed by NM, 1-Oct-2000.) (New usage is discouraged.) |
β’ π» β Cβ β β’ ((projββπ») β (projββπ»)) = (projββπ») | ||
Theorem | pjoccoi 31900 | Composition of projections of a subspace and its orthocomplement. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
β’ π» β Cβ β β’ ((projββπ») β (projββ(β₯βπ»))) = 0hop |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |