![]() |
Metamath
Proof Explorer Theorem List (p. 313 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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | kbop 31201 | 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 31202 | 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 31203 | Multiplication property of outer product. (Contributed by NM, 31-May-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ Β·β π΅) ketbra πΆ) = (π΅ ketbra ((ββπ΄) Β·β πΆ))) | ||
Theorem | kbpj 31204 | 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 31205* | 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 31206 | 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 31207 | Closure of an eigenvector of a Hilbert space operator. (Contributed by NM, 23-Mar-2006.) (New usage is discouraged.) |
β’ ((π: ββΆ β β§ π΄ β (eigvecβπ)) β π΄ β β) | ||
Theorem | eigvalval 31208 | 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 31209 | An eigenvalue is a complex number. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
β’ ((π: ββΆ β β§ π΄ β (eigvecβπ)) β ((eigvalβπ)βπ΄) β β) | ||
Theorem | eigvec1 31210 | Property of an eigenvector. (Contributed by NM, 12-Mar-2006.) (New usage is discouraged.) |
β’ ((π: ββΆ β β§ π΄ β (eigvecβπ)) β ((πβπ΄) = (((eigvalβπ)βπ΄) Β·β π΄) β§ π΄ β 0β)) | ||
Theorem | eighmre 31211 | 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 31212 | 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 31213 | Value of the norm of the negative of a Hilbert space operator. Unlike nmophmi 31279, the operator does not have to be bounded. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ π: ββΆ β β β’ (normopβ(-1 Β·op π)) = (normopβπ) | ||
Theorem | lnop0 31214 | 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 31215 | Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
β’ ((π β LinOp β§ π΄ β β β§ π΅ β β) β (πβ(π΄ Β·β π΅)) = (π΄ Β·β (πβπ΅))) | ||
Theorem | lnopli 31216 | Basic scalar product property of a linear Hilbert space operator. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πβ((π΄ Β·β π΅) +β πΆ)) = ((π΄ Β·β (πβπ΅)) +β (πβπΆ))) | ||
Theorem | lnopfi 31217 | A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.) |
β’ π β LinOp β β’ π: ββΆ β | ||
Theorem | lnop0i 31218 | 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 31219 | Additive property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β) β (πβ(π΄ +β π΅)) = ((πβπ΄) +β (πβπ΅))) | ||
Theorem | lnopmuli 31220 | Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β) β (πβ(π΄ Β·β π΅)) = (π΄ Β·β (πβπ΅))) | ||
Theorem | lnopaddmuli 31221 | Sum/product property of a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πβ(π΅ +β (π΄ Β·β πΆ))) = ((πβπ΅) +β (π΄ Β·β (πβπΆ)))) | ||
Theorem | lnopsubi 31222 | Subtraction property for a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β) β (πβ(π΄ ββ π΅)) = ((πβπ΄) ββ (πβπ΅))) | ||
Theorem | lnopsubmuli 31223 | Subtraction/product property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πβ(π΅ ββ (π΄ Β·β πΆ))) = ((πβπ΅) ββ (π΄ Β·β (πβπΆ)))) | ||
Theorem | lnopmulsubi 31224 | Product/subtraction property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πβ((π΄ Β·β π΅) ββ πΆ)) = ((π΄ Β·β (πβπ΅)) ββ (πβπΆ))) | ||
Theorem | homco2 31225 | Move a scalar product out of a composition of operators. The operator π must be linear, unlike homco1 31049 that works for any operators. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π β LinOp β§ π: ββΆ β) β (π β (π΄ Β·op π)) = (π΄ Β·op (π β π))) | ||
Theorem | idunop 31226 | 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 31227 | The identically zero function is a continuous Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
β’ 0hop β ContOp | ||
Theorem | 0cnfn 31228 | The identically zero function is a continuous Hilbert space functional. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
β’ ( β Γ {0}) β ContFn | ||
Theorem | idcnop 31229 | 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 31230 | The Hilbert space identity operator is a Hermitian operator. (Contributed by NM, 22-Apr-2006.) (New usage is discouraged.) |
β’ Iop β HrmOp | ||
Theorem | 0hmop 31231 | The identically zero function is a Hermitian operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.) |
β’ 0hop β HrmOp | ||
Theorem | 0lnop 31232 | The identically zero function is a linear Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
β’ 0hop β LinOp | ||
Theorem | 0lnfn 31233 | The identically zero function is a linear Hilbert space functional. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ ( β Γ {0}) β LinFn | ||
Theorem | nmop0 31234 | The norm of the zero operator is zero. (Contributed by NM, 8-Feb-2006.) (New usage is discouraged.) |
β’ (normopβ 0hop ) = 0 | ||
Theorem | nmfn0 31235 | The norm of the identically zero functional is zero. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
β’ (normfnβ( β Γ {0})) = 0 | ||
Theorem | hmopbdoptHIL 31236 | 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 31237 | Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 31028 does not require linearity.) (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π: ββΆ β & β’ π: ββΆ β β β’ (π β (π βop π)) = ((π β π) βop (π β π)) | ||
Theorem | hoddi 31238 | Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 31028 does not require linearity.) (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
β’ ((π β LinOp β§ π: ββΆ β β§ π: ββΆ β) β (π β (π βop π)) = ((π β π) βop (π β π))) | ||
Theorem | nmop0h 31239 | The norm of any operator on the trivial Hilbert space is zero. (This is the reason we need β β 0β in nmopun 31262.) (Contributed by NM, 24-Feb-2006.) (New usage is discouraged.) |
β’ (( β = 0β β§ π: ββΆ β) β (normopβπ) = 0) | ||
Theorem | idlnop 31240 | 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 31241 | The identically zero operator is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ 0hop β BndLinOp | ||
Theorem | adj0 31242 | Adjoint of the zero operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
β’ (adjββ 0hop ) = 0hop | ||
Theorem | nmlnop0iALT 31243 | 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 31244 | 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 31245 | 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 31246 | 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 31247 | 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 31248 | 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 31249 | The sum of two linear operators is linear. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β LinOp β β’ (π +op π) β LinOp | ||
Theorem | lnophdi 31250 | The difference of two linear operators is linear. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β LinOp β β’ (π βop π) β LinOp | ||
Theorem | lnopcoi 31251 | The composition of two linear operators is linear. (Contributed by NM, 8-Mar-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β LinOp β β’ (π β π) β LinOp | ||
Theorem | lnopco0i 31252 | 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 31253 | Lemma for lnopeq0i 31255. Apply the generalized polarization identity polid2i 30405 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 31254 | Lemma for lnopeq0i 31255. (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β) β ((πβπ΄) Β·ih π΅) = (((((πβ(π΄ +β π΅)) Β·ih (π΄ +β π΅)) β ((πβ(π΄ ββ π΅)) Β·ih (π΄ ββ π΅))) + (i Β· (((πβ(π΄ +β (i Β·β π΅))) Β·ih (π΄ +β (i Β·β π΅))) β ((πβ(π΄ ββ (i Β·β π΅))) Β·ih (π΄ ββ (i Β·β π΅)))))) / 4)) | ||
Theorem | lnopeq0i 31255* | A condition implying that a linear Hilbert space operator is identically zero. Unlike ho01i 31076 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 31256* | 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 31257* | 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 31258* | Lemma for lnopunii 31260. (Contributed by NM, 14-May-2005.) (New usage is discouraged.) |
β’ π β LinOp & β’ βπ₯ β β (normββ(πβπ₯)) = (normββπ₯) & β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (ββ(πΆ Β· ((πβπ΄) Β·ih (πβπ΅)))) = (ββ(πΆ Β· (π΄ Β·ih π΅))) | ||
Theorem | lnopunilem2 31259* | Lemma for lnopunii 31260. (Contributed by NM, 12-May-2005.) (New usage is discouraged.) |
β’ π β LinOp & β’ βπ₯ β β (normββ(πβπ₯)) = (normββπ₯) & β’ π΄ β β & β’ π΅ β β β β’ ((πβπ΄) Β·ih (πβπ΅)) = (π΄ Β·ih π΅) | ||
Theorem | lnopunii 31260* | 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 31261* | 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 31262 | Norm of a unitary Hilbert space operator. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.) |
β’ (( β β 0β β§ π β UniOp) β (normopβπ) = 1) | ||
Theorem | unopbd 31263 | A unitary operator is a bounded linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ (π β UniOp β π β BndLinOp) | ||
Theorem | lnophmlem1 31264* | Lemma for lnophmi 31266. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ π β LinOp & β’ βπ₯ β β (π₯ Β·ih (πβπ₯)) β β β β’ (π΄ Β·ih (πβπ΄)) β β | ||
Theorem | lnophmlem2 31265* | Lemma for lnophmi 31266. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ π β LinOp & β’ βπ₯ β β (π₯ Β·ih (πβπ₯)) β β β β’ (π΄ Β·ih (πβπ΅)) = ((πβπ΄) Β·ih π΅) | ||
Theorem | lnophmi 31266* | 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 31267* | 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 31268 | The sum of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
β’ ((π β HrmOp β§ π β HrmOp) β (π +op π) β HrmOp) | ||
Theorem | hmopm 31269 | 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 31270 | The difference of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
β’ ((π β HrmOp β§ π β HrmOp) β (π βop π) β HrmOp) | ||
Theorem | hmopco 31271 | The composition of two commuting Hermitian operators is Hermitian. (Contributed by NM, 22-Aug-2006.) (New usage is discouraged.) |
β’ ((π β HrmOp β§ π β HrmOp β§ (π β π) = (π β π)) β (π β π) β HrmOp) | ||
Theorem | nmbdoplbi 31272 | 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 31273 | 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 31274* | Lemma for nmcopexi 31275 and nmcfnexi 31299. 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 31275 | 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 31276 | 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 31277 | 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 31278 | 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 31279 | 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 31280 | 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 31281* | Lemma for lnopconi 31282 and lnfnconi 31303. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
β’ (π β πΆ β π β β) & β’ ((π β πΆ β§ π¦ β β) β (πβ(πβπ¦)) β€ (π Β· (normββπ¦))) & β’ (π β πΆ β βπ₯ β β βπ§ β β+ βπ¦ β β+ βπ€ β β ((normββ(π€ ββ π₯)) < π¦ β (πβ((πβπ€)π(πβπ₯))) < π§)) & β’ (π¦ β β β (πβ(πβπ¦)) β β) & β’ ((π€ β β β§ π₯ β β) β (πβ(π€ ββ π₯)) = ((πβπ€)π(πβπ₯))) β β’ (π β πΆ β βπ₯ β β βπ¦ β β (πβ(πβπ¦)) β€ (π₯ Β· (normββπ¦))) | ||
Theorem | lnopconi 31282* | 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 31283* | 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 31284 | A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ (π β LinOp β (π β ContOp β π β BndLinOp)) | ||
Theorem | lncnopbd 31285 | 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 31286 | A continuous linear operator is a bounded linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
β’ (LinOp β© ContOp) = BndLinOp | ||
Theorem | lnopcnre 31287 | A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ (π β LinOp β (π β ContOp β (normopβπ) β β)) | ||
Theorem | lnfnli 31288 | Basic property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πβ((π΄ Β·β π΅) +β πΆ)) = ((π΄ Β· (πβπ΅)) + (πβπΆ))) | ||
Theorem | lnfnfi 31289 | A linear Hilbert space functional is a functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ π: ββΆβ | ||
Theorem | lnfn0i 31290 | 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 31291 | Additive property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ ((π΄ β β β§ π΅ β β) β (πβ(π΄ +β π΅)) = ((πβπ΄) + (πβπ΅))) | ||
Theorem | lnfnmuli 31292 | Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ ((π΄ β β β§ π΅ β β) β (πβ(π΄ Β·β π΅)) = (π΄ Β· (πβπ΅))) | ||
Theorem | lnfnaddmuli 31293 | Sum/product property of a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πβ(π΅ +β (π΄ Β·β πΆ))) = ((πβπ΅) + (π΄ Β· (πβπΆ)))) | ||
Theorem | lnfnsubi 31294 | Subtraction property for a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ ((π΄ β β β§ π΅ β β) β (πβ(π΄ ββ π΅)) = ((πβπ΄) β (πβπ΅))) | ||
Theorem | lnfn0 31295 | 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 31296 | Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ ((π β LinFn β§ π΄ β β β§ π΅ β β) β (πβ(π΄ Β·β π΅)) = (π΄ Β· (πβπ΅))) | ||
Theorem | nmbdfnlbi 31297 | 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 31298 | 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 31299 | 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 31300 | 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ββπ΄))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |