Home | Metamath
Proof Explorer Theorem List (p. 278 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dipassr 27701 | "Associative" law for second argument of inner product (compare dipass 27700). (Contributed by NM, 22-Nov-2007.) (New usage is discouraged.) |
Theorem | dipassr2 27702 | "Associative" law for inner product. Conjugate version of dipassr 27701. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.) |
Theorem | dipsubdir 27703 | Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
Theorem | dipsubdi 27704 | Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
Theorem | pythi 27705 | The Pythagorean theorem for an arbitrary complex inner product (pre-Hilbert) space . The square of the norm of the sum of two orthogonal vectors (i.e. whose inner product is 0) is the sum of the squares of their norms. Problem 2 in [Kreyszig] p. 135. This is Metamath 100 proof #4. (Contributed by NM, 17-Apr-2008.) (New usage is discouraged.) |
CV | ||
Theorem | siilem1 27706 | Lemma for sii 27709. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.) |
CV | ||
Theorem | siilem2 27707 | Lemma for sii 27709. (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.) |
CV | ||
Theorem | siii 27708 | Inference from sii 27709. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
CV | ||
Theorem | sii 27709 | Schwarz inequality. Part of Lemma 3-2.1(a) of [Kreyszig] p. 137. This is also called the Cauchy-Schwarz inequality by some authors and Bunjakovaskij-Cauchy-Schwarz inequality by others. See also theorems bcseqi 27977, bcsiALT 28036, bcsiHIL 28037, csbren 23182. This is Metamath 100 proof #78. (Contributed by NM, 12-Jan-2008.) (New usage is discouraged.) |
CV | ||
Theorem | sspph 27710 | A subspace of an inner product space is an inner product space. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.) |
Theorem | ipblnfi 27711* | A function generated by varying the first argument of an inner product (with its second argument a fixed vector ) is a bounded linear functional, i.e. a bounded linear operator from the vector space to . (Contributed by NM, 12-Jan-2008.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
Theorem | ip2eqi 27712* | Two vectors are equal iff their inner products with all other vectors are equal. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.) |
Theorem | phoeqi 27713* | A condition implying that two operators are equal. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
Theorem | ajmoi 27714* | Every operator has at most one adjoint. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
Theorem | ajfuni 27715 | The adjoint function is a function. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
Theorem | ajfun 27716 | The adjoint function is a function. This is not immediately apparent from df-aj 27605 but results from the uniqueness shown by ajmoi 27714. (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
Theorem | ajval 27717* | Value of the adjoint function. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
Syntax | ccbn 27718 | Extend class notation with the class of all complex Banach spaces. |
Definition | df-cbn 27719 | Define the class of all complex Banach spaces. (Contributed by NM, 5-Dec-2006.) (New usage is discouraged.) |
Theorem | iscbn 27720 | A complex Banach space is a normed complex vector space with a complete induced metric. (Contributed by NM, 5-Dec-2006.) (New usage is discouraged.) |
Theorem | cbncms 27721 | The induced metric on complex Banach space is complete. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
Theorem | bnnv 27722 | Every complex Banach space is a normed complex vector space. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
Theorem | bnrel 27723 | The class of all complex Banach spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
Theorem | bnsscmcl 27724 | 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.) |
Theorem | cnbn 27725 | The set of complex numbers is a complex Banach space. (Contributed by Steve Rodriguez, 4-Jan-2007.) (New usage is discouraged.) |
Theorem | ubthlem1 27726* | Lemma for ubth 27729. 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 23127, 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.) |
CV | ||
Theorem | ubthlem2 27727* | Lemma for ubth 27729. Given that there is a closed ball in , for any , we have and , so both of these have and so , which is our desired uniform bound. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.) |
CV | ||
Theorem | ubthlem3 27728* | Lemma for ubth 27729. Prove the reverse implication, using nmblolbi 27655. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.) |
CV | ||
Theorem | ubth 27729* | 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.) |
CV | ||
Theorem | minvecolem1 27730* | Lemma for minveco 27740. 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.) |
CV | ||
Theorem | minvecolem2 27731* | Lemma for minveco 27740. 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.) |
CV inf | ||
Theorem | minvecolem3 27732* | Lemma for minveco 27740. 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.) |
CV inf | ||
Theorem | minvecolem4a 27733* | Lemma for minveco 27740. is convergent in the subspace topology on . (Contributed by Mario Carneiro, 7-May-2014.) (New usage is discouraged.) |
CV inf | ||
Theorem | minvecolem4b 27734* | Lemma for minveco 27740. 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.) |
CV inf | ||
Theorem | minvecolem4c 27735* | Lemma for minveco 27740. 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.) |
CV inf | ||
Theorem | minvecolem4 27736* | Lemma for minveco 27740. 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.) |
CV inf | ||
Theorem | minvecolem5 27737* | Lemma for minveco 27740. Discharge the assumption about the sequence by applying countable choice ax-cc 9257. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.) |
CV inf | ||
Theorem | minvecolem6 27738* | Lemma for minveco 27740. 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.) |
CV inf | ||
Theorem | minvecolem7 27739* | Lemma for minveco 27740. 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.) |
CV inf | ||
Theorem | minveco 27740* | 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.) |
CV | ||
Syntax | chlo 27741 | Extend class notation with the class of all complex Hilbert spaces. |
Definition | df-hlo 27742 | 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.) |
Theorem | ishlo 27743 | 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.) |
Theorem | hlobn 27744 | Every complex Hilbert space is a complex Banach space. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
Theorem | hlph 27745 | 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.) |
Theorem | hlrel 27746 | The class of all complex Hilbert spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
Theorem | hlnv 27747 | Every complex Hilbert space is a normed complex vector space. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
Theorem | hlnvi 27748 | Every complex Hilbert space is a normed complex vector space. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.) |
Theorem | hlvc 27749 | Every complex Hilbert space is a complex vector space. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
Theorem | hlcmet 27750 | The induced metric on a complex Hilbert space is complete. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
Theorem | hlmet 27751 | The induced metric on a complex Hilbert space. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
Theorem | hlpar2 27752 | The parallelogram law satified by Hilbert space vectors. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
CV | ||
Theorem | hlpar 27753 | The parallelogram law satified by Hilbert space vectors. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
CV | ||
Theorem | hlex 27754 | The base set of a Hilbert space is a set. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
Theorem | hladdf 27755 | Mapping for Hilbert space vector addition. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
Theorem | hlcom 27756 | Hilbert space vector addition is commutative. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
Theorem | hlass 27757 | Hilbert space vector addition is associative. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
Theorem | hl0cl 27758 | The Hilbert space zero vector. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
Theorem | hladdid 27759 | Hilbert space addition with the zero vector. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
Theorem | hlmulf 27760 | Mapping for Hilbert space scalar multiplication. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
Theorem | hlmulid 27761 | Hilbert space scalar multiplication by one. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
Theorem | hlmulass 27762 | Hilbert space scalar multiplication associative law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
Theorem | hldi 27763 | Hilbert space scalar multiplication distributive law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
Theorem | hldir 27764 | Hilbert space scalar multiplication distributive law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
Theorem | hlmul0 27765 | Hilbert space scalar multiplication by zero. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
Theorem | hlipf 27766 | Mapping for Hilbert space inner product. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.) |
Theorem | hlipcj 27767 | Conjugate law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
Theorem | hlipdir 27768 | Distributive law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
Theorem | hlipass 27769 | Associative law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
Theorem | hlipgt0 27770 | The inner product of a Hilbert space vector by itself is positive. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
Theorem | hlcompl 27771 | Completeness of a Hilbert space. (Contributed by NM, 8-Sep-2007.) (Revised by Mario Carneiro, 9-May-2014.) (New usage is discouraged.) |
Theorem | cnchl 27772 | The set of complex numbers is a complex Hilbert space. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
Theorem | ssphl 27773 | A Banach subspace of an inner product space is a Hilbert space. (Contributed by NM, 11-Apr-2008.) (New usage is discouraged.) |
Theorem | htthlem 27774* | Lemma for htth 27775. The collection , which consists of functions for each in the unit ball, is a collection of bounded linear functions by ipblnfi 27711, so by the Uniform Boundedness theorem ubth 27729, there is a uniform bound on for all in the unit ball. Then , so and is bounded. (Contributed by NM, 11-Jan-2008.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
CV | ||
Theorem | htth 27775* | 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.) |
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 20048; note that df-hil 20048 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 | chil 27776 | Extend class notation with Hilbert vector space. |
Syntax | cva 27777 | Extend class notation with vector addition in Hilbert space. In the literature, the subscript "v" is omitted, but we need it to avoid ambiguity with complex number addition caddc 9939. |
Syntax | csm 27778 | 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. |
Syntax | csp 27779 | 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 us to use existing theorems about operations and also eliminates ambiguity with the definition of an ordered pair df-op 4184. |
Syntax | cno 27780 | 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. |
Syntax | c0v 27781 | Extend class notation with zero vector in Hilbert space. |
Syntax | cmv 27782 | Extend class notation with vector subtraction in Hilbert space. |
Syntax | ccau 27783 | Extend class notation with set of Cauchy sequences in Hilbert space. |
Syntax | chli 27784 | Extend class notation with convergence relation in Hilbert space. |
Syntax | csh 27785 | Extend class notation with set of subspaces of a Hilbert space. |
Syntax | cch 27786 | Extend class notation with set of closed subspaces of a Hilbert space. |
Syntax | cort 27787 | Extend class notation with orthogonal complement in . |
Syntax | cph 27788 | Extend class notation with subspace sum in . |
Syntax | cspn 27789 | Extend class notation with subspace span in . |
Syntax | chj 27790 | Extend class notation with join in . |
Syntax | chsup 27791 | Extend class notation with supremum of a collection in . |
Syntax | c0h 27792 | Extend class notation with zero of . |
Syntax | ccm 27793 | Extend class notation with the commutes relation on a Hilbert lattice. |
Syntax | cpjh 27794 | Extend class notation with set of projections on a Hilbert space. |
Syntax | chos 27795 | Extend class notation with sum of Hilbert space operators. |
Syntax | chot 27796 | Extend class notation with scalar product of a Hilbert space operator. |
Syntax | chod 27797 | Extend class notation with difference of Hilbert space operators. |
Syntax | chfs 27798 | Extend class notation with sum of Hilbert space functionals. |
Syntax | chft 27799 | Extend class notation with scalar product of Hilbert space functional. |
Syntax | ch0o 27800 | Extend class notation with the Hilbert space zero operator. |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |