![]() |
Metamath
Proof Explorer Theorem List (p. 314 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lnfnmul 31301 | Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ ((π β LinFn β§ π΄ β β β§ π΅ β β) β (πβ(π΄ Β·β π΅)) = (π΄ Β· (πβπ΅))) | ||
Theorem | nmbdfnlbi 31302 | A lower bound for the norm of a bounded linear functional. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
β’ (π β LinFn β§ (normfnβπ) β β) β β’ (π΄ β β β (absβ(πβπ΄)) β€ ((normfnβπ) Β· (normββπ΄))) | ||
Theorem | nmbdfnlb 31303 | A lower bound for the norm of a bounded linear functional. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
β’ ((π β LinFn β§ (normfnβπ) β β β§ π΄ β β) β (absβ(πβπ΄)) β€ ((normfnβπ) Β· (normββπ΄))) | ||
Theorem | nmcfnexi 31304 | The norm of a continuous linear Hilbert space functional exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
β’ π β LinFn & β’ π β ContFn β β’ (normfnβπ) β β | ||
Theorem | nmcfnlbi 31305 | A lower bound for the norm of a continuous linear functional. Theorem 3.5(ii) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn & β’ π β ContFn β β’ (π΄ β β β (absβ(πβπ΄)) β€ ((normfnβπ) Β· (normββπ΄))) | ||
Theorem | nmcfnex 31306 | The norm of a continuous linear Hilbert space functional exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ ((π β LinFn β§ π β ContFn) β (normfnβπ) β β) | ||
Theorem | nmcfnlb 31307 | A lower bound of the norm of a continuous linear Hilbert space functional. Theorem 3.5(ii) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ ((π β LinFn β§ π β ContFn β§ π΄ β β) β (absβ(πβπ΄)) β€ ((normfnβπ) Β· (normββπ΄))) | ||
Theorem | lnfnconi 31308* | A condition equivalent to "π is continuous" when π is linear. Theorem 3.5(iii) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
β’ π β LinFn β β’ (π β ContFn β βπ₯ β β βπ¦ β β (absβ(πβπ¦)) β€ (π₯ Β· (normββπ¦))) | ||
Theorem | lnfncon 31309* | A condition equivalent to "π is continuous" when π is linear. Theorem 3.5(iii) of [Beran] p. 99. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.) |
β’ (π β LinFn β (π β ContFn β βπ₯ β β βπ¦ β β (absβ(πβπ¦)) β€ (π₯ Β· (normββπ¦)))) | ||
Theorem | lnfncnbd 31310 | A linear functional is continuous iff it is bounded. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
β’ (π β LinFn β (π β ContFn β (normfnβπ) β β)) | ||
Theorem | imaelshi 31311 | The image of a subspace under a linear operator is a subspace. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
β’ π β LinOp & β’ π΄ β Sβ β β’ (π β π΄) β Sβ | ||
Theorem | rnelshi 31312 | The range of a linear operator is a subspace. (Contributed by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
β’ π β LinOp β β’ ran π β Sβ | ||
Theorem | nlelshi 31313 | The null space of a linear functional is a subspace. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
β’ π β LinFn β β’ (nullβπ) β Sβ | ||
Theorem | nlelchi 31314 | The null space of a continuous linear functional is a closed subspace. Remark 3.8 of [Beran] p. 103. (Contributed by NM, 11-Feb-2006.) (Proof shortened by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
β’ π β LinFn & β’ π β ContFn β β’ (nullβπ) β Cβ | ||
Theorem | riesz3i 31315* | A continuous linear functional can be expressed as an inner product. Existence part of Theorem 3.9 of [Beran] p. 104. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn & β’ π β ContFn β β’ βπ€ β β βπ£ β β (πβπ£) = (π£ Β·ih π€) | ||
Theorem | riesz4i 31316* | A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn & β’ π β ContFn β β’ β!π€ β β βπ£ β β (πβπ£) = (π£ Β·ih π€) | ||
Theorem | riesz4 31317* | A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104. See riesz2 31319 for the bounded linear functional version. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.) |
β’ (π β (LinFn β© ContFn) β β!π€ β β βπ£ β β (πβπ£) = (π£ Β·ih π€)) | ||
Theorem | riesz1 31318* | Part 1 of the Riesz representation theorem for bounded linear functionals. A linear functional is bounded iff its value can be expressed as an inner product. Part of Theorem 17.3 of [Halmos] p. 31. For part 2, see riesz2 31319. For the continuous linear functional version, see riesz3i 31315 and riesz4 31317. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
β’ (π β LinFn β ((normfnβπ) β β β βπ¦ β β βπ₯ β β (πβπ₯) = (π₯ Β·ih π¦))) | ||
Theorem | riesz2 31319* | Part 2 of the Riesz representation theorem for bounded linear functionals. The value of a bounded linear functional corresponds to a unique inner product. Part of Theorem 17.3 of [Halmos] p. 31. For part 1, see riesz1 31318. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
β’ ((π β LinFn β§ (normfnβπ) β β) β β!π¦ β β βπ₯ β β (πβπ₯) = (π₯ Β·ih π¦)) | ||
Theorem | cnlnadjlem1 31320* | Lemma for cnlnadji 31329 (Theorem 3.10 of [Beran] p. 104: every continuous linear operator has an adjoint). The value of the auxiliary functional πΊ. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β ContOp & β’ πΊ = (π β β β¦ ((πβπ) Β·ih π¦)) β β’ (π΄ β β β (πΊβπ΄) = ((πβπ΄) Β·ih π¦)) | ||
Theorem | cnlnadjlem2 31321* | Lemma for cnlnadji 31329. πΊ is a continuous linear functional. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β ContOp & β’ πΊ = (π β β β¦ ((πβπ) Β·ih π¦)) β β’ (π¦ β β β (πΊ β LinFn β§ πΊ β ContFn)) | ||
Theorem | cnlnadjlem3 31322* | Lemma for cnlnadji 31329. By riesz4 31317, π΅ is the unique vector such that (πβπ£) Β·ih π¦) = (π£ Β·ih π€) for all π£. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β ContOp & β’ πΊ = (π β β β¦ ((πβπ) Β·ih π¦)) & β’ π΅ = (β©π€ β β βπ£ β β ((πβπ£) Β·ih π¦) = (π£ Β·ih π€)) β β’ (π¦ β β β π΅ β β) | ||
Theorem | cnlnadjlem4 31323* | Lemma for cnlnadji 31329. The values of auxiliary function πΉ are vectors. (Contributed by NM, 17-Feb-2006.) (Proof shortened by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β ContOp & β’ πΊ = (π β β β¦ ((πβπ) Β·ih π¦)) & β’ π΅ = (β©π€ β β βπ£ β β ((πβπ£) Β·ih π¦) = (π£ Β·ih π€)) & β’ πΉ = (π¦ β β β¦ π΅) β β’ (π΄ β β β (πΉβπ΄) β β) | ||
Theorem | cnlnadjlem5 31324* | Lemma for cnlnadji 31329. πΉ is an adjoint of π (later, we will show it is unique). (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β ContOp & β’ πΊ = (π β β β¦ ((πβπ) Β·ih π¦)) & β’ π΅ = (β©π€ β β βπ£ β β ((πβπ£) Β·ih π¦) = (π£ Β·ih π€)) & β’ πΉ = (π¦ β β β¦ π΅) β β’ ((π΄ β β β§ πΆ β β) β ((πβπΆ) Β·ih π΄) = (πΆ Β·ih (πΉβπ΄))) | ||
Theorem | cnlnadjlem6 31325* | Lemma for cnlnadji 31329. πΉ is linear. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β ContOp & β’ πΊ = (π β β β¦ ((πβπ) Β·ih π¦)) & β’ π΅ = (β©π€ β β βπ£ β β ((πβπ£) Β·ih π¦) = (π£ Β·ih π€)) & β’ πΉ = (π¦ β β β¦ π΅) β β’ πΉ β LinOp | ||
Theorem | cnlnadjlem7 31326* | Lemma for cnlnadji 31329. 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 31327* | Lemma for cnlnadji 31329. πΉ is continuous. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β ContOp & β’ πΊ = (π β β β¦ ((πβπ) Β·ih π¦)) & β’ π΅ = (β©π€ β β βπ£ β β ((πβπ£) Β·ih π¦) = (π£ Β·ih π€)) & β’ πΉ = (π¦ β β β¦ π΅) β β’ πΉ β ContOp | ||
Theorem | cnlnadjlem9 31328* | Lemma for cnlnadji 31329. πΉ 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 31329* | 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 31330* | 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 31331* | 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 31332* | 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 31333 | 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 31334 | Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
β’ BndLinOp β dom adjβ | ||
Theorem | bdopadj 31335 | Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
β’ (π β BndLinOp β π β dom adjβ) | ||
Theorem | adjbdln 31336 | 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 31337 | 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 31338 | 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 31339 | 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 31340 | Every operator with an adjoint is linear. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.) |
β’ dom adjβ β LinOp | ||
Theorem | nmopadjlei 31341 | 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 31342 | Lemma for nmopadji 31343. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
β’ π β BndLinOp β β’ (normopβ(adjββπ)) β€ (normopβπ) | ||
Theorem | nmopadji 31343 | 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 31344 | 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 31345 | 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 31346 | 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 31347 | 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 31348 | 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 31349 | 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 31350 | 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 31351 | The composition of two bounded linear operators is bounded. (Contributed by NM, 9-Mar-2006.) (New usage is discouraged.) |
β’ π β BndLinOp & β’ π β BndLinOp β β’ (π β π) β BndLinOp | ||
Theorem | nmoptri2i 31352 | 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 31353 | 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 31354 | 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 31355 | 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 31356 | 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 31357 | 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 31358 | The norm of the bra function. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
β’ (π΄ β β β (normfnβ(braβπ΄)) = (normββπ΄)) | ||
Theorem | brabn 31359 | The bra of a vector is a bounded functional. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
β’ (π΄ β β β (normfnβ(braβπ΄)) β β) | ||
Theorem | rnbra 31360 | 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 31361 | 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 31362 | A bra is a continuous linear functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ (π΄ β β β (braβπ΄) β (LinFn β© ContFn)) | ||
Theorem | cnvbraval 31363* | Value of the converse of the bra function. Based on the Riesz Lemma riesz4 31317, 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 31364 | Closure of the converse of the bra function. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
β’ (π β (LinFn β© ContFn) β (β‘braβπ) β β) | ||
Theorem | cnvbrabra 31365 | 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 31366 | 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 31367* | 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 31368 | Multiplication property of the converse bra function. (Contributed by NM, 31-May-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π β (LinFn β© ContFn)) β (β‘braβ(π΄ Β·fn π)) = ((ββπ΄) Β·β (β‘braβπ))) | ||
Theorem | kbass1 31369 | 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 31370 | 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 31371 | Dirac bra-ket associative law β¨π΄ β£ π΅β©β¨πΆ β£ π·β© = (β¨π΄ β£ π΅β©β¨πΆ β£ ) β£ π·β©. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β (((braβπ΄)βπ΅) Β· ((braβπΆ)βπ·)) = ((((braβπ΄)βπ΅) Β·fn (braβπΆ))βπ·)) | ||
Theorem | kbass4 31372 | Dirac bra-ket associative law β¨π΄ β£ π΅β©β¨πΆ β£ π·β© = β¨π΄ β£ ( β£ π΅β©β¨πΆ β£ π·β©). (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β (((braβπ΄)βπ΅) Β· ((braβπΆ)βπ·)) = ((braβπ΄)β(((braβπΆ)βπ·) Β·β π΅))) | ||
Theorem | kbass5 31373 | Dirac bra-ket associative law ( β£ π΄β©β¨π΅ β£ )( β£ πΆβ©β¨π· β£ ) = (( β£ π΄β©β¨π΅ β£ ) β£ πΆβ©)β¨π· β£. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ ketbra π΅) β (πΆ ketbra π·)) = (((π΄ ketbra π΅)βπΆ) ketbra π·)) | ||
Theorem | kbass6 31374 | Dirac bra-ket associative law ( β£ π΄β©β¨π΅ β£ )( β£ πΆβ©β¨π· β£ ) = β£ π΄β©(β¨π΅ β£ ( β£ πΆβ©β¨π· β£ )). (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ ketbra π΅) β (πΆ ketbra π·)) = (π΄ ketbra (β‘braβ((braβπ΅) β (πΆ ketbra π·))))) | ||
Theorem | leopg 31375* | 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 31376* | 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 31377* | 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 31378 | 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 31379* | 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 31380 | The ordering relation for operators is reflexive. (Contributed by NM, 24-Jul-2006.) (New usage is discouraged.) |
β’ (π: ββΆ β β π β€op π) | ||
Theorem | leoprf 31381 | The ordering relation for operators is reflexive. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
β’ (π β HrmOp β π β€op π) | ||
Theorem | leopsq 31382 | The square of a Hermitian operator is positive. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
β’ (π β HrmOp β 0hop β€op (π β π)) | ||
Theorem | 0leop 31383 | 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 31384 | 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 31385 | 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 31386 | 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 31387 | 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 31388 | 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 31389 | 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 31390 | 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 31391 | 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 31392 | 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 31393* | 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 31394* | 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 31395* | 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 31396* | 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 31397* | 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 31398* | 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 31399 | A projector is a Hermitian operator. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
β’ π» β Cβ β β’ (projββπ») β HrmOp | ||
Theorem | pjlnopi 31400 | A projector is a linear operator. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
β’ π» β Cβ β β’ (projββπ») β LinOp |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |