![]() |
Metamath
Proof Explorer Theorem List (p. 319 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | kbfval 31801* | The outer product of two vectors, expressed as β£ π΄β©β¨π΅ β£ in Dirac notation. See df-kb 31700. (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ ketbra π΅) = (π₯ β β β¦ ((π₯ Β·ih π΅) Β·β π΄))) | ||
Theorem | kbop 31802 | The outer product of two vectors, expressed as β£ π΄β©β¨π΅ β£ in Dirac notation, is an operator. (Contributed by NM, 30-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ ketbra π΅): ββΆ β) | ||
Theorem | kbval 31803 | The value of the operator resulting from the outer product β£ π΄β© β¨π΅ β£ of two vectors. Equation 8.1 of [Prugovecki] p. 376. (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ketbra π΅)βπΆ) = ((πΆ Β·ih π΅) Β·β π΄)) | ||
Theorem | kbmul 31804 | Multiplication property of outer product. (Contributed by NM, 31-May-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ Β·β π΅) ketbra πΆ) = (π΅ ketbra ((ββπ΄) Β·β πΆ))) | ||
Theorem | kbpj 31805 | If a vector π΄ has norm 1, the outer product β£ π΄β©β¨π΄ β£ is the projector onto the subspace spanned by π΄. http://en.wikipedia.org/wiki/Bra-ket#Linear%5Foperators. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ (normββπ΄) = 1) β (π΄ ketbra π΄) = (projββ(spanβ{π΄}))) | ||
Theorem | eleigvec 31806* | Membership in the set of eigenvectors of a Hilbert space operator. (Contributed by NM, 11-Mar-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
β’ (π: ββΆ β β (π΄ β (eigvecβπ) β (π΄ β β β§ π΄ β 0β β§ βπ₯ β β (πβπ΄) = (π₯ Β·β π΄)))) | ||
Theorem | eleigvec2 31807 | Membership in the set of eigenvectors of a Hilbert space operator. (Contributed by NM, 18-Mar-2006.) (New usage is discouraged.) |
β’ (π: ββΆ β β (π΄ β (eigvecβπ) β (π΄ β β β§ π΄ β 0β β§ (πβπ΄) β (spanβ{π΄})))) | ||
Theorem | eleigveccl 31808 | Closure of an eigenvector of a Hilbert space operator. (Contributed by NM, 23-Mar-2006.) (New usage is discouraged.) |
β’ ((π: ββΆ β β§ π΄ β (eigvecβπ)) β π΄ β β) | ||
Theorem | eigvalval 31809 | The eigenvalue of an eigenvector of a Hilbert space operator. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
β’ ((π: ββΆ β β§ π΄ β (eigvecβπ)) β ((eigvalβπ)βπ΄) = (((πβπ΄) Β·ih π΄) / ((normββπ΄)β2))) | ||
Theorem | eigvalcl 31810 | An eigenvalue is a complex number. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
β’ ((π: ββΆ β β§ π΄ β (eigvecβπ)) β ((eigvalβπ)βπ΄) β β) | ||
Theorem | eigvec1 31811 | Property of an eigenvector. (Contributed by NM, 12-Mar-2006.) (New usage is discouraged.) |
β’ ((π: ββΆ β β§ π΄ β (eigvecβπ)) β ((πβπ΄) = (((eigvalβπ)βπ΄) Β·β π΄) β§ π΄ β 0β)) | ||
Theorem | eighmre 31812 | The eigenvalues of a Hermitian operator are real. Equation 1.30 of [Hughes] p. 49. (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.) |
β’ ((π β HrmOp β§ π΄ β (eigvecβπ)) β ((eigvalβπ)βπ΄) β β) | ||
Theorem | eighmorth 31813 | Eigenvectors of a Hermitian operator with distinct eigenvalues are orthogonal. Equation 1.31 of [Hughes] p. 49. (Contributed by NM, 23-Mar-2006.) (New usage is discouraged.) |
β’ (((π β HrmOp β§ π΄ β (eigvecβπ)) β§ (π΅ β (eigvecβπ) β§ ((eigvalβπ)βπ΄) β ((eigvalβπ)βπ΅))) β (π΄ Β·ih π΅) = 0) | ||
Theorem | nmopnegi 31814 | Value of the norm of the negative of a Hilbert space operator. Unlike nmophmi 31880, the operator does not have to be bounded. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ π: ββΆ β β β’ (normopβ(-1 Β·op π)) = (normopβπ) | ||
Theorem | lnop0 31815 | The value of a linear Hilbert space operator at zero is zero. Remark in [Beran] p. 99. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
β’ (π β LinOp β (πβ0β) = 0β) | ||
Theorem | lnopmul 31816 | Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
β’ ((π β LinOp β§ π΄ β β β§ π΅ β β) β (πβ(π΄ Β·β π΅)) = (π΄ Β·β (πβπ΅))) | ||
Theorem | lnopli 31817 | Basic scalar product property of a linear Hilbert space operator. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πβ((π΄ Β·β π΅) +β πΆ)) = ((π΄ Β·β (πβπ΅)) +β (πβπΆ))) | ||
Theorem | lnopfi 31818 | A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.) |
β’ π β LinOp β β’ π: ββΆ β | ||
Theorem | lnop0i 31819 | The value of a linear Hilbert space operator at zero is zero. Remark in [Beran] p. 99. (Contributed by NM, 11-May-2005.) (New usage is discouraged.) |
β’ π β LinOp β β’ (πβ0β) = 0β | ||
Theorem | lnopaddi 31820 | Additive property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β) β (πβ(π΄ +β π΅)) = ((πβπ΄) +β (πβπ΅))) | ||
Theorem | lnopmuli 31821 | Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β) β (πβ(π΄ Β·β π΅)) = (π΄ Β·β (πβπ΅))) | ||
Theorem | lnopaddmuli 31822 | Sum/product property of a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πβ(π΅ +β (π΄ Β·β πΆ))) = ((πβπ΅) +β (π΄ Β·β (πβπΆ)))) | ||
Theorem | lnopsubi 31823 | Subtraction property for a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β) β (πβ(π΄ ββ π΅)) = ((πβπ΄) ββ (πβπ΅))) | ||
Theorem | lnopsubmuli 31824 | Subtraction/product property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πβ(π΅ ββ (π΄ Β·β πΆ))) = ((πβπ΅) ββ (π΄ Β·β (πβπΆ)))) | ||
Theorem | lnopmulsubi 31825 | Product/subtraction property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πβ((π΄ Β·β π΅) ββ πΆ)) = ((π΄ Β·β (πβπ΅)) ββ (πβπΆ))) | ||
Theorem | homco2 31826 | Move a scalar product out of a composition of operators. The operator π must be linear, unlike homco1 31650 that works for any operators. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π β LinOp β§ π: ββΆ β) β (π β (π΄ Β·op π)) = (π΄ Β·op (π β π))) | ||
Theorem | idunop 31827 | The identity function (restricted to Hilbert space) is a unitary operator. (Contributed by NM, 21-Jan-2006.) (New usage is discouraged.) |
β’ ( I βΎ β) β UniOp | ||
Theorem | 0cnop 31828 | The identically zero function is a continuous Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
β’ 0hop β ContOp | ||
Theorem | 0cnfn 31829 | The identically zero function is a continuous Hilbert space functional. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
β’ ( β Γ {0}) β ContFn | ||
Theorem | idcnop 31830 | The identity function (restricted to Hilbert space) is a continuous operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
β’ ( I βΎ β) β ContOp | ||
Theorem | idhmop 31831 | The Hilbert space identity operator is a Hermitian operator. (Contributed by NM, 22-Apr-2006.) (New usage is discouraged.) |
β’ Iop β HrmOp | ||
Theorem | 0hmop 31832 | The identically zero function is a Hermitian operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.) |
β’ 0hop β HrmOp | ||
Theorem | 0lnop 31833 | The identically zero function is a linear Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
β’ 0hop β LinOp | ||
Theorem | 0lnfn 31834 | The identically zero function is a linear Hilbert space functional. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ ( β Γ {0}) β LinFn | ||
Theorem | nmop0 31835 | The norm of the zero operator is zero. (Contributed by NM, 8-Feb-2006.) (New usage is discouraged.) |
β’ (normopβ 0hop ) = 0 | ||
Theorem | nmfn0 31836 | The norm of the identically zero functional is zero. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
β’ (normfnβ( β Γ {0})) = 0 | ||
Theorem | hmopbdoptHIL 31837 | A Hermitian operator is a bounded linear operator (Hellinger-Toeplitz Theorem). (Contributed by NM, 18-Jan-2008.) (New usage is discouraged.) |
β’ (π β HrmOp β π β BndLinOp) | ||
Theorem | hoddii 31838 | Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 31629 does not require linearity.) (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π: ββΆ β & β’ π: ββΆ β β β’ (π β (π βop π)) = ((π β π) βop (π β π)) | ||
Theorem | hoddi 31839 | Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 31629 does not require linearity.) (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
β’ ((π β LinOp β§ π: ββΆ β β§ π: ββΆ β) β (π β (π βop π)) = ((π β π) βop (π β π))) | ||
Theorem | nmop0h 31840 | The norm of any operator on the trivial Hilbert space is zero. (This is the reason we need β β 0β in nmopun 31863.) (Contributed by NM, 24-Feb-2006.) (New usage is discouraged.) |
β’ (( β = 0β β§ π: ββΆ β) β (normopβπ) = 0) | ||
Theorem | idlnop 31841 | The identity function (restricted to Hilbert space) is a linear operator. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.) |
β’ ( I βΎ β) β LinOp | ||
Theorem | 0bdop 31842 | The identically zero operator is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ 0hop β BndLinOp | ||
Theorem | adj0 31843 | Adjoint of the zero operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
β’ (adjββ 0hop ) = 0hop | ||
Theorem | nmlnop0iALT 31844 | A linear operator with a zero norm is identically zero. (Contributed by NM, 8-Feb-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π β LinOp β β’ ((normopβπ) = 0 β π = 0hop ) | ||
Theorem | nmlnop0iHIL 31845 | A linear operator with a zero norm is identically zero. (Contributed by NM, 18-Jan-2008.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((normopβπ) = 0 β π = 0hop ) | ||
Theorem | nmlnopgt0i 31846 | A linear Hilbert space operator that is not identically zero has a positive norm. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
β’ π β LinOp β β’ (π β 0hop β 0 < (normopβπ)) | ||
Theorem | nmlnop0 31847 | A linear operator with a zero norm is identically zero. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
β’ (π β LinOp β ((normopβπ) = 0 β π = 0hop )) | ||
Theorem | nmlnopne0 31848 | A linear operator with a nonzero norm is nonzero. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
β’ (π β LinOp β ((normopβπ) β 0 β π β 0hop )) | ||
Theorem | lnopmi 31849 | The scalar product of a linear operator is a linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ π β LinOp β β’ (π΄ β β β (π΄ Β·op π) β LinOp) | ||
Theorem | lnophsi 31850 | The sum of two linear operators is linear. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β LinOp β β’ (π +op π) β LinOp | ||
Theorem | lnophdi 31851 | The difference of two linear operators is linear. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β LinOp β β’ (π βop π) β LinOp | ||
Theorem | lnopcoi 31852 | The composition of two linear operators is linear. (Contributed by NM, 8-Mar-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β LinOp β β’ (π β π) β LinOp | ||
Theorem | lnopco0i 31853 | The composition of a linear operator with one whose norm is zero. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β LinOp β β’ ((normopβπ) = 0 β (normopβ(π β π)) = 0) | ||
Theorem | lnopeq0lem1 31854 | Lemma for lnopeq0i 31856. Apply the generalized polarization identity polid2i 31006 to the quadratic form ((πβπ₯), π₯). (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π΄ β β & β’ π΅ β β β β’ ((πβπ΄) Β·ih π΅) = (((((πβ(π΄ +β π΅)) Β·ih (π΄ +β π΅)) β ((πβ(π΄ ββ π΅)) Β·ih (π΄ ββ π΅))) + (i Β· (((πβ(π΄ +β (i Β·β π΅))) Β·ih (π΄ +β (i Β·β π΅))) β ((πβ(π΄ ββ (i Β·β π΅))) Β·ih (π΄ ββ (i Β·β π΅)))))) / 4) | ||
Theorem | lnopeq0lem2 31855 | Lemma for lnopeq0i 31856. (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β) β ((πβπ΄) Β·ih π΅) = (((((πβ(π΄ +β π΅)) Β·ih (π΄ +β π΅)) β ((πβ(π΄ ββ π΅)) Β·ih (π΄ ββ π΅))) + (i Β· (((πβ(π΄ +β (i Β·β π΅))) Β·ih (π΄ +β (i Β·β π΅))) β ((πβ(π΄ ββ (i Β·β π΅))) Β·ih (π΄ ββ (i Β·β π΅)))))) / 4)) | ||
Theorem | lnopeq0i 31856* | A condition implying that a linear Hilbert space operator is identically zero. Unlike ho01i 31677 for arbitrary operators, when the operator is linear we need to consider only the values of the quadratic form (πβπ₯) Β·ih π₯). (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.) |
β’ π β LinOp β β’ (βπ₯ β β ((πβπ₯) Β·ih π₯) = 0 β π = 0hop ) | ||
Theorem | lnopeqi 31857* | Two linear Hilbert space operators are equal iff their quadratic forms are equal. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β LinOp β β’ (βπ₯ β β ((πβπ₯) Β·ih π₯) = ((πβπ₯) Β·ih π₯) β π = π) | ||
Theorem | lnopeq 31858* | Two linear Hilbert space operators are equal iff their quadratic forms are equal. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.) |
β’ ((π β LinOp β§ π β LinOp) β (βπ₯ β β ((πβπ₯) Β·ih π₯) = ((πβπ₯) Β·ih π₯) β π = π)) | ||
Theorem | lnopunilem1 31859* | Lemma for lnopunii 31861. (Contributed by NM, 14-May-2005.) (New usage is discouraged.) |
β’ π β LinOp & β’ βπ₯ β β (normββ(πβπ₯)) = (normββπ₯) & β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (ββ(πΆ Β· ((πβπ΄) Β·ih (πβπ΅)))) = (ββ(πΆ Β· (π΄ Β·ih π΅))) | ||
Theorem | lnopunilem2 31860* | Lemma for lnopunii 31861. (Contributed by NM, 12-May-2005.) (New usage is discouraged.) |
β’ π β LinOp & β’ βπ₯ β β (normββ(πβπ₯)) = (normββπ₯) & β’ π΄ β β & β’ π΅ β β β β’ ((πβπ΄) Β·ih (πβπ΅)) = (π΄ Β·ih π΅) | ||
Theorem | lnopunii 31861* | If a linear operator (whose range is β) is idempotent in the norm, the operator is unitary. Similar to theorem in [AkhiezerGlazman] p. 73. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π: ββontoβ β & β’ βπ₯ β β (normββ(πβπ₯)) = (normββπ₯) β β’ π β UniOp | ||
Theorem | elunop2 31862* | An operator is unitary iff it is linear, onto, and idempotent in the norm. Similar to theorem in [AkhiezerGlazman] p. 73, and its converse. (Contributed by NM, 24-Feb-2006.) (New usage is discouraged.) |
β’ (π β UniOp β (π β LinOp β§ π: ββontoβ β β§ βπ₯ β β (normββ(πβπ₯)) = (normββπ₯))) | ||
Theorem | nmopun 31863 | Norm of a unitary Hilbert space operator. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.) |
β’ (( β β 0β β§ π β UniOp) β (normopβπ) = 1) | ||
Theorem | unopbd 31864 | A unitary operator is a bounded linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ (π β UniOp β π β BndLinOp) | ||
Theorem | lnophmlem1 31865* | Lemma for lnophmi 31867. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ π β LinOp & β’ βπ₯ β β (π₯ Β·ih (πβπ₯)) β β β β’ (π΄ Β·ih (πβπ΄)) β β | ||
Theorem | lnophmlem2 31866* | Lemma for lnophmi 31867. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ π β LinOp & β’ βπ₯ β β (π₯ Β·ih (πβπ₯)) β β β β’ (π΄ Β·ih (πβπ΅)) = ((πβπ΄) Β·ih π΅) | ||
Theorem | lnophmi 31867* | A linear operator is Hermitian if π₯ Β·ih (πβπ₯) takes only real values. Remark in [ReedSimon] p. 195. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ βπ₯ β β (π₯ Β·ih (πβπ₯)) β β β β’ π β HrmOp | ||
Theorem | lnophm 31868* | A linear operator is Hermitian if π₯ Β·ih (πβπ₯) takes only real values. Remark in [ReedSimon] p. 195. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.) |
β’ ((π β LinOp β§ βπ₯ β β (π₯ Β·ih (πβπ₯)) β β) β π β HrmOp) | ||
Theorem | hmops 31869 | The sum of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
β’ ((π β HrmOp β§ π β HrmOp) β (π +op π) β HrmOp) | ||
Theorem | hmopm 31870 | The scalar product of a Hermitian operator with a real is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π β HrmOp) β (π΄ Β·op π) β HrmOp) | ||
Theorem | hmopd 31871 | The difference of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
β’ ((π β HrmOp β§ π β HrmOp) β (π βop π) β HrmOp) | ||
Theorem | hmopco 31872 | The composition of two commuting Hermitian operators is Hermitian. (Contributed by NM, 22-Aug-2006.) (New usage is discouraged.) |
β’ ((π β HrmOp β§ π β HrmOp β§ (π β π) = (π β π)) β (π β π) β HrmOp) | ||
Theorem | nmbdoplbi 31873 | A lower bound for the norm of a bounded linear operator. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ π β BndLinOp β β’ (π΄ β β β (normββ(πβπ΄)) β€ ((normopβπ) Β· (normββπ΄))) | ||
Theorem | nmbdoplb 31874 | A lower bound for the norm of a bounded linear Hilbert space operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
β’ ((π β BndLinOp β§ π΄ β β) β (normββ(πβπ΄)) β€ ((normopβπ) Β· (normββπ΄))) | ||
Theorem | nmcexi 31875* | Lemma for nmcopexi 31876 and nmcfnexi 31900. The norm of a continuous linear Hilbert space operator or functional exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by Mario Carneiro, 17-Nov-2013.) (Proof shortened by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ βπ¦ β β+ βπ§ β β ((normββπ§) < π¦ β (πβ(πβπ§)) < 1) & β’ (πβπ) = sup({π β£ βπ₯ β β ((normββπ₯) β€ 1 β§ π = (πβ(πβπ₯)))}, β*, < ) & β’ (π₯ β β β (πβ(πβπ₯)) β β) & β’ (πβ(πβ0β)) = 0 & β’ (((π¦ / 2) β β+ β§ π₯ β β) β ((π¦ / 2) Β· (πβ(πβπ₯))) = (πβ(πβ((π¦ / 2) Β·β π₯)))) β β’ (πβπ) β β | ||
Theorem | nmcopexi 31876 | The norm of a continuous linear Hilbert space operator exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by NM, 5-Feb-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β ContOp β β’ (normopβπ) β β | ||
Theorem | nmcoplbi 31877 | A lower bound for the norm of a continuous linear operator. Theorem 3.5(ii) of [Beran] p. 99. (Contributed by NM, 7-Feb-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β ContOp β β’ (π΄ β β β (normββ(πβπ΄)) β€ ((normopβπ) Β· (normββπ΄))) | ||
Theorem | nmcopex 31878 | The norm of a continuous linear Hilbert space operator exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
β’ ((π β LinOp β§ π β ContOp) β (normopβπ) β β) | ||
Theorem | nmcoplb 31879 | A lower bound for the norm of a continuous linear Hilbert space operator. Theorem 3.5(ii) of [Beran] p. 99. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
β’ ((π β LinOp β§ π β ContOp β§ π΄ β β) β (normββ(πβπ΄)) β€ ((normopβπ) Β· (normββπ΄))) | ||
Theorem | nmophmi 31880 | The norm of the scalar product of a bounded linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ π β BndLinOp β β’ (π΄ β β β (normopβ(π΄ Β·op π)) = ((absβπ΄) Β· (normopβπ))) | ||
Theorem | bdophmi 31881 | The scalar product of a bounded linear operator is a bounded linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ π β BndLinOp β β’ (π΄ β β β (π΄ Β·op π) β BndLinOp) | ||
Theorem | lnconi 31882* | Lemma for lnopconi 31883 and lnfnconi 31904. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
β’ (π β πΆ β π β β) & β’ ((π β πΆ β§ π¦ β β) β (πβ(πβπ¦)) β€ (π Β· (normββπ¦))) & β’ (π β πΆ β βπ₯ β β βπ§ β β+ βπ¦ β β+ βπ€ β β ((normββ(π€ ββ π₯)) < π¦ β (πβ((πβπ€)π(πβπ₯))) < π§)) & β’ (π¦ β β β (πβ(πβπ¦)) β β) & β’ ((π€ β β β§ π₯ β β) β (πβ(π€ ββ π₯)) = ((πβπ€)π(πβπ₯))) β β’ (π β πΆ β βπ₯ β β βπ¦ β β (πβ(πβπ¦)) β€ (π₯ Β· (normββπ¦))) | ||
Theorem | lnopconi 31883* | A condition equivalent to "π is continuous" when π is linear. Theorem 3.5(iii) of [Beran] p. 99. (Contributed by NM, 7-Feb-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
β’ π β LinOp β β’ (π β ContOp β βπ₯ β β βπ¦ β β (normββ(πβπ¦)) β€ (π₯ Β· (normββπ¦))) | ||
Theorem | lnopcon 31884* | A condition equivalent to "π is continuous" when π is linear. Theorem 3.5(iii) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ (π β LinOp β (π β ContOp β βπ₯ β β βπ¦ β β (normββ(πβπ¦)) β€ (π₯ Β· (normββπ¦)))) | ||
Theorem | lnopcnbd 31885 | A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ (π β LinOp β (π β ContOp β π β BndLinOp)) | ||
Theorem | lncnopbd 31886 | A continuous linear operator is a bounded linear operator. This theorem justifies our use of "bounded linear" as an interchangeable condition for "continuous linear" used in some textbook proofs. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
β’ (π β (LinOp β© ContOp) β π β BndLinOp) | ||
Theorem | lncnbd 31887 | A continuous linear operator is a bounded linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
β’ (LinOp β© ContOp) = BndLinOp | ||
Theorem | lnopcnre 31888 | A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ (π β LinOp β (π β ContOp β (normopβπ) β β)) | ||
Theorem | lnfnli 31889 | Basic property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πβ((π΄ Β·β π΅) +β πΆ)) = ((π΄ Β· (πβπ΅)) + (πβπΆ))) | ||
Theorem | lnfnfi 31890 | A linear Hilbert space functional is a functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ π: ββΆβ | ||
Theorem | lnfn0i 31891 | The value of a linear Hilbert space functional at zero is zero. Remark in [Beran] p. 99. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ (πβ0β) = 0 | ||
Theorem | lnfnaddi 31892 | Additive property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ ((π΄ β β β§ π΅ β β) β (πβ(π΄ +β π΅)) = ((πβπ΄) + (πβπ΅))) | ||
Theorem | lnfnmuli 31893 | Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ ((π΄ β β β§ π΅ β β) β (πβ(π΄ Β·β π΅)) = (π΄ Β· (πβπ΅))) | ||
Theorem | lnfnaddmuli 31894 | Sum/product property of a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πβ(π΅ +β (π΄ Β·β πΆ))) = ((πβπ΅) + (π΄ Β· (πβπΆ)))) | ||
Theorem | lnfnsubi 31895 | Subtraction property for a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ ((π΄ β β β§ π΅ β β) β (πβ(π΄ ββ π΅)) = ((πβπ΄) β (πβπ΅))) | ||
Theorem | lnfn0 31896 | The value of a linear Hilbert space functional at zero is zero. Remark in [Beran] p. 99. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
β’ (π β LinFn β (πβ0β) = 0) | ||
Theorem | lnfnmul 31897 | Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ ((π β LinFn β§ π΄ β β β§ π΅ β β) β (πβ(π΄ Β·β π΅)) = (π΄ Β· (πβπ΅))) | ||
Theorem | nmbdfnlbi 31898 | 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 31899 | 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 31900 | 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βπ) β β |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |