Home | Metamath
Proof Explorer Theorem List (p. 309 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 | cnlnadjlem7 30801* | Lemma for cnlnadji 30804. Helper lemma to show that πΉ is continuous. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β ContOp & β’ πΊ = (π β β β¦ ((πβπ) Β·ih π¦)) & β’ π΅ = (β©π€ β β βπ£ β β ((πβπ£) Β·ih π¦) = (π£ Β·ih π€)) & β’ πΉ = (π¦ β β β¦ π΅) β β’ (π΄ β β β (normββ(πΉβπ΄)) β€ ((normopβπ) Β· (normββπ΄))) | ||
Theorem | cnlnadjlem8 30802* | Lemma for cnlnadji 30804. πΉ is continuous. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β ContOp & β’ πΊ = (π β β β¦ ((πβπ) Β·ih π¦)) & β’ π΅ = (β©π€ β β βπ£ β β ((πβπ£) Β·ih π¦) = (π£ Β·ih π€)) & β’ πΉ = (π¦ β β β¦ π΅) β β’ πΉ β ContOp | ||
Theorem | cnlnadjlem9 30803* | Lemma for cnlnadji 30804. πΉ provides an example showing the existence of a continuous linear adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β ContOp & β’ πΊ = (π β β β¦ ((πβπ) Β·ih π¦)) & β’ π΅ = (β©π€ β β βπ£ β β ((πβπ£) Β·ih π¦) = (π£ Β·ih π€)) & β’ πΉ = (π¦ β β β¦ π΅) β β’ βπ‘ β (LinOp β© ContOp)βπ₯ β β βπ§ β β ((πβπ₯) Β·ih π§) = (π₯ Β·ih (π‘βπ§)) | ||
Theorem | cnlnadji 30804* | 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 | cnlnadjeui 30805* | Every continuous linear operator has a unique 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 | cnlnadjeu 30806* | Every continuous linear operator has a unique adjoint. Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
β’ (π β (LinOp β© ContOp) β β!π‘ β (LinOp β© ContOp)βπ₯ β β βπ¦ β β ((πβπ₯) Β·ih π¦) = (π₯ Β·ih (π‘βπ¦))) | ||
Theorem | cnlnadj 30807* | 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 30808 | 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 30809 | Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
β’ BndLinOp β dom adjβ | ||
Theorem | bdopadj 30810 | Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
β’ (π β BndLinOp β π β dom adjβ) | ||
Theorem | adjbdln 30811 | 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 30812 | 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 30813 | 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 30814 | 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 30815 | Every operator with an adjoint is linear. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.) |
β’ dom adjβ β LinOp | ||
Theorem | nmopadjlei 30816 | 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 30817 | Lemma for nmopadji 30818. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
β’ π β BndLinOp β β’ (normopβ(adjββπ)) β€ (normopβπ) | ||
Theorem | nmopadji 30818 | 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 30819 | 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 30820 | 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 30821 | 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 30822 | 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 30823 | 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 30824 | 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 30825 | 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 30826 | The composition of two bounded linear operators is bounded. (Contributed by NM, 9-Mar-2006.) (New usage is discouraged.) |
β’ π β BndLinOp & β’ π β BndLinOp β β’ (π β π) β BndLinOp | ||
Theorem | nmoptri2i 30827 | 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 30828 | 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 30829 | 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 30830 | 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 30831 | 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 30832 | 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 30833 | The norm of the bra function. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
β’ (π΄ β β β (normfnβ(braβπ΄)) = (normββπ΄)) | ||
Theorem | brabn 30834 | The bra of a vector is a bounded functional. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
β’ (π΄ β β β (normfnβ(braβπ΄)) β β) | ||
Theorem | rnbra 30835 | 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 30836 | 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 30837 | A bra is a continuous linear functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ (π΄ β β β (braβπ΄) β (LinFn β© ContFn)) | ||
Theorem | cnvbraval 30838* | Value of the converse of the bra function. Based on the Riesz Lemma riesz4 30792, 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 30839 | Closure of the converse of the bra function. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
β’ (π β (LinFn β© ContFn) β (β‘braβπ) β β) | ||
Theorem | cnvbrabra 30840 | 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 30841 | 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 30842* | 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 30843 | Multiplication property of the converse bra function. (Contributed by NM, 31-May-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π β (LinFn β© ContFn)) β (β‘braβ(π΄ Β·fn π)) = ((ββπ΄) Β·β (β‘braβπ))) | ||
Theorem | kbass1 30844 | 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 30845 | 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 30846 | Dirac bra-ket associative law β¨π΄ β£ π΅β©β¨πΆ β£ π·β© = (β¨π΄ β£ π΅β©β¨πΆ β£ ) β£ π·β©. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β (((braβπ΄)βπ΅) Β· ((braβπΆ)βπ·)) = ((((braβπ΄)βπ΅) Β·fn (braβπΆ))βπ·)) | ||
Theorem | kbass4 30847 | Dirac bra-ket associative law β¨π΄ β£ π΅β©β¨πΆ β£ π·β© = β¨π΄ β£ ( β£ π΅β©β¨πΆ β£ π·β©). (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β (((braβπ΄)βπ΅) Β· ((braβπΆ)βπ·)) = ((braβπ΄)β(((braβπΆ)βπ·) Β·β π΅))) | ||
Theorem | kbass5 30848 | Dirac bra-ket associative law ( β£ π΄β©β¨π΅ β£ )( β£ πΆβ©β¨π· β£ ) = (( β£ π΄β©β¨π΅ β£ ) β£ πΆβ©)β¨π· β£. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ ketbra π΅) β (πΆ ketbra π·)) = (((π΄ ketbra π΅)βπΆ) ketbra π·)) | ||
Theorem | kbass6 30849 | Dirac bra-ket associative law ( β£ π΄β©β¨π΅ β£ )( β£ πΆβ©β¨π· β£ ) = β£ π΄β©(β¨π΅ β£ ( β£ πΆβ©β¨π· β£ )). (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ ketbra π΅) β (πΆ ketbra π·)) = (π΄ ketbra (β‘braβ((braβπ΅) β (πΆ ketbra π·))))) | ||
Theorem | leopg 30850* | 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 30851* | 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 30852* | 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 30853 | 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 30854* | 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 30855 | The ordering relation for operators is reflexive. (Contributed by NM, 24-Jul-2006.) (New usage is discouraged.) |
β’ (π: ββΆ β β π β€op π) | ||
Theorem | leoprf 30856 | The ordering relation for operators is reflexive. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
β’ (π β HrmOp β π β€op π) | ||
Theorem | leopsq 30857 | The square of a Hermitian operator is positive. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
β’ (π β HrmOp β 0hop β€op (π β π)) | ||
Theorem | 0leop 30858 | 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 30859 | 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 30860 | 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 30861 | 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 30862 | 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 30863 | 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 30864 | 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 30865 | 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 30866 | 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 30867 | 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 30868* | 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 30869* | 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 30870* | 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 30871* | 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 30872* | 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 30873* | 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 30874 | A projector is a Hermitian operator. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
β’ π» β Cβ β β’ (projββπ») β HrmOp | ||
Theorem | pjlnopi 30875 | A projector is a linear operator. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
β’ π» β Cβ β β’ (projββπ») β LinOp | ||
Theorem | pjnmopi 30876 | 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 30877 | A projector is a bounded linear operator. (Contributed by NM, 3-Jun-2006.) (New usage is discouraged.) |
β’ π» β Cβ β β’ (projββπ») β BndLinOp | ||
Theorem | pjhmop 30878 | A projection is a Hermitian operator. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
β’ (π» β Cβ β (projββπ») β HrmOp) | ||
Theorem | hmopidmchi 30879 | 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 30880 | 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 30879 shows.) (Contributed by NM, 22-Apr-2006.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
β’ π β HrmOp & β’ (π β π) = π β β’ π = (projββran π) | ||
Theorem | hmopidmch 30881 | 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 30882 | 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 30883 | 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 30884 | 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 30885 | 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 30886 | Composition of projections. (Contributed by NM, 16-Aug-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (π΄ β β β (((projββπΊ) β (projββπ»))βπ΄) = ((projββπΊ)β((projββπ»)βπ΄))) | ||
Theorem | pjcocli 30887 | Closure of composition of projections. (Contributed by NM, 29-Nov-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (π΄ β β β (((projββπΊ) β (projββπ»))βπ΄) β πΊ) | ||
Theorem | pjcohcli 30888 | Closure of composition of projections. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (π΄ β β β (((projββπΊ) β (projββπ»))βπ΄) β β) | ||
Theorem | pjadjcoi 30889 | 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 30890 | Functionality of composition of projections. (Contributed by NM, 1-Oct-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ ((projββπΊ) β (projββπ»)) Fn β | ||
Theorem | pjss1coi 30891 | 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 30892 | 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 30893 | 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 30894 | 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 30895 | 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 30896* | 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 30897 | 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 30898 | 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 30899 | 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 30900* | 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 π₯) β πΊ β π») |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |