Home | Metamath
Proof Explorer Theorem List (p. 308 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lnopaddmuli 30701 | Sum/product property of a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.) |
โข ๐ โ LinOp โ โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐โ(๐ต +โ (๐ด ยทโ ๐ถ))) = ((๐โ๐ต) +โ (๐ด ยทโ (๐โ๐ถ)))) | ||
Theorem | lnopsubi 30702 | Subtraction property for a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.) |
โข ๐ โ LinOp โ โข ((๐ด โ โ โง ๐ต โ โ) โ (๐โ(๐ด โโ ๐ต)) = ((๐โ๐ด) โโ (๐โ๐ต))) | ||
Theorem | lnopsubmuli 30703 | Subtraction/product property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.) |
โข ๐ โ LinOp โ โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐โ(๐ต โโ (๐ด ยทโ ๐ถ))) = ((๐โ๐ต) โโ (๐ด ยทโ (๐โ๐ถ)))) | ||
Theorem | lnopmulsubi 30704 | Product/subtraction property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.) |
โข ๐ โ LinOp โ โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐โ((๐ด ยทโ ๐ต) โโ ๐ถ)) = ((๐ด ยทโ (๐โ๐ต)) โโ (๐โ๐ถ))) | ||
Theorem | homco2 30705 | Move a scalar product out of a composition of operators. The operator ๐ must be linear, unlike homco1 30529 that works for any operators. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐ โ LinOp โง ๐: โโถ โ) โ (๐ โ (๐ด ยทop ๐)) = (๐ด ยทop (๐ โ ๐))) | ||
Theorem | idunop 30706 | 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 30707 | The identically zero function is a continuous Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
โข 0hop โ ContOp | ||
Theorem | 0cnfn 30708 | The identically zero function is a continuous Hilbert space functional. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
โข ( โ ร {0}) โ ContFn | ||
Theorem | idcnop 30709 | 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 30710 | The Hilbert space identity operator is a Hermitian operator. (Contributed by NM, 22-Apr-2006.) (New usage is discouraged.) |
โข Iop โ HrmOp | ||
Theorem | 0hmop 30711 | The identically zero function is a Hermitian operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.) |
โข 0hop โ HrmOp | ||
Theorem | 0lnop 30712 | The identically zero function is a linear Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
โข 0hop โ LinOp | ||
Theorem | 0lnfn 30713 | The identically zero function is a linear Hilbert space functional. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
โข ( โ ร {0}) โ LinFn | ||
Theorem | nmop0 30714 | The norm of the zero operator is zero. (Contributed by NM, 8-Feb-2006.) (New usage is discouraged.) |
โข (normopโ 0hop ) = 0 | ||
Theorem | nmfn0 30715 | The norm of the identically zero functional is zero. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
โข (normfnโ( โ ร {0})) = 0 | ||
Theorem | hmopbdoptHIL 30716 | 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 30717 | Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 30508 does not require linearity.) (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
โข ๐ โ LinOp & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ โ (๐ โop ๐)) = ((๐ โ ๐) โop (๐ โ ๐)) | ||
Theorem | hoddi 30718 | Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 30508 does not require linearity.) (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
โข ((๐ โ LinOp โง ๐: โโถ โ โง ๐: โโถ โ) โ (๐ โ (๐ โop ๐)) = ((๐ โ ๐) โop (๐ โ ๐))) | ||
Theorem | nmop0h 30719 | The norm of any operator on the trivial Hilbert space is zero. (This is the reason we need โ โ 0โ in nmopun 30742.) (Contributed by NM, 24-Feb-2006.) (New usage is discouraged.) |
โข (( โ = 0โ โง ๐: โโถ โ) โ (normopโ๐) = 0) | ||
Theorem | idlnop 30720 | 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 30721 | The identically zero operator is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
โข 0hop โ BndLinOp | ||
Theorem | adj0 30722 | Adjoint of the zero operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
โข (adjโโ 0hop ) = 0hop | ||
Theorem | nmlnop0iALT 30723 | 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 30724 | 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 30725 | 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 30726 | 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 30727 | 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 30728 | 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 30729 | The sum of two linear operators is linear. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
โข ๐ โ LinOp & โข ๐ โ LinOp โ โข (๐ +op ๐) โ LinOp | ||
Theorem | lnophdi 30730 | The difference of two linear operators is linear. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.) |
โข ๐ โ LinOp & โข ๐ โ LinOp โ โข (๐ โop ๐) โ LinOp | ||
Theorem | lnopcoi 30731 | The composition of two linear operators is linear. (Contributed by NM, 8-Mar-2006.) (New usage is discouraged.) |
โข ๐ โ LinOp & โข ๐ โ LinOp โ โข (๐ โ ๐) โ LinOp | ||
Theorem | lnopco0i 30732 | 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 30733 | Lemma for lnopeq0i 30735. Apply the generalized polarization identity polid2i 29885 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 30734 | Lemma for lnopeq0i 30735. (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.) |
โข ๐ โ LinOp โ โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐โ๐ด) ยทih ๐ต) = (((((๐โ(๐ด +โ ๐ต)) ยทih (๐ด +โ ๐ต)) โ ((๐โ(๐ด โโ ๐ต)) ยทih (๐ด โโ ๐ต))) + (i ยท (((๐โ(๐ด +โ (i ยทโ ๐ต))) ยทih (๐ด +โ (i ยทโ ๐ต))) โ ((๐โ(๐ด โโ (i ยทโ ๐ต))) ยทih (๐ด โโ (i ยทโ ๐ต)))))) / 4)) | ||
Theorem | lnopeq0i 30735* | A condition implying that a linear Hilbert space operator is identically zero. Unlike ho01i 30556 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 30736* | 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 30737* | 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 30738* | Lemma for lnopunii 30740. (Contributed by NM, 14-May-2005.) (New usage is discouraged.) |
โข ๐ โ LinOp & โข โ๐ฅ โ โ (normโโ(๐โ๐ฅ)) = (normโโ๐ฅ) & โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข (โโ(๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต)))) = (โโ(๐ถ ยท (๐ด ยทih ๐ต))) | ||
Theorem | lnopunilem2 30739* | Lemma for lnopunii 30740. (Contributed by NM, 12-May-2005.) (New usage is discouraged.) |
โข ๐ โ LinOp & โข โ๐ฅ โ โ (normโโ(๐โ๐ฅ)) = (normโโ๐ฅ) & โข ๐ด โ โ & โข ๐ต โ โ โ โข ((๐โ๐ด) ยทih (๐โ๐ต)) = (๐ด ยทih ๐ต) | ||
Theorem | lnopunii 30740* | 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 30741* | 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 30742 | Norm of a unitary Hilbert space operator. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.) |
โข (( โ โ 0โ โง ๐ โ UniOp) โ (normopโ๐) = 1) | ||
Theorem | unopbd 30743 | A unitary operator is a bounded linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
โข (๐ โ UniOp โ ๐ โ BndLinOp) | ||
Theorem | lnophmlem1 30744* | Lemma for lnophmi 30746. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ โ LinOp & โข โ๐ฅ โ โ (๐ฅ ยทih (๐โ๐ฅ)) โ โ โ โข (๐ด ยทih (๐โ๐ด)) โ โ | ||
Theorem | lnophmlem2 30745* | Lemma for lnophmi 30746. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ โ LinOp & โข โ๐ฅ โ โ (๐ฅ ยทih (๐โ๐ฅ)) โ โ โ โข (๐ด ยทih (๐โ๐ต)) = ((๐โ๐ด) ยทih ๐ต) | ||
Theorem | lnophmi 30746* | 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 30747* | 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 30748 | The sum of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
โข ((๐ โ HrmOp โง ๐ โ HrmOp) โ (๐ +op ๐) โ HrmOp) | ||
Theorem | hmopm 30749 | 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 30750 | The difference of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
โข ((๐ โ HrmOp โง ๐ โ HrmOp) โ (๐ โop ๐) โ HrmOp) | ||
Theorem | hmopco 30751 | The composition of two commuting Hermitian operators is Hermitian. (Contributed by NM, 22-Aug-2006.) (New usage is discouraged.) |
โข ((๐ โ HrmOp โง ๐ โ HrmOp โง (๐ โ ๐) = (๐ โ ๐)) โ (๐ โ ๐) โ HrmOp) | ||
Theorem | nmbdoplbi 30752 | 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 30753 | 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 30754* | Lemma for nmcopexi 30755 and nmcfnexi 30779. 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 30755 | 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 30756 | 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 30757 | 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 30758 | 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 30759 | 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 30760 | 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 30761* | Lemma for lnopconi 30762 and lnfnconi 30783. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
โข (๐ โ ๐ถ โ ๐ โ โ) & โข ((๐ โ ๐ถ โง ๐ฆ โ โ) โ (๐โ(๐โ๐ฆ)) โค (๐ ยท (normโโ๐ฆ))) & โข (๐ โ ๐ถ โ โ๐ฅ โ โ โ๐ง โ โ+ โ๐ฆ โ โ+ โ๐ค โ โ ((normโโ(๐ค โโ ๐ฅ)) < ๐ฆ โ (๐โ((๐โ๐ค)๐(๐โ๐ฅ))) < ๐ง)) & โข (๐ฆ โ โ โ (๐โ(๐โ๐ฆ)) โ โ) & โข ((๐ค โ โ โง ๐ฅ โ โ) โ (๐โ(๐ค โโ ๐ฅ)) = ((๐โ๐ค)๐(๐โ๐ฅ))) โ โข (๐ โ ๐ถ โ โ๐ฅ โ โ โ๐ฆ โ โ (๐โ(๐โ๐ฆ)) โค (๐ฅ ยท (normโโ๐ฆ))) | ||
Theorem | lnopconi 30762* | 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 30763* | 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 30764 | A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
โข (๐ โ LinOp โ (๐ โ ContOp โ ๐ โ BndLinOp)) | ||
Theorem | lncnopbd 30765 | 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 30766 | A continuous linear operator is a bounded linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
โข (LinOp โฉ ContOp) = BndLinOp | ||
Theorem | lnopcnre 30767 | A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
โข (๐ โ LinOp โ (๐ โ ContOp โ (normopโ๐) โ โ)) | ||
Theorem | lnfnli 30768 | Basic property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
โข ๐ โ LinFn โ โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐โ((๐ด ยทโ ๐ต) +โ ๐ถ)) = ((๐ด ยท (๐โ๐ต)) + (๐โ๐ถ))) | ||
Theorem | lnfnfi 30769 | A linear Hilbert space functional is a functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
โข ๐ โ LinFn โ โข ๐: โโถโ | ||
Theorem | lnfn0i 30770 | 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 30771 | Additive property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
โข ๐ โ LinFn โ โข ((๐ด โ โ โง ๐ต โ โ) โ (๐โ(๐ด +โ ๐ต)) = ((๐โ๐ด) + (๐โ๐ต))) | ||
Theorem | lnfnmuli 30772 | Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
โข ๐ โ LinFn โ โข ((๐ด โ โ โง ๐ต โ โ) โ (๐โ(๐ด ยทโ ๐ต)) = (๐ด ยท (๐โ๐ต))) | ||
Theorem | lnfnaddmuli 30773 | Sum/product property of a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
โข ๐ โ LinFn โ โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐โ(๐ต +โ (๐ด ยทโ ๐ถ))) = ((๐โ๐ต) + (๐ด ยท (๐โ๐ถ)))) | ||
Theorem | lnfnsubi 30774 | Subtraction property for a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
โข ๐ โ LinFn โ โข ((๐ด โ โ โง ๐ต โ โ) โ (๐โ(๐ด โโ ๐ต)) = ((๐โ๐ด) โ (๐โ๐ต))) | ||
Theorem | lnfn0 30775 | 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 30776 | Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
โข ((๐ โ LinFn โง ๐ด โ โ โง ๐ต โ โ) โ (๐โ(๐ด ยทโ ๐ต)) = (๐ด ยท (๐โ๐ต))) | ||
Theorem | nmbdfnlbi 30777 | 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 30778 | 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 30779 | 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 30780 | 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 30781 | 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 30782 | 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 30783* | 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 30784* | 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 30785 | A linear functional is continuous iff it is bounded. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
โข (๐ โ LinFn โ (๐ โ ContFn โ (normfnโ๐) โ โ)) | ||
Theorem | imaelshi 30786 | 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 30787 | 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 30788 | 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 30789 | 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 30790* | 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 30791* | 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 30792* | A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104. See riesz2 30794 for the bounded linear functional version. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.) |
โข (๐ โ (LinFn โฉ ContFn) โ โ!๐ค โ โ โ๐ฃ โ โ (๐โ๐ฃ) = (๐ฃ ยทih ๐ค)) | ||
Theorem | riesz1 30793* | 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 30794. For the continuous linear functional version, see riesz3i 30790 and riesz4 30792. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
โข (๐ โ LinFn โ ((normfnโ๐) โ โ โ โ๐ฆ โ โ โ๐ฅ โ โ (๐โ๐ฅ) = (๐ฅ ยทih ๐ฆ))) | ||
Theorem | riesz2 30794* | 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 30793. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
โข ((๐ โ LinFn โง (normfnโ๐) โ โ) โ โ!๐ฆ โ โ โ๐ฅ โ โ (๐โ๐ฅ) = (๐ฅ ยทih ๐ฆ)) | ||
Theorem | cnlnadjlem1 30795* | Lemma for cnlnadji 30804 (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 30796* | Lemma for cnlnadji 30804. ๐บ is a continuous linear functional. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.) |
โข ๐ โ LinOp & โข ๐ โ ContOp & โข ๐บ = (๐ โ โ โฆ ((๐โ๐) ยทih ๐ฆ)) โ โข (๐ฆ โ โ โ (๐บ โ LinFn โง ๐บ โ ContFn)) | ||
Theorem | cnlnadjlem3 30797* | Lemma for cnlnadji 30804. By riesz4 30792, ๐ต 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 30798* | Lemma for cnlnadji 30804. 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 30799* | Lemma for cnlnadji 30804. ๐น 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 30800* | Lemma for cnlnadji 30804. ๐น is linear. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.) |
โข ๐ โ LinOp & โข ๐ โ ContOp & โข ๐บ = (๐ โ โ โฆ ((๐โ๐) ยทih ๐ฆ)) & โข ๐ต = (โฉ๐ค โ โ โ๐ฃ โ โ ((๐โ๐ฃ) ยทih ๐ฆ) = (๐ฃ ยทih ๐ค)) & โข ๐น = (๐ฆ โ โ โฆ ๐ต) โ โข ๐น โ LinOp |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |