Home | Metamath
Proof Explorer Theorem List (p. 297 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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ajval 29601* | Value of the adjoint function. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) & β’ π = (Β·πOLDβπ) & β’ π΄ = (πadjπ) β β’ ((π β CPreHilOLD β§ π β NrmCVec β§ π:πβΆπ) β (π΄βπ) = (β©π (π :πβΆπ β§ βπ₯ β π βπ¦ β π ((πβπ₯)ππ¦) = (π₯π(π βπ¦))))) | ||
Syntax | ccbn 29602 | Extend class notation with the class of all complex Banach spaces. |
class CBan | ||
Definition | df-cbn 29603 | Define the class of all complex Banach spaces. (Contributed by NM, 5-Dec-2006.) Use df-bn 24622 instead. (New usage is discouraged.) |
β’ CBan = {π’ β NrmCVec β£ (IndMetβπ’) β (CMetβ(BaseSetβπ’))} | ||
Theorem | iscbn 29604 | A complex Banach space is a normed complex vector space with a complete induced metric. (Contributed by NM, 5-Dec-2006.) Use isbn 24624 instead. (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π· = (IndMetβπ) β β’ (π β CBan β (π β NrmCVec β§ π· β (CMetβπ))) | ||
Theorem | cbncms 29605 | The induced metric on complex Banach space is complete. (Contributed by NM, 8-Sep-2007.) Use bncmet 24633 (or preferably bncms 24630) instead. (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π· = (IndMetβπ) β β’ (π β CBan β π· β (CMetβπ)) | ||
Theorem | bnnv 29606 | Every complex Banach space is a normed complex vector space. (Contributed by NM, 17-Mar-2007.) Use bnnvc 24626 instead. (New usage is discouraged.) |
β’ (π β CBan β π β NrmCVec) | ||
Theorem | bnrel 29607 | The class of all complex Banach spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
β’ Rel CBan | ||
Theorem | bnsscmcl 29608 | A subspace of a Banach space is a Banach space iff it is closed in the norm-induced metric of the parent space. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π» = (SubSpβπ) & β’ π = (BaseSetβπ) β β’ ((π β CBan β§ π β π») β (π β CBan β π β (Clsdβπ½))) | ||
Theorem | cnbn 29609 | The set of complex numbers is a complex Banach space. (Contributed by Steve Rodriguez, 4-Jan-2007.) (New usage is discouraged.) |
β’ π = β¨β¨ + , Β· β©, absβ© β β’ π β CBan | ||
Theorem | ubthlem1 29610* | Lemma for ubth 29613. The function π΄ exhibits a countable collection of sets that are closed, being the inverse image under π‘ of the closed ball of radius π, and by assumption they cover π. Thus, by the Baire Category theorem bcth2 24616, for some π the set π΄βπ has an interior, meaning that there is a closed ball {π§ β π β£ (π¦π·π§) β€ π} in the set. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π β CBan & β’ π β NrmCVec & β’ (π β π β (π BLnOp π)) & β’ (π β βπ₯ β π βπ β β βπ‘ β π (πβ(π‘βπ₯)) β€ π) & β’ π΄ = (π β β β¦ {π§ β π β£ βπ‘ β π (πβ(π‘βπ§)) β€ π}) β β’ (π β βπ β β βπ¦ β π βπ β β+ {π§ β π β£ (π¦π·π§) β€ π} β (π΄βπ)) | ||
Theorem | ubthlem2 29611* | Lemma for ubth 29613. Given that there is a closed ball π΅(π, π ) in π΄βπΎ, for any π₯ β π΅(0, 1), we have π + π Β· π₯ β π΅(π, π ) and π β π΅(π, π ), so both of these have norm(π‘(π§)) β€ πΎ and so norm(π‘(π₯ )) β€ (norm(π‘(π)) + norm(π‘(π + π Β· π₯))) / π β€ ( πΎ + πΎ) / π , which is our desired uniform bound. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π β CBan & β’ π β NrmCVec & β’ (π β π β (π BLnOp π)) & β’ (π β βπ₯ β π βπ β β βπ‘ β π (πβ(π‘βπ₯)) β€ π) & β’ π΄ = (π β β β¦ {π§ β π β£ βπ‘ β π (πβ(π‘βπ§)) β€ π}) & β’ (π β πΎ β β) & β’ (π β π β π) & β’ (π β π β β+) & β’ (π β {π§ β π β£ (ππ·π§) β€ π } β (π΄βπΎ)) β β’ (π β βπ β β βπ‘ β π ((π normOpOLD π)βπ‘) β€ π) | ||
Theorem | ubthlem3 29612* | Lemma for ubth 29613. Prove the reverse implication, using nmblolbi 29540. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π β CBan & β’ π β NrmCVec & β’ (π β π β (π BLnOp π)) β β’ (π β (βπ₯ β π βπ β β βπ‘ β π (πβ(π‘βπ₯)) β€ π β βπ β β βπ‘ β π ((π normOpOLD π)βπ‘) β€ π)) | ||
Theorem | ubth 29613* | Uniform Boundedness Theorem, also called the Banach-Steinhaus Theorem. Let π be a collection of bounded linear operators on a Banach space. If, for every vector π₯, the norms of the operators' values are bounded, then the operators' norms are also bounded. Theorem 4.7-3 of [Kreyszig] p. 249. See also http://en.wikipedia.org/wiki/Uniform_boundedness_principle. (Contributed by NM, 7-Nov-2007.) (Proof shortened by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (π normOpOLD π) β β’ ((π β CBan β§ π β NrmCVec β§ π β (π BLnOp π)) β (βπ₯ β π βπ β β βπ‘ β π (πβ(π‘βπ₯)) β€ π β βπ β β βπ‘ β π (πβπ‘) β€ π)) | ||
Theorem | minvecolem1 29614* | Lemma for minveco 29624. The set of all distances from points of π to π΄ are a nonempty set of nonnegative reals. (Contributed by Mario Carneiro, 8-May-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) β β’ (π β (π β β β§ π β β β§ βπ€ β π 0 β€ π€)) | ||
Theorem | minvecolem2 29615* | Lemma for minveco 29624. Any two points πΎ and πΏ in π are close to each other if they are close to the infimum of distance to π΄. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) & β’ (π β π΅ β β) & β’ (π β 0 β€ π΅) & β’ (π β πΎ β π) & β’ (π β πΏ β π) & β’ (π β ((π΄π·πΎ)β2) β€ ((πβ2) + π΅)) & β’ (π β ((π΄π·πΏ)β2) β€ ((πβ2) + π΅)) β β’ (π β ((πΎπ·πΏ)β2) β€ (4 Β· π΅)) | ||
Theorem | minvecolem3 29616* | Lemma for minveco 29624. The sequence formed by taking elements successively closer to the infimum is Cauchy. (Contributed by Mario Carneiro, 8-May-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) & β’ (π β πΉ:ββΆπ) & β’ ((π β§ π β β) β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π))) β β’ (π β πΉ β (Cauβπ·)) | ||
Theorem | minvecolem4a 29617* | Lemma for minveco 29624. πΉ is convergent in the subspace topology on π. (Contributed by Mario Carneiro, 7-May-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) & β’ (π β πΉ:ββΆπ) & β’ ((π β§ π β β) β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π))) β β’ (π β πΉ(βπ‘β(MetOpenβ(π· βΎ (π Γ π))))((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ)) | ||
Theorem | minvecolem4b 29618* | Lemma for minveco 29624. The convergent point of the cauchy sequence πΉ is a member of the base space. (Contributed by Mario Carneiro, 16-Jun-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) & β’ (π β πΉ:ββΆπ) & β’ ((π β§ π β β) β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π))) β β’ (π β ((βπ‘βπ½)βπΉ) β π) | ||
Theorem | minvecolem4c 29619* | Lemma for minveco 29624. The infimum of the distances to π΄ is a real number. (Contributed by Mario Carneiro, 16-Jun-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) & β’ (π β πΉ:ββΆπ) & β’ ((π β§ π β β) β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π))) β β’ (π β π β β) | ||
Theorem | minvecolem4 29620* | Lemma for minveco 29624. The convergent point of the cauchy sequence πΉ attains the minimum distance, and so is closer to π΄ than any other point in π. (Contributed by Mario Carneiro, 7-May-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) & β’ (π β πΉ:ββΆπ) & β’ ((π β§ π β β) β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π))) & β’ π = (1 / (((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β (πβ2))) β β’ (π β βπ₯ β π βπ¦ β π (πβ(π΄ππ₯)) β€ (πβ(π΄ππ¦))) | ||
Theorem | minvecolem5 29621* | Lemma for minveco 29624. Discharge the assumption about the sequence πΉ by applying countable choice ax-cc 10304. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) β β’ (π β βπ₯ β π βπ¦ β π (πβ(π΄ππ₯)) β€ (πβ(π΄ππ¦))) | ||
Theorem | minvecolem6 29622* | Lemma for minveco 29624. Any minimal point is less than π away from π΄. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) β β’ ((π β§ π₯ β π) β (((π΄π·π₯)β2) β€ ((πβ2) + 0) β βπ¦ β π (πβ(π΄ππ₯)) β€ (πβ(π΄ππ¦)))) | ||
Theorem | minvecolem7 29623* | Lemma for minveco 29624. Since any two minimal points are distance zero away from each other, the minimal point is unique. (Contributed by Mario Carneiro, 9-May-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) β β’ (π β β!π₯ β π βπ¦ β π (πβ(π΄ππ₯)) β€ (πβ(π΄ππ¦))) | ||
Theorem | minveco 29624* | Minimizing vector theorem, or the Hilbert projection theorem. There is exactly one vector in a complete subspace π that minimizes the distance to an arbitrary vector π΄ in a parent inner product space. Theorem 3.3-1 of [Kreyszig] p. 144, specialized to subspaces instead of convex subsets. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Mario Carneiro, 9-May-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) β β’ (π β β!π₯ β π βπ¦ β π (πβ(π΄ππ₯)) β€ (πβ(π΄ππ¦))) | ||
Syntax | chlo 29625 | Extend class notation with the class of all complex Hilbert spaces. |
class CHilOLD | ||
Definition | df-hlo 29626 | Define the class of all complex Hilbert spaces. A Hilbert space is a Banach space which is also an inner product space. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
β’ CHilOLD = (CBan β© CPreHilOLD) | ||
Theorem | ishlo 29627 | The predicate "is a complex Hilbert space." A Hilbert space is a Banach space which is also an inner product space, i.e. whose norm satisfies the parallelogram law. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
β’ (π β CHilOLD β (π β CBan β§ π β CPreHilOLD)) | ||
Theorem | hlobn 29628 | Every complex Hilbert space is a complex Banach space. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
β’ (π β CHilOLD β π β CBan) | ||
Theorem | hlph 29629 | Every complex Hilbert space is an inner product space (also called a pre-Hilbert space). (Contributed by NM, 28-Apr-2007.) (New usage is discouraged.) |
β’ (π β CHilOLD β π β CPreHilOLD) | ||
Theorem | hlrel 29630 | The class of all complex Hilbert spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
β’ Rel CHilOLD | ||
Theorem | hlnv 29631 | Every complex Hilbert space is a normed complex vector space. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
β’ (π β CHilOLD β π β NrmCVec) | ||
Theorem | hlnvi 29632 | Every complex Hilbert space is a normed complex vector space. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.) |
β’ π β CHilOLD β β’ π β NrmCVec | ||
Theorem | hlvc 29633 | Every complex Hilbert space is a complex vector space. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (1st βπ) β β’ (π β CHilOLD β π β CVecOLD) | ||
Theorem | hlcmet 29634 | The induced metric on a complex Hilbert space is complete. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π· = (IndMetβπ) β β’ (π β CHilOLD β π· β (CMetβπ)) | ||
Theorem | hlmet 29635 | The induced metric on a complex Hilbert space. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π· = (IndMetβπ) β β’ (π β CHilOLD β π· β (Metβπ)) | ||
Theorem | hlpar2 29636 | The parallelogram law satisfied by Hilbert space vectors. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) β β’ ((π β CHilOLD β§ π΄ β π β§ π΅ β π) β (((πβ(π΄πΊπ΅))β2) + ((πβ(π΄ππ΅))β2)) = (2 Β· (((πβπ΄)β2) + ((πβπ΅)β2)))) | ||
Theorem | hlpar 29637 | The parallelogram law satisfied by Hilbert space vectors. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (normCVβπ) β β’ ((π β CHilOLD β§ π΄ β π β§ π΅ β π) β (((πβ(π΄πΊπ΅))β2) + ((πβ(π΄πΊ(-1ππ΅)))β2)) = (2 Β· (((πβπ΄)β2) + ((πβπ΅)β2)))) | ||
Theorem | hlex 29638 | The base set of a Hilbert space is a set. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) β β’ π β V | ||
Theorem | hladdf 29639 | Mapping for Hilbert space vector addition. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) β β’ (π β CHilOLD β πΊ:(π Γ π)βΆπ) | ||
Theorem | hlcom 29640 | Hilbert space vector addition is commutative. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) β β’ ((π β CHilOLD β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) = (π΅πΊπ΄)) | ||
Theorem | hlass 29641 | Hilbert space vector addition is associative. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) β β’ ((π β CHilOLD β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)πΊπΆ) = (π΄πΊ(π΅πΊπΆ))) | ||
Theorem | hl0cl 29642 | The Hilbert space zero vector. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (0vecβπ) β β’ (π β CHilOLD β π β π) | ||
Theorem | hladdid 29643 | Hilbert space addition with the zero vector. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = (0vecβπ) β β’ ((π β CHilOLD β§ π΄ β π) β (π΄πΊπ) = π΄) | ||
Theorem | hlmulf 29644 | Mapping for Hilbert space scalar multiplication. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) β β’ (π β CHilOLD β π:(β Γ π)βΆπ) | ||
Theorem | hlmulid 29645 | Hilbert space scalar multiplication by one. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) β β’ ((π β CHilOLD β§ π΄ β π) β (1ππ΄) = π΄) | ||
Theorem | hlmulass 29646 | Hilbert space scalar multiplication associative law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) β β’ ((π β CHilOLD β§ (π΄ β β β§ π΅ β β β§ πΆ β π)) β ((π΄ Β· π΅)ππΆ) = (π΄π(π΅ππΆ))) | ||
Theorem | hldi 29647 | Hilbert space scalar multiplication distributive law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) β β’ ((π β CHilOLD β§ (π΄ β β β§ π΅ β π β§ πΆ β π)) β (π΄π(π΅πΊπΆ)) = ((π΄ππ΅)πΊ(π΄ππΆ))) | ||
Theorem | hldir 29648 | Hilbert space scalar multiplication distributive law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) β β’ ((π β CHilOLD β§ (π΄ β β β§ π΅ β β β§ πΆ β π)) β ((π΄ + π΅)ππΆ) = ((π΄ππΆ)πΊ(π΅ππΆ))) | ||
Theorem | hlmul0 29649 | Hilbert space scalar multiplication by zero. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) & β’ π = (0vecβπ) β β’ ((π β CHilOLD β§ π΄ β π) β (0ππ΄) = π) | ||
Theorem | hlipf 29650 | Mapping for Hilbert space inner product. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) β β’ (π β CHilOLD β π:(π Γ π)βΆβ) | ||
Theorem | hlipcj 29651 | Conjugate law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CHilOLD β§ π΄ β π β§ π΅ β π) β (π΄ππ΅) = (ββ(π΅ππ΄))) | ||
Theorem | hlipdir 29652 | Distributive law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CHilOLD β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)ππΆ) = ((π΄ππΆ) + (π΅ππΆ))) | ||
Theorem | hlipass 29653 | Associative law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CHilOLD β§ (π΄ β β β§ π΅ β π β§ πΆ β π)) β ((π΄ππ΅)ππΆ) = (π΄ Β· (π΅ππΆ))) | ||
Theorem | hlipgt0 29654 | The inner product of a Hilbert space vector by itself is positive. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (0vecβπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CHilOLD β§ π΄ β π β§ π΄ β π) β 0 < (π΄ππ΄)) | ||
Theorem | hlcompl 29655 | Completeness of a Hilbert space. (Contributed by NM, 8-Sep-2007.) (Revised by Mario Carneiro, 9-May-2014.) (New usage is discouraged.) |
β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) β β’ ((π β CHilOLD β§ πΉ β (Cauβπ·)) β πΉ β dom (βπ‘βπ½)) | ||
Theorem | cnchl 29656 | The set of complex numbers is a complex Hilbert space. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
β’ π = β¨β¨ + , Β· β©, absβ© β β’ π β CHilOLD | ||
Theorem | htthlem 29657* | Lemma for htth 29658. The collection πΎ, which consists of functions πΉ(π§)(π€) = β¨π€ β£ π(π§)β© = β¨π(π€) β£ π§β© for each π§ in the unit ball, is a collection of bounded linear functions by ipblnfi 29595, so by the Uniform Boundedness theorem ubth 29613, there is a uniform bound π¦ on β₯ πΉ(π₯) β₯ for all π₯ in the unit ball. Then β£ π(π₯) β£ β2 = β¨π(π₯) β£ π(π₯)β© = πΉ(π₯)( π(π₯)) β€ π¦ β£ π(π₯) β£, so β£ π(π₯) β£ β€ π¦ and π is bounded. (Contributed by NM, 11-Jan-2008.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) & β’ πΏ = (π LnOp π) & β’ π΅ = (π BLnOp π) & β’ π = (normCVβπ) & β’ π β CHilOLD & β’ π = β¨β¨ + , Β· β©, absβ© & β’ (π β π β πΏ) & β’ (π β βπ₯ β π βπ¦ β π (π₯π(πβπ¦)) = ((πβπ₯)ππ¦)) & β’ πΉ = (π§ β π β¦ (π€ β π β¦ (π€π(πβπ§)))) & β’ πΎ = (πΉ β {π§ β π β£ (πβπ§) β€ 1}) β β’ (π β π β π΅) | ||
Theorem | htth 29658* | Hellinger-Toeplitz Theorem: any self-adjoint linear operator defined on all of Hilbert space is bounded. Theorem 10.1-1 of [Kreyszig] p. 525. Discovered by E. Hellinger and O. Toeplitz in 1910, "it aroused both admiration and puzzlement since the theorem establishes a relation between properties of two different kinds, namely, the properties of being defined everywhere and being bounded." (Contributed by NM, 11-Jan-2008.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) & β’ πΏ = (π LnOp π) & β’ π΅ = (π BLnOp π) β β’ ((π β CHilOLD β§ π β πΏ β§ βπ₯ β π βπ¦ β π (π₯π(πβπ¦)) = ((πβπ₯)ππ¦)) β π β π΅) | ||
This part contains the definitions and theorems used by the Hilbert Space Explorer (HSE), mmhil.html. Because it axiomatizes a single complex Hilbert space whose existence is assumed, its usefulness is limited. For example, it cannot work with real or quaternion Hilbert spaces and it cannot study relationships between two Hilbert spaces. More information can be found on the Hilbert Space Explorer page. Future development should instead work with general Hilbert spaces as defined by df-hil 21033; note that df-hil 21033 uses extensible structures. The intent is for this deprecated section to be deleted once all its theorems have been translated into extensible structure versions (or are not useful). Many of the theorems in this section have already been translated to extensible structure versions, but there is still a lot in this section that might be useful for future reference. It is much easier to translate these by hand from this section than to start from scratch from textbook proofs, since the HSE omits no details. | ||
Syntax | chba 29659 | Extend class notation with Hilbert vector space. |
class β | ||
Syntax | cva 29660 | Extend class notation with vector addition in Hilbert space. In the literature, the subscript "h" is omitted, but we need it to avoid ambiguity with complex number addition + caddc 10987. |
class +β | ||
Syntax | csm 29661 | Extend class notation with scalar multiplication in Hilbert space. In the literature scalar multiplication is usually indicated by juxtaposition, but we need an explicit symbol to prevent ambiguity. |
class Β·β | ||
Syntax | csp 29662 | Extend class notation with inner (scalar) product in Hilbert space. In the literature, the inner product of π΄ and π΅ is usually written β¨π΄, π΅β© but our operation notation allows to use existing theorems about operations and also eliminates ambiguity with the definition of an ordered pair df-op 4591. |
class Β·ih | ||
Syntax | cno 29663 | Extend class notation with the norm function in Hilbert space. In the literature, the norm of π΄ is usually written "|| π΄ ||", but we use function notation to take advantage of our existing theorems about functions. |
class normβ | ||
Syntax | c0v 29664 | Extend class notation with zero vector in Hilbert space. |
class 0β | ||
Syntax | cmv 29665 | Extend class notation with vector subtraction in Hilbert space. |
class ββ | ||
Syntax | ccauold 29666 | Extend class notation with set of Cauchy sequences in Hilbert space. |
class Cauchy | ||
Syntax | chli 29667 | Extend class notation with convergence relation in Hilbert space. |
class βπ£ | ||
Syntax | csh 29668 | Extend class notation with set of subspaces of a Hilbert space. |
class Sβ | ||
Syntax | cch 29669 | Extend class notation with set of closed subspaces of a Hilbert space. |
class Cβ | ||
Syntax | cort 29670 | Extend class notation with orthogonal complement in Cβ. |
class β₯ | ||
Syntax | cph 29671 | Extend class notation with subspace sum in Cβ. |
class +β | ||
Syntax | cspn 29672 | Extend class notation with subspace span in Cβ. |
class span | ||
Syntax | chj 29673 | Extend class notation with join in Cβ. |
class β¨β | ||
Syntax | chsup 29674 | Extend class notation with supremum of a collection in Cβ. |
class β¨β | ||
Syntax | c0h 29675 | Extend class notation with zero of Cβ. |
class 0β | ||
Syntax | ccm 29676 | Extend class notation with the commutes relation on a Hilbert lattice. |
class πΆβ | ||
Syntax | cpjh 29677 | Extend class notation with set of projections on a Hilbert space. |
class projβ | ||
Syntax | chos 29678 | Extend class notation with sum of Hilbert space operators. |
class +op | ||
Syntax | chot 29679 | Extend class notation with scalar product of a Hilbert space operator. |
class Β·op | ||
Syntax | chod 29680 | Extend class notation with difference of Hilbert space operators. |
class βop | ||
Syntax | chfs 29681 | Extend class notation with sum of Hilbert space functionals. |
class +fn | ||
Syntax | chft 29682 | Extend class notation with scalar product of Hilbert space functional. |
class Β·fn | ||
Syntax | ch0o 29683 | Extend class notation with the Hilbert space zero operator. |
class 0hop | ||
Syntax | chio 29684 | Extend class notation with Hilbert space identity operator. |
class Iop | ||
Syntax | cnop 29685 | Extend class notation with the operator norm function. |
class normop | ||
Syntax | ccop 29686 | Extend class notation with set of continuous Hilbert space operators. |
class ContOp | ||
Syntax | clo 29687 | Extend class notation with set of linear Hilbert space operators. |
class LinOp | ||
Syntax | cbo 29688 | Extend class notation with set of bounded linear operators. |
class BndLinOp | ||
Syntax | cuo 29689 | Extend class notation with set of unitary Hilbert space operators. |
class UniOp | ||
Syntax | cho 29690 | Extend class notation with set of Hermitian Hilbert space operators. |
class HrmOp | ||
Syntax | cnmf 29691 | Extend class notation with the functional norm function. |
class normfn | ||
Syntax | cnl 29692 | Extend class notation with the functional nullspace function. |
class null | ||
Syntax | ccnfn 29693 | Extend class notation with set of continuous Hilbert space functionals. |
class ContFn | ||
Syntax | clf 29694 | Extend class notation with set of linear Hilbert space functionals. |
class LinFn | ||
Syntax | cado 29695 | Extend class notation with Hilbert space adjoint function. |
class adjβ | ||
Syntax | cbr 29696 | Extend class notation with the bra of a vector in Dirac bra-ket notation. |
class bra | ||
Syntax | ck 29697 | Extend class notation with the outer product of two vectors in Dirac bra-ket notation. |
class ketbra | ||
Syntax | cleo 29698 | Extend class notation with positive operator ordering. |
class β€op | ||
Syntax | cei 29699 | Extend class notation with Hilbert space eigenvector function. |
class eigvec | ||
Syntax | cel 29700 | Extend class notation with Hilbert space eigenvalue function. |
class eigval |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |