![]() |
Metamath
Proof Explorer Theorem List (p. 319 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 | lnopco0i 31801 | 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 31802 | Lemma for lnopeq0i 31804. Apply the generalized polarization identity polid2i 30954 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 31803 | Lemma for lnopeq0i 31804. (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β) β ((πβπ΄) Β·ih π΅) = (((((πβ(π΄ +β π΅)) Β·ih (π΄ +β π΅)) β ((πβ(π΄ ββ π΅)) Β·ih (π΄ ββ π΅))) + (i Β· (((πβ(π΄ +β (i Β·β π΅))) Β·ih (π΄ +β (i Β·β π΅))) β ((πβ(π΄ ββ (i Β·β π΅))) Β·ih (π΄ ββ (i Β·β π΅)))))) / 4)) | ||
Theorem | lnopeq0i 31804* | A condition implying that a linear Hilbert space operator is identically zero. Unlike ho01i 31625 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 31805* | 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 31806* | 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 31807* | Lemma for lnopunii 31809. (Contributed by NM, 14-May-2005.) (New usage is discouraged.) |
β’ π β LinOp & β’ βπ₯ β β (normββ(πβπ₯)) = (normββπ₯) & β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (ββ(πΆ Β· ((πβπ΄) Β·ih (πβπ΅)))) = (ββ(πΆ Β· (π΄ Β·ih π΅))) | ||
Theorem | lnopunilem2 31808* | Lemma for lnopunii 31809. (Contributed by NM, 12-May-2005.) (New usage is discouraged.) |
β’ π β LinOp & β’ βπ₯ β β (normββ(πβπ₯)) = (normββπ₯) & β’ π΄ β β & β’ π΅ β β β β’ ((πβπ΄) Β·ih (πβπ΅)) = (π΄ Β·ih π΅) | ||
Theorem | lnopunii 31809* | 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 31810* | 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 31811 | Norm of a unitary Hilbert space operator. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.) |
β’ (( β β 0β β§ π β UniOp) β (normopβπ) = 1) | ||
Theorem | unopbd 31812 | A unitary operator is a bounded linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ (π β UniOp β π β BndLinOp) | ||
Theorem | lnophmlem1 31813* | Lemma for lnophmi 31815. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ π β LinOp & β’ βπ₯ β β (π₯ Β·ih (πβπ₯)) β β β β’ (π΄ Β·ih (πβπ΄)) β β | ||
Theorem | lnophmlem2 31814* | Lemma for lnophmi 31815. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ π β LinOp & β’ βπ₯ β β (π₯ Β·ih (πβπ₯)) β β β β’ (π΄ Β·ih (πβπ΅)) = ((πβπ΄) Β·ih π΅) | ||
Theorem | lnophmi 31815* | 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 31816* | 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 31817 | The sum of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
β’ ((π β HrmOp β§ π β HrmOp) β (π +op π) β HrmOp) | ||
Theorem | hmopm 31818 | 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 31819 | The difference of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
β’ ((π β HrmOp β§ π β HrmOp) β (π βop π) β HrmOp) | ||
Theorem | hmopco 31820 | The composition of two commuting Hermitian operators is Hermitian. (Contributed by NM, 22-Aug-2006.) (New usage is discouraged.) |
β’ ((π β HrmOp β§ π β HrmOp β§ (π β π) = (π β π)) β (π β π) β HrmOp) | ||
Theorem | nmbdoplbi 31821 | 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 31822 | 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 31823* | Lemma for nmcopexi 31824 and nmcfnexi 31848. 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 31824 | 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 31825 | 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 31826 | 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 31827 | 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 31828 | 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 31829 | 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 31830* | Lemma for lnopconi 31831 and lnfnconi 31852. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
β’ (π β πΆ β π β β) & β’ ((π β πΆ β§ π¦ β β) β (πβ(πβπ¦)) β€ (π Β· (normββπ¦))) & β’ (π β πΆ β βπ₯ β β βπ§ β β+ βπ¦ β β+ βπ€ β β ((normββ(π€ ββ π₯)) < π¦ β (πβ((πβπ€)π(πβπ₯))) < π§)) & β’ (π¦ β β β (πβ(πβπ¦)) β β) & β’ ((π€ β β β§ π₯ β β) β (πβ(π€ ββ π₯)) = ((πβπ€)π(πβπ₯))) β β’ (π β πΆ β βπ₯ β β βπ¦ β β (πβ(πβπ¦)) β€ (π₯ Β· (normββπ¦))) | ||
Theorem | lnopconi 31831* | 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 31832* | 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 31833 | A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ (π β LinOp β (π β ContOp β π β BndLinOp)) | ||
Theorem | lncnopbd 31834 | 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 31835 | A continuous linear operator is a bounded linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
β’ (LinOp β© ContOp) = BndLinOp | ||
Theorem | lnopcnre 31836 | A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ (π β LinOp β (π β ContOp β (normopβπ) β β)) | ||
Theorem | lnfnli 31837 | Basic property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πβ((π΄ Β·β π΅) +β πΆ)) = ((π΄ Β· (πβπ΅)) + (πβπΆ))) | ||
Theorem | lnfnfi 31838 | A linear Hilbert space functional is a functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ π: ββΆβ | ||
Theorem | lnfn0i 31839 | 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 31840 | Additive property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ ((π΄ β β β§ π΅ β β) β (πβ(π΄ +β π΅)) = ((πβπ΄) + (πβπ΅))) | ||
Theorem | lnfnmuli 31841 | Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ ((π΄ β β β§ π΅ β β) β (πβ(π΄ Β·β π΅)) = (π΄ Β· (πβπ΅))) | ||
Theorem | lnfnaddmuli 31842 | Sum/product property of a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πβ(π΅ +β (π΄ Β·β πΆ))) = ((πβπ΅) + (π΄ Β· (πβπΆ)))) | ||
Theorem | lnfnsubi 31843 | Subtraction property for a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ ((π΄ β β β§ π΅ β β) β (πβ(π΄ ββ π΅)) = ((πβπ΄) β (πβπ΅))) | ||
Theorem | lnfn0 31844 | 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 31845 | Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ ((π β LinFn β§ π΄ β β β§ π΅ β β) β (πβ(π΄ Β·β π΅)) = (π΄ Β· (πβπ΅))) | ||
Theorem | nmbdfnlbi 31846 | 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 31847 | 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 31848 | 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 31849 | 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 31850 | 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 31851 | 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 31852* | 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 31853* | 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 31854 | A linear functional is continuous iff it is bounded. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
β’ (π β LinFn β (π β ContFn β (normfnβπ) β β)) | ||
Theorem | imaelshi 31855 | 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 31856 | 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 31857 | 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 31858 | 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 31859* | 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 31860* | 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 31861* | A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104. See riesz2 31863 for the bounded linear functional version. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.) |
β’ (π β (LinFn β© ContFn) β β!π€ β β βπ£ β β (πβπ£) = (π£ Β·ih π€)) | ||
Theorem | riesz1 31862* | 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 31863. For the continuous linear functional version, see riesz3i 31859 and riesz4 31861. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
β’ (π β LinFn β ((normfnβπ) β β β βπ¦ β β βπ₯ β β (πβπ₯) = (π₯ Β·ih π¦))) | ||
Theorem | riesz2 31863* | 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 31862. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
β’ ((π β LinFn β§ (normfnβπ) β β) β β!π¦ β β βπ₯ β β (πβπ₯) = (π₯ Β·ih π¦)) | ||
Theorem | cnlnadjlem1 31864* | Lemma for cnlnadji 31873 (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 31865* | Lemma for cnlnadji 31873. πΊ is a continuous linear functional. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β ContOp & β’ πΊ = (π β β β¦ ((πβπ) Β·ih π¦)) β β’ (π¦ β β β (πΊ β LinFn β§ πΊ β ContFn)) | ||
Theorem | cnlnadjlem3 31866* | Lemma for cnlnadji 31873. By riesz4 31861, π΅ 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 31867* | Lemma for cnlnadji 31873. 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 31868* | Lemma for cnlnadji 31873. πΉ 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 31869* | Lemma for cnlnadji 31873. πΉ is linear. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β ContOp & β’ πΊ = (π β β β¦ ((πβπ) Β·ih π¦)) & β’ π΅ = (β©π€ β β βπ£ β β ((πβπ£) Β·ih π¦) = (π£ Β·ih π€)) & β’ πΉ = (π¦ β β β¦ π΅) β β’ πΉ β LinOp | ||
Theorem | cnlnadjlem7 31870* | Lemma for cnlnadji 31873. 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 31871* | Lemma for cnlnadji 31873. πΉ is continuous. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β ContOp & β’ πΊ = (π β β β¦ ((πβπ) Β·ih π¦)) & β’ π΅ = (β©π€ β β βπ£ β β ((πβπ£) Β·ih π¦) = (π£ Β·ih π€)) & β’ πΉ = (π¦ β β β¦ π΅) β β’ πΉ β ContOp | ||
Theorem | cnlnadjlem9 31872* | Lemma for cnlnadji 31873. πΉ 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 31873* | 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 31874* | 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 31875* | 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 31876* | 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 31877 | 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 31878 | Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
β’ BndLinOp β dom adjβ | ||
Theorem | bdopadj 31879 | Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
β’ (π β BndLinOp β π β dom adjβ) | ||
Theorem | adjbdln 31880 | 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 31881 | 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 31882 | 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 31883 | 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 31884 | Every operator with an adjoint is linear. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.) |
β’ dom adjβ β LinOp | ||
Theorem | nmopadjlei 31885 | 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 31886 | Lemma for nmopadji 31887. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
β’ π β BndLinOp β β’ (normopβ(adjββπ)) β€ (normopβπ) | ||
Theorem | nmopadji 31887 | 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 31888 | 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 31889 | 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 31890 | 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 31891 | 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 31892 | 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 31893 | 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 31894 | 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 31895 | The composition of two bounded linear operators is bounded. (Contributed by NM, 9-Mar-2006.) (New usage is discouraged.) |
β’ π β BndLinOp & β’ π β BndLinOp β β’ (π β π) β BndLinOp | ||
Theorem | nmoptri2i 31896 | 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 31897 | 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 31898 | 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 31899 | 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 31900 | 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 ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |