![]() |
Metamath
Proof Explorer Theorem List (p. 320 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | unierri 31901 | 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 31902 | The norm of the bra function. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
β’ (π΄ β β β (normfnβ(braβπ΄)) = (normββπ΄)) | ||
Theorem | brabn 31903 | The bra of a vector is a bounded functional. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
β’ (π΄ β β β (normfnβ(braβπ΄)) β β) | ||
Theorem | rnbra 31904 | 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 31905 | 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 31906 | A bra is a continuous linear functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ (π΄ β β β (braβπ΄) β (LinFn β© ContFn)) | ||
Theorem | cnvbraval 31907* | Value of the converse of the bra function. Based on the Riesz Lemma riesz4 31861, 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 31908 | Closure of the converse of the bra function. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
β’ (π β (LinFn β© ContFn) β (β‘braβπ) β β) | ||
Theorem | cnvbrabra 31909 | 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 31910 | 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 31911* | 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 31912 | Multiplication property of the converse bra function. (Contributed by NM, 31-May-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π β (LinFn β© ContFn)) β (β‘braβ(π΄ Β·fn π)) = ((ββπ΄) Β·β (β‘braβπ))) | ||
Theorem | kbass1 31913 | 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 31914 | 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 31915 | Dirac bra-ket associative law β¨π΄ β£ π΅β©β¨πΆ β£ π·β© = (β¨π΄ β£ π΅β©β¨πΆ β£ ) β£ π·β©. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β (((braβπ΄)βπ΅) Β· ((braβπΆ)βπ·)) = ((((braβπ΄)βπ΅) Β·fn (braβπΆ))βπ·)) | ||
Theorem | kbass4 31916 | Dirac bra-ket associative law β¨π΄ β£ π΅β©β¨πΆ β£ π·β© = β¨π΄ β£ ( β£ π΅β©β¨πΆ β£ π·β©). (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β (((braβπ΄)βπ΅) Β· ((braβπΆ)βπ·)) = ((braβπ΄)β(((braβπΆ)βπ·) Β·β π΅))) | ||
Theorem | kbass5 31917 | Dirac bra-ket associative law ( β£ π΄β©β¨π΅ β£ )( β£ πΆβ©β¨π· β£ ) = (( β£ π΄β©β¨π΅ β£ ) β£ πΆβ©)β¨π· β£. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ ketbra π΅) β (πΆ ketbra π·)) = (((π΄ ketbra π΅)βπΆ) ketbra π·)) | ||
Theorem | kbass6 31918 | Dirac bra-ket associative law ( β£ π΄β©β¨π΅ β£ )( β£ πΆβ©β¨π· β£ ) = β£ π΄β©(β¨π΅ β£ ( β£ πΆβ©β¨π· β£ )). (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ ketbra π΅) β (πΆ ketbra π·)) = (π΄ ketbra (β‘braβ((braβπ΅) β (πΆ ketbra π·))))) | ||
Theorem | leopg 31919* | 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 31920* | 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 31921* | 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 31922 | 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 31923* | 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 31924 | The ordering relation for operators is reflexive. (Contributed by NM, 24-Jul-2006.) (New usage is discouraged.) |
β’ (π: ββΆ β β π β€op π) | ||
Theorem | leoprf 31925 | The ordering relation for operators is reflexive. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
β’ (π β HrmOp β π β€op π) | ||
Theorem | leopsq 31926 | The square of a Hermitian operator is positive. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
β’ (π β HrmOp β 0hop β€op (π β π)) | ||
Theorem | 0leop 31927 | 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 31928 | 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 31929 | 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 31930 | 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 31931 | 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 31932 | 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 31933 | 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 31934 | 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 31935 | 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 31936 | 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 31937* | 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 31938* | 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 31939* | 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 31940* | 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 31941* | 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 31942* | 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 31943 | A projector is a Hermitian operator. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
β’ π» β Cβ β β’ (projββπ») β HrmOp | ||
Theorem | pjlnopi 31944 | A projector is a linear operator. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
β’ π» β Cβ β β’ (projββπ») β LinOp | ||
Theorem | pjnmopi 31945 | 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 31946 | A projector is a bounded linear operator. (Contributed by NM, 3-Jun-2006.) (New usage is discouraged.) |
β’ π» β Cβ β β’ (projββπ») β BndLinOp | ||
Theorem | pjhmop 31947 | A projection is a Hermitian operator. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
β’ (π» β Cβ β (projββπ») β HrmOp) | ||
Theorem | hmopidmchi 31948 | 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 31949 | 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 31948 shows.) (Contributed by NM, 22-Apr-2006.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
β’ π β HrmOp & β’ (π β π) = π β β’ π = (projββran π) | ||
Theorem | hmopidmch 31950 | 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 31951 | 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 31952 | 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 31953 | 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 31954 | 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 31955 | Composition of projections. (Contributed by NM, 16-Aug-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (π΄ β β β (((projββπΊ) β (projββπ»))βπ΄) = ((projββπΊ)β((projββπ»)βπ΄))) | ||
Theorem | pjcocli 31956 | Closure of composition of projections. (Contributed by NM, 29-Nov-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (π΄ β β β (((projββπΊ) β (projββπ»))βπ΄) β πΊ) | ||
Theorem | pjcohcli 31957 | Closure of composition of projections. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (π΄ β β β (((projββπΊ) β (projββπ»))βπ΄) β β) | ||
Theorem | pjadjcoi 31958 | 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 31959 | Functionality of composition of projections. (Contributed by NM, 1-Oct-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ ((projββπΊ) β (projββπ»)) Fn β | ||
Theorem | pjss1coi 31960 | 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 31961 | 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 31962 | 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 31963 | 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 31964 | 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 31965* | 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 31966 | 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 31967 | 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 31968 | 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 31969* | 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 31970* | 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 31969). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (βπ₯ β β 0 β€ ((((projββπ») βop (projββπΊ))βπ₯) Β·ih π₯) β ((projββπΊ) β β) β ((projββπ») β β)) | ||
Theorem | pjssdif2i 31971 | The projection subspace of the difference between two projectors. Part 2 of Theorem 29.3 of [Halmos] p. 48 (shortened with pjssposi 31969). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ β π» β ((projββπ») βop (projββπΊ)) = (projββ(π» β© (β₯βπΊ)))) | ||
Theorem | pjssdif1i 31972 | 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 31969). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ β π» β ((projββπ») βop (projββπΊ)) β ran projβ) | ||
Theorem | pjimai 31973 | 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 31974 | 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 31975 | Composition of projections of a subspace and its orthocomplement. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
β’ π» β Cβ β β’ ((projββπ») β (projββ(β₯βπ»))) = 0hop | ||
Theorem | pjtoi 31976 | Subspace sum of projection and projection of orthocomplement. (Contributed by NM, 16-Nov-2000.) (New usage is discouraged.) |
β’ π» β Cβ β β’ ((projββπ») +op (projββ(β₯βπ»))) = (projββ β) | ||
Theorem | pjoci 31977 | Projection of orthocomplement. First part of Theorem 27.3 of [Halmos] p. 45. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
β’ π» β Cβ β β’ ((projββ β) βop (projββπ»)) = (projββ(β₯βπ»)) | ||
Theorem | pjidmco 31978 | A projection operator is idempotent. Property (ii) of [Beran] p. 109. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
β’ (π» β Cβ β ((projββπ») β (projββπ»)) = (projββπ»)) | ||
Theorem | dfpjop 31979 | Definition of projection operator in [Hughes] p. 47, except that we do not need linearity to be explicit by virtue of hmoplin 31739. (Contributed by NM, 24-Apr-2006.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
β’ (π β ran projβ β (π β HrmOp β§ (π β π) = π)) | ||
Theorem | pjhmopidm 31980 | Two ways to express the set of all projection operators. (Contributed by NM, 24-Apr-2006.) (Proof shortened by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
β’ ran projβ = {π‘ β HrmOp β£ (π‘ β π‘) = π‘} | ||
Theorem | elpjidm 31981 | A projection operator is idempotent. Part of Theorem 26.1 of [Halmos] p. 43. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
β’ (π β ran projβ β (π β π) = π) | ||
Theorem | elpjhmop 31982 | A projection operator is Hermitian. Part of Theorem 26.1 of [Halmos] p. 43. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
β’ (π β ran projβ β π β HrmOp) | ||
Theorem | 0leopj 31983 | A projector is a positive operator. (Contributed by NM, 27-Sep-2008.) (New usage is discouraged.) |
β’ (π β ran projβ β 0hop β€op π) | ||
Theorem | pjadj2 31984 | A projector is self-adjoint. Property (i) of [Beran] p. 109. (Contributed by NM, 3-Jun-2006.) (New usage is discouraged.) |
β’ (π β ran projβ β (adjββπ) = π) | ||
Theorem | pjadj3 31985 | A projector is self-adjoint. Property (i) of [Beran] p. 109. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
β’ (π» β Cβ β (adjββ(projββπ»)) = (projββπ»)) | ||
Theorem | elpjch 31986 | Reconstruction of the subspace of a projection operator. Part of Theorem 26.2 of [Halmos] p. 44. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
β’ (π β ran projβ β (ran π β Cβ β§ π = (projββran π))) | ||
Theorem | elpjrn 31987* | Reconstruction of the subspace of a projection operator. (Contributed by NM, 24-Apr-2006.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
β’ (π β ran projβ β ran π = {π₯ β β β£ (πβπ₯) = π₯}) | ||
Theorem | pjinvari 31988 | A closed subspace π» with projection π is invariant under an operator π iff ππ = πππ. Theorem 27.1 of [Halmos] p. 45. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
β’ π: ββΆ β & β’ π» β Cβ & β’ π = (projββπ») β β’ ((π β π): ββΆπ» β (π β π) = (π β (π β π))) | ||
Theorem | pjin1i 31989 | Lemma for Theorem 1.22 of Mittelstaedt, p. 20. (Contributed by NM, 22-Apr-2001.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (projββ(πΊ β© π»)) = ((projββπΊ) β (projββ(πΊ β© π»))) | ||
Theorem | pjin2i 31990 | Lemma for Theorem 1.22 of Mittelstaedt, p. 20. (Contributed by NM, 22-Apr-2001.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (((projββπΊ) = ((projββπΊ) β (projββπ»)) β§ (projββπ») = ((projββπ») β (projββπΊ))) β (projββπΊ) = (projββπ»)) | ||
Theorem | pjin3i 31991 | Lemma for Theorem 1.22 of Mittelstaedt, p. 20. (Contributed by NM, 22-Apr-2001.) (New usage is discouraged.) |
β’ πΉ β Cβ & β’ πΊ β Cβ & β’ π» β Cβ β β’ (((projββπΉ) = ((projββπΉ) β (projββπΊ)) β§ (projββπΉ) = ((projββπΉ) β (projββπ»))) β (projββπΉ) = ((projββπΉ) β (projββ(πΊ β© π»)))) | ||
Theorem | pjclem1 31992 | Lemma for projection commutation theorem. (Contributed by NM, 16-Nov-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ πΆβ π» β ((projββπΊ) β (projββπ»)) = (projββ(πΊ β© π»))) | ||
Theorem | pjclem2 31993 | Lemma for projection commutation theorem. (Contributed by NM, 17-Nov-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ πΆβ π» β ((projββπΊ) β (projββπ»)) = ((projββπ») β (projββπΊ))) | ||
Theorem | pjclem3 31994 | Lemma for projection commutation theorem. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (((projββπΊ) β (projββπ»)) = ((projββπ») β (projββπΊ)) β ((projββπΊ) β (projββ(β₯βπ»))) = ((projββ(β₯βπ»)) β (projββπΊ))) | ||
Theorem | pjclem4a 31995 | Lemma for projection commutation theorem. (Contributed by NM, 2-Dec-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (π΄ β (πΊ β© π») β (((projββπΊ) β (projββπ»))βπ΄) = π΄) | ||
Theorem | pjclem4 31996 | Lemma for projection commutation theorem. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (((projββπΊ) β (projββπ»)) = ((projββπ») β (projββπΊ)) β ((projββπΊ) β (projββπ»)) = (projββ(πΊ β© π»))) | ||
Theorem | pjci 31997 | Two subspaces commute iff their projections commute. Lemma 4 of [Kalmbach] p. 67. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ πΆβ π» β ((projββπΊ) β (projββπ»)) = ((projββπ») β (projββπΊ))) | ||
Theorem | pjcmul1i 31998 | A necessary and sufficient condition for the product of two projectors to be a projector is that the projectors commute. Part 1 of Theorem 1 of [AkhiezerGlazman] p. 65. (Contributed by NM, 3-Jun-2006.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (((projββπΊ) β (projββπ»)) = ((projββπ») β (projββπΊ)) β ((projββπΊ) β (projββπ»)) β ran projβ) | ||
Theorem | pjcmul2i 31999 | The projection subspace of the difference between two projectors. Part 2 of Theorem 1 of [AkhiezerGlazman] p. 65. (Contributed by NM, 3-Jun-2006.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (((projββπΊ) β (projββπ»)) = ((projββπ») β (projββπΊ)) β ((projββπΊ) β (projββπ»)) = (projββ(πΊ β© π»))) | ||
Theorem | pjcohocli 32000 | Closure of composition of projection and Hilbert space operator. (Contributed by NM, 3-Dec-2000.) (New usage is discouraged.) |
β’ π» β Cβ & β’ π: ββΆ β β β’ (π΄ β β β (((projββπ») β π)βπ΄) β π») |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |