![]() |
Metamath
Proof Explorer Theorem List (p. 305 of 480) | < 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | minveco 30401* | 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 30402 | Extend class notation with the class of all complex Hilbert spaces. |
class CHilOLD | ||
Definition | df-hlo 30403 | 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 30404 | 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 30405 | Every complex Hilbert space is a complex Banach space. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
β’ (π β CHilOLD β π β CBan) | ||
Theorem | hlph 30406 | 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 30407 | The class of all complex Hilbert spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
β’ Rel CHilOLD | ||
Theorem | hlnv 30408 | Every complex Hilbert space is a normed complex vector space. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
β’ (π β CHilOLD β π β NrmCVec) | ||
Theorem | hlnvi 30409 | Every complex Hilbert space is a normed complex vector space. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.) |
β’ π β CHilOLD β β’ π β NrmCVec | ||
Theorem | hlvc 30410 | Every complex Hilbert space is a complex vector space. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (1st βπ) β β’ (π β CHilOLD β π β CVecOLD) | ||
Theorem | hlcmet 30411 | 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 30412 | The induced metric on a complex Hilbert space. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π· = (IndMetβπ) β β’ (π β CHilOLD β π· β (Metβπ)) | ||
Theorem | hlpar2 30413 | 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 30414 | 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 30415 | The base set of a Hilbert space is a set. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) β β’ π β V | ||
Theorem | hladdf 30416 | Mapping for Hilbert space vector addition. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) β β’ (π β CHilOLD β πΊ:(π Γ π)βΆπ) | ||
Theorem | hlcom 30417 | Hilbert space vector addition is commutative. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) β β’ ((π β CHilOLD β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) = (π΅πΊπ΄)) | ||
Theorem | hlass 30418 | Hilbert space vector addition is associative. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) β β’ ((π β CHilOLD β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)πΊπΆ) = (π΄πΊ(π΅πΊπΆ))) | ||
Theorem | hl0cl 30419 | The Hilbert space zero vector. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (0vecβπ) β β’ (π β CHilOLD β π β π) | ||
Theorem | hladdid 30420 | Hilbert space addition with the zero vector. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = (0vecβπ) β β’ ((π β CHilOLD β§ π΄ β π) β (π΄πΊπ) = π΄) | ||
Theorem | hlmulf 30421 | Mapping for Hilbert space scalar multiplication. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) β β’ (π β CHilOLD β π:(β Γ π)βΆπ) | ||
Theorem | hlmulid 30422 | Hilbert space scalar multiplication by one. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) β β’ ((π β CHilOLD β§ π΄ β π) β (1ππ΄) = π΄) | ||
Theorem | hlmulass 30423 | Hilbert space scalar multiplication associative law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) β β’ ((π β CHilOLD β§ (π΄ β β β§ π΅ β β β§ πΆ β π)) β ((π΄ Β· π΅)ππΆ) = (π΄π(π΅ππΆ))) | ||
Theorem | hldi 30424 | Hilbert space scalar multiplication distributive law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) β β’ ((π β CHilOLD β§ (π΄ β β β§ π΅ β π β§ πΆ β π)) β (π΄π(π΅πΊπΆ)) = ((π΄ππ΅)πΊ(π΄ππΆ))) | ||
Theorem | hldir 30425 | Hilbert space scalar multiplication distributive law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) β β’ ((π β CHilOLD β§ (π΄ β β β§ π΅ β β β§ πΆ β π)) β ((π΄ + π΅)ππΆ) = ((π΄ππΆ)πΊ(π΅ππΆ))) | ||
Theorem | hlmul0 30426 | Hilbert space scalar multiplication by zero. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) & β’ π = (0vecβπ) β β’ ((π β CHilOLD β§ π΄ β π) β (0ππ΄) = π) | ||
Theorem | hlipf 30427 | Mapping for Hilbert space inner product. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) β β’ (π β CHilOLD β π:(π Γ π)βΆβ) | ||
Theorem | hlipcj 30428 | Conjugate law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CHilOLD β§ π΄ β π β§ π΅ β π) β (π΄ππ΅) = (ββ(π΅ππ΄))) | ||
Theorem | hlipdir 30429 | Distributive law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CHilOLD β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)ππΆ) = ((π΄ππΆ) + (π΅ππΆ))) | ||
Theorem | hlipass 30430 | Associative law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CHilOLD β§ (π΄ β β β§ π΅ β π β§ πΆ β π)) β ((π΄ππ΅)ππΆ) = (π΄ Β· (π΅ππΆ))) | ||
Theorem | hlipgt0 30431 | 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 30432 | 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 30433 | 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 30434* | Lemma for htth 30435. The collection πΎ, which consists of functions πΉ(π§)(π€) = β¨π€ β£ π(π§)β© = β¨π(π€) β£ π§β© for each π§ in the unit ball, is a collection of bounded linear functions by ipblnfi 30372, so by the Uniform Boundedness theorem ubth 30390, 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 30435* | 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 21479; note that df-hil 21479 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 30436 | Extend class notation with Hilbert vector space. |
class β | ||
Syntax | cva 30437 | 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 11116. |
class +β | ||
Syntax | csm 30438 | 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 30439 | 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 4636. |
class Β·ih | ||
Syntax | cno 30440 | 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 30441 | Extend class notation with zero vector in Hilbert space. |
class 0β | ||
Syntax | cmv 30442 | Extend class notation with vector subtraction in Hilbert space. |
class ββ | ||
Syntax | ccauold 30443 | Extend class notation with set of Cauchy sequences in Hilbert space. |
class Cauchy | ||
Syntax | chli 30444 | Extend class notation with convergence relation in Hilbert space. |
class βπ£ | ||
Syntax | csh 30445 | Extend class notation with set of subspaces of a Hilbert space. |
class Sβ | ||
Syntax | cch 30446 | Extend class notation with set of closed subspaces of a Hilbert space. |
class Cβ | ||
Syntax | cort 30447 | Extend class notation with orthogonal complement in Cβ. |
class β₯ | ||
Syntax | cph 30448 | Extend class notation with subspace sum in Cβ. |
class +β | ||
Syntax | cspn 30449 | Extend class notation with subspace span in Cβ. |
class span | ||
Syntax | chj 30450 | Extend class notation with join in Cβ. |
class β¨β | ||
Syntax | chsup 30451 | Extend class notation with supremum of a collection in Cβ. |
class β¨β | ||
Syntax | c0h 30452 | Extend class notation with zero of Cβ. |
class 0β | ||
Syntax | ccm 30453 | Extend class notation with the commutes relation on a Hilbert lattice. |
class πΆβ | ||
Syntax | cpjh 30454 | Extend class notation with set of projections on a Hilbert space. |
class projβ | ||
Syntax | chos 30455 | Extend class notation with sum of Hilbert space operators. |
class +op | ||
Syntax | chot 30456 | Extend class notation with scalar product of a Hilbert space operator. |
class Β·op | ||
Syntax | chod 30457 | Extend class notation with difference of Hilbert space operators. |
class βop | ||
Syntax | chfs 30458 | Extend class notation with sum of Hilbert space functionals. |
class +fn | ||
Syntax | chft 30459 | Extend class notation with scalar product of Hilbert space functional. |
class Β·fn | ||
Syntax | ch0o 30460 | Extend class notation with the Hilbert space zero operator. |
class 0hop | ||
Syntax | chio 30461 | Extend class notation with Hilbert space identity operator. |
class Iop | ||
Syntax | cnop 30462 | Extend class notation with the operator norm function. |
class normop | ||
Syntax | ccop 30463 | Extend class notation with set of continuous Hilbert space operators. |
class ContOp | ||
Syntax | clo 30464 | Extend class notation with set of linear Hilbert space operators. |
class LinOp | ||
Syntax | cbo 30465 | Extend class notation with set of bounded linear operators. |
class BndLinOp | ||
Syntax | cuo 30466 | Extend class notation with set of unitary Hilbert space operators. |
class UniOp | ||
Syntax | cho 30467 | Extend class notation with set of Hermitian Hilbert space operators. |
class HrmOp | ||
Syntax | cnmf 30468 | Extend class notation with the functional norm function. |
class normfn | ||
Syntax | cnl 30469 | Extend class notation with the functional nullspace function. |
class null | ||
Syntax | ccnfn 30470 | Extend class notation with set of continuous Hilbert space functionals. |
class ContFn | ||
Syntax | clf 30471 | Extend class notation with set of linear Hilbert space functionals. |
class LinFn | ||
Syntax | cado 30472 | Extend class notation with Hilbert space adjoint function. |
class adjβ | ||
Syntax | cbr 30473 | Extend class notation with the bra of a vector in Dirac bra-ket notation. |
class bra | ||
Syntax | ck 30474 | Extend class notation with the outer product of two vectors in Dirac bra-ket notation. |
class ketbra | ||
Syntax | cleo 30475 | Extend class notation with positive operator ordering. |
class β€op | ||
Syntax | cei 30476 | Extend class notation with Hilbert space eigenvector function. |
class eigvec | ||
Syntax | cel 30477 | Extend class notation with Hilbert space eigenvalue function. |
class eigval | ||
Syntax | cspc 30478 | Extend class notation with the spectrum of an operator. |
class Lambda | ||
Syntax | cst 30479 | Extend class notation with set of states on a Hilbert lattice. |
class States | ||
Syntax | chst 30480 | Extend class notation with set of Hilbert-space-valued states on a Hilbert lattice. |
class CHStates | ||
Syntax | ccv 30481 | Extend class notation with the covers relation on a Hilbert lattice. |
class ββ | ||
Syntax | cat 30482 | Extend class notation with set of atoms on a Hilbert lattice. |
class HAtoms | ||
Syntax | cmd 30483 | Extend class notation with the modular pair relation on a Hilbert lattice. |
class πβ | ||
Syntax | cdmd 30484 | Extend class notation with the dual modular pair relation on a Hilbert lattice. |
class πβ* | ||
Definition | df-hnorm 30485 | Define the function for the norm of a vector of Hilbert space. See normval 30641 for its value and normcl 30642 for its closure. Theorems norm-i-i 30650, norm-ii-i 30654, and norm-iii-i 30656 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 30486 | Define base set of Hilbert space, for use if we want to develop Hilbert space independently from the axioms (see comments in ax-hilex 30516). 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 30684. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ β = (BaseSetββ¨β¨ +β , Β·β β©, normββ©) | ||
Definition | df-h0v 30487 | 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 30685. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ 0β = (0vecββ¨β¨ +β , Β·β β©, normββ©) | ||
Definition | df-hvsub 30488* | Define vector subtraction. See hvsubvali 30537 for its value and hvsubcli 30538 for its closure. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.) |
β’ ββ = (π₯ β β, π¦ β β β¦ (π₯ +β (-1 Β·β π¦))) | ||
Definition | df-hlim 30489* | Define the limit relation for Hilbert space. See hlimi 30705 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ββ((πβπ§) ββ π€)) < π₯)} | ||
Definition | df-hcau 30490* | Define the set of Cauchy sequences on a Hilbert space. See hcau 30701 for its membership relation. Note that π:ββΆ β is an infinite sequence of vectors, i.e. a mapping from integers to vectors. Definition of Cauchy sequence in [Beran] p. 96. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.) |
β’ Cauchy = {π β ( β βm β) β£ βπ₯ β β+ βπ¦ β β βπ§ β (β€β₯βπ¦)(normββ((πβπ¦) ββ (πβπ§))) < π₯} | ||
Theorem | h2hva 30491 | The group (addition) operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β NrmCVec β β’ +β = ( +π£ βπ) | ||
Theorem | h2hsm 30492 | The scalar product operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β NrmCVec β β’ Β·β = ( Β·π OLD βπ) | ||
Theorem | h2hnm 30493 | The norm function of Hilbert space. (Contributed by NM, 5-Jun-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β NrmCVec β β’ normβ = (normCVβπ) | ||
Theorem | h2hvs 30494 | The vector subtraction operation of Hilbert space. (Contributed by NM, 6-Jun-2008.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β NrmCVec & β’ β = (BaseSetβπ) β β’ ββ = ( βπ£ βπ) | ||
Theorem | h2hmetdval 30495 | Value of the distance function of the metric space of Hilbert space. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β NrmCVec & β’ β = (BaseSetβπ) & β’ π· = (IndMetβπ) β β’ ((π΄ β β β§ π΅ β β) β (π΄π·π΅) = (normββ(π΄ ββ π΅))) | ||
Theorem | h2hcau 30496 | The Cauchy sequences of Hilbert space. (Contributed by NM, 6-Jun-2008.) (Revised by Mario Carneiro, 13-May-2014.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β NrmCVec & β’ β = (BaseSetβπ) & β’ π· = (IndMetβπ) β β’ Cauchy = ((Cauβπ·) β© ( β βm β)) | ||
Theorem | h2hlm 30497 | The limit sequences of Hilbert space. (Contributed by NM, 6-Jun-2008.) (Revised by Mario Carneiro, 13-May-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β NrmCVec & β’ β = (BaseSetβπ) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) β β’ βπ£ = ((βπ‘βπ½) βΎ ( β βm β)) | ||
Before introducing the 18 axioms for Hilbert space, we first prove them as the conclusions of Theorems axhilex-zf 30498 through axhcompl-zf 30515, using ZFC set theory only. These show that if we are given a known, fixed Hilbert space π = β¨β¨ +β , Β·β β©, normββ© that satisfies their hypotheses, then we can derive the Hilbert space axioms as theorems of ZFC set theory. In practice, in order to use these theorems to convert the Hilbert Space explorer to a ZFC-only subtheory, we would also have to provide definitions for the 3 (otherwise primitive) class constants +β, Β·β, and Β·ih before df-hnorm 30485 above. See also the comment in ax-hilex 30516. | ||
Theorem | axhilex-zf 30498 | Derive Axiom ax-hilex 30516 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ β β V | ||
Theorem | axhfvadd-zf 30499 | Derive Axiom ax-hfvadd 30517 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ +β :( β Γ β)βΆ β | ||
Theorem | axhvcom-zf 30500 | Derive Axiom ax-hvcom 30518 from Hilbert space under ZF set theory. (Contributed by NM, 27-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β) β (π΄ +β π΅) = (π΅ +β π΄)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |