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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ubth 29601* | 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 29602* | Lemma for minveco 29612. 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 29603* | Lemma for minveco 29612. 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 29604* | Lemma for minveco 29612. 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 29605* | Lemma for minveco 29612. πΉ 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 29606* | Lemma for minveco 29612. 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 29607* | Lemma for minveco 29612. 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 29608* | Lemma for minveco 29612. 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 29609* | Lemma for minveco 29612. Discharge the assumption about the sequence πΉ by applying countable choice ax-cc 10305. (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 29610* | Lemma for minveco 29612. 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 29611* | Lemma for minveco 29612. 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 29612* | 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 29613 | Extend class notation with the class of all complex Hilbert spaces. |
class CHilOLD | ||
Definition | df-hlo 29614 | 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 29615 | 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 29616 | Every complex Hilbert space is a complex Banach space. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
β’ (π β CHilOLD β π β CBan) | ||
Theorem | hlph 29617 | 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 29618 | The class of all complex Hilbert spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
β’ Rel CHilOLD | ||
Theorem | hlnv 29619 | Every complex Hilbert space is a normed complex vector space. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
β’ (π β CHilOLD β π β NrmCVec) | ||
Theorem | hlnvi 29620 | Every complex Hilbert space is a normed complex vector space. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.) |
β’ π β CHilOLD β β’ π β NrmCVec | ||
Theorem | hlvc 29621 | Every complex Hilbert space is a complex vector space. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (1st βπ) β β’ (π β CHilOLD β π β CVecOLD) | ||
Theorem | hlcmet 29622 | 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 29623 | The induced metric on a complex Hilbert space. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π· = (IndMetβπ) β β’ (π β CHilOLD β π· β (Metβπ)) | ||
Theorem | hlpar2 29624 | 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 29625 | 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 29626 | The base set of a Hilbert space is a set. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) β β’ π β V | ||
Theorem | hladdf 29627 | Mapping for Hilbert space vector addition. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) β β’ (π β CHilOLD β πΊ:(π Γ π)βΆπ) | ||
Theorem | hlcom 29628 | Hilbert space vector addition is commutative. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) β β’ ((π β CHilOLD β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) = (π΅πΊπ΄)) | ||
Theorem | hlass 29629 | Hilbert space vector addition is associative. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) β β’ ((π β CHilOLD β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)πΊπΆ) = (π΄πΊ(π΅πΊπΆ))) | ||
Theorem | hl0cl 29630 | The Hilbert space zero vector. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (0vecβπ) β β’ (π β CHilOLD β π β π) | ||
Theorem | hladdid 29631 | Hilbert space addition with the zero vector. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = (0vecβπ) β β’ ((π β CHilOLD β§ π΄ β π) β (π΄πΊπ) = π΄) | ||
Theorem | hlmulf 29632 | Mapping for Hilbert space scalar multiplication. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) β β’ (π β CHilOLD β π:(β Γ π)βΆπ) | ||
Theorem | hlmulid 29633 | Hilbert space scalar multiplication by one. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) β β’ ((π β CHilOLD β§ π΄ β π) β (1ππ΄) = π΄) | ||
Theorem | hlmulass 29634 | Hilbert space scalar multiplication associative law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) β β’ ((π β CHilOLD β§ (π΄ β β β§ π΅ β β β§ πΆ β π)) β ((π΄ Β· π΅)ππΆ) = (π΄π(π΅ππΆ))) | ||
Theorem | hldi 29635 | Hilbert space scalar multiplication distributive law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) β β’ ((π β CHilOLD β§ (π΄ β β β§ π΅ β π β§ πΆ β π)) β (π΄π(π΅πΊπΆ)) = ((π΄ππ΅)πΊ(π΄ππΆ))) | ||
Theorem | hldir 29636 | Hilbert space scalar multiplication distributive law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) β β’ ((π β CHilOLD β§ (π΄ β β β§ π΅ β β β§ πΆ β π)) β ((π΄ + π΅)ππΆ) = ((π΄ππΆ)πΊ(π΅ππΆ))) | ||
Theorem | hlmul0 29637 | Hilbert space scalar multiplication by zero. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) & β’ π = (0vecβπ) β β’ ((π β CHilOLD β§ π΄ β π) β (0ππ΄) = π) | ||
Theorem | hlipf 29638 | Mapping for Hilbert space inner product. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) β β’ (π β CHilOLD β π:(π Γ π)βΆβ) | ||
Theorem | hlipcj 29639 | Conjugate law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CHilOLD β§ π΄ β π β§ π΅ β π) β (π΄ππ΅) = (ββ(π΅ππ΄))) | ||
Theorem | hlipdir 29640 | Distributive law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CHilOLD β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)ππΆ) = ((π΄ππΆ) + (π΅ππΆ))) | ||
Theorem | hlipass 29641 | Associative law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CHilOLD β§ (π΄ β β β§ π΅ β π β§ πΆ β π)) β ((π΄ππ΅)ππΆ) = (π΄ Β· (π΅ππΆ))) | ||
Theorem | hlipgt0 29642 | 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 29643 | 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 29644 | 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 29645* | Lemma for htth 29646. The collection πΎ, which consists of functions πΉ(π§)(π€) = β¨π€ β£ π(π§)β© = β¨π(π€) β£ π§β© for each π§ in the unit ball, is a collection of bounded linear functions by ipblnfi 29583, so by the Uniform Boundedness theorem ubth 29601, 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 29646* | 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 29647 | Extend class notation with Hilbert vector space. |
class β | ||
Syntax | cva 29648 | 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 10988. |
class +β | ||
Syntax | csm 29649 | 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 29650 | 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 4592. |
class Β·ih | ||
Syntax | cno 29651 | 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 29652 | Extend class notation with zero vector in Hilbert space. |
class 0β | ||
Syntax | cmv 29653 | Extend class notation with vector subtraction in Hilbert space. |
class ββ | ||
Syntax | ccauold 29654 | Extend class notation with set of Cauchy sequences in Hilbert space. |
class Cauchy | ||
Syntax | chli 29655 | Extend class notation with convergence relation in Hilbert space. |
class βπ£ | ||
Syntax | csh 29656 | Extend class notation with set of subspaces of a Hilbert space. |
class Sβ | ||
Syntax | cch 29657 | Extend class notation with set of closed subspaces of a Hilbert space. |
class Cβ | ||
Syntax | cort 29658 | Extend class notation with orthogonal complement in Cβ. |
class β₯ | ||
Syntax | cph 29659 | Extend class notation with subspace sum in Cβ. |
class +β | ||
Syntax | cspn 29660 | Extend class notation with subspace span in Cβ. |
class span | ||
Syntax | chj 29661 | Extend class notation with join in Cβ. |
class β¨β | ||
Syntax | chsup 29662 | Extend class notation with supremum of a collection in Cβ. |
class β¨β | ||
Syntax | c0h 29663 | Extend class notation with zero of Cβ. |
class 0β | ||
Syntax | ccm 29664 | Extend class notation with the commutes relation on a Hilbert lattice. |
class πΆβ | ||
Syntax | cpjh 29665 | Extend class notation with set of projections on a Hilbert space. |
class projβ | ||
Syntax | chos 29666 | Extend class notation with sum of Hilbert space operators. |
class +op | ||
Syntax | chot 29667 | Extend class notation with scalar product of a Hilbert space operator. |
class Β·op | ||
Syntax | chod 29668 | Extend class notation with difference of Hilbert space operators. |
class βop | ||
Syntax | chfs 29669 | Extend class notation with sum of Hilbert space functionals. |
class +fn | ||
Syntax | chft 29670 | Extend class notation with scalar product of Hilbert space functional. |
class Β·fn | ||
Syntax | ch0o 29671 | Extend class notation with the Hilbert space zero operator. |
class 0hop | ||
Syntax | chio 29672 | Extend class notation with Hilbert space identity operator. |
class Iop | ||
Syntax | cnop 29673 | Extend class notation with the operator norm function. |
class normop | ||
Syntax | ccop 29674 | Extend class notation with set of continuous Hilbert space operators. |
class ContOp | ||
Syntax | clo 29675 | Extend class notation with set of linear Hilbert space operators. |
class LinOp | ||
Syntax | cbo 29676 | Extend class notation with set of bounded linear operators. |
class BndLinOp | ||
Syntax | cuo 29677 | Extend class notation with set of unitary Hilbert space operators. |
class UniOp | ||
Syntax | cho 29678 | Extend class notation with set of Hermitian Hilbert space operators. |
class HrmOp | ||
Syntax | cnmf 29679 | Extend class notation with the functional norm function. |
class normfn | ||
Syntax | cnl 29680 | Extend class notation with the functional nullspace function. |
class null | ||
Syntax | ccnfn 29681 | Extend class notation with set of continuous Hilbert space functionals. |
class ContFn | ||
Syntax | clf 29682 | Extend class notation with set of linear Hilbert space functionals. |
class LinFn | ||
Syntax | cado 29683 | Extend class notation with Hilbert space adjoint function. |
class adjβ | ||
Syntax | cbr 29684 | Extend class notation with the bra of a vector in Dirac bra-ket notation. |
class bra | ||
Syntax | ck 29685 | Extend class notation with the outer product of two vectors in Dirac bra-ket notation. |
class ketbra | ||
Syntax | cleo 29686 | Extend class notation with positive operator ordering. |
class β€op | ||
Syntax | cei 29687 | Extend class notation with Hilbert space eigenvector function. |
class eigvec | ||
Syntax | cel 29688 | Extend class notation with Hilbert space eigenvalue function. |
class eigval | ||
Syntax | cspc 29689 | Extend class notation with the spectrum of an operator. |
class Lambda | ||
Syntax | cst 29690 | Extend class notation with set of states on a Hilbert lattice. |
class States | ||
Syntax | chst 29691 | Extend class notation with set of Hilbert-space-valued states on a Hilbert lattice. |
class CHStates | ||
Syntax | ccv 29692 | Extend class notation with the covers relation on a Hilbert lattice. |
class ββ | ||
Syntax | cat 29693 | Extend class notation with set of atoms on a Hilbert lattice. |
class HAtoms | ||
Syntax | cmd 29694 | Extend class notation with the modular pair relation on a Hilbert lattice. |
class πβ | ||
Syntax | cdmd 29695 | Extend class notation with the dual modular pair relation on a Hilbert lattice. |
class πβ* | ||
Definition | df-hnorm 29696 | Define the function for the norm of a vector of Hilbert space. See normval 29852 for its value and normcl 29853 for its closure. Theorems norm-i-i 29861, norm-ii-i 29865, and norm-iii-i 29867 show it has the expected properties of a norm. In the literature, the norm of π΄ is usually written "|| π΄ ||", but we use function notation to take advantage of our existing theorems about functions. Definition of norm in [Beran] p. 96. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.) |
β’ normβ = (π₯ β dom dom Β·ih β¦ (ββ(π₯ Β·ih π₯))) | ||
Definition | df-hba 29697 | Define base set of Hilbert space, for use if we want to develop Hilbert space independently from the axioms (see comments in ax-hilex 29727). Note that β is considered a primitive in the Hilbert space axioms below, and we don't use this definition outside of this section. This definition can be proved independently from those axioms as Theorem hhba 29895. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ β = (BaseSetββ¨β¨ +β , Β·β β©, normββ©) | ||
Definition | df-h0v 29698 | Define the zero vector of Hilbert space. Note that 0vec is considered a primitive in the Hilbert space axioms below, and we don't use this definition outside of this section. It is proved from the axioms as Theorem hh0v 29896. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ 0β = (0vecββ¨β¨ +β , Β·β β©, normββ©) | ||
Definition | df-hvsub 29699* | Define vector subtraction. See hvsubvali 29748 for its value and hvsubcli 29749 for its closure. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.) |
β’ ββ = (π₯ β β, π¦ β β β¦ (π₯ +β (-1 Β·β π¦))) | ||
Definition | df-hlim 29700* | Define the limit relation for Hilbert space. See hlimi 29916 for its relational expression. Note that π:ββΆ β is an infinite sequence of vectors, i.e. a mapping from integers to vectors. Definition of converge in [Beran] p. 96. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.) |
β’ βπ£ = {β¨π, π€β© β£ ((π:ββΆ β β§ π€ β β) β§ βπ₯ β β+ βπ¦ β β βπ§ β (β€β₯βπ¦)(normββ((πβπ§) ββ π€)) < π₯)} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |