HomeTheorem List (p. 319 of 500)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 319 of 500) | < 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-30900) |
Hilbert Space Explorer
(30901-32423) |
Users' Mathboxes
(32424-49930) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | ho2times 31801 | Two times a Hilbert space operator. (Contributed by NM, 26-Aug-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (2 ·op 𝑇) = (𝑇 +op 𝑇)) | ||
| Theorem | hoaddsubassi 31802 | Associativity of sum and difference of Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 +op 𝑆) −op 𝑇) = (𝑅 +op (𝑆 −op 𝑇)) | ||
| Theorem | hoaddsubi 31803 | Law for sum and difference of Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 +op 𝑆) −op 𝑇) = ((𝑅 −op 𝑇) +op 𝑆) | ||
| Theorem | hosd1i 31804 | Hilbert space operator sum expressed in terms of difference. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ & ⊢ 𝑈: ℋ⟶ ℋ ⇒ ⊢ (𝑇 +op 𝑈) = (𝑇 −op ( 0hop −op 𝑈)) | ||
| Theorem | hosd2i 31805 | Hilbert space operator sum expressed in terms of difference. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ & ⊢ 𝑈: ℋ⟶ ℋ ⇒ ⊢ (𝑇 +op 𝑈) = (𝑇 −op ((𝑈 −op 𝑈) −op 𝑈)) | ||
| Theorem | hopncani 31806 | Hilbert space operator cancellation law. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ & ⊢ 𝑈: ℋ⟶ ℋ ⇒ ⊢ ((𝑇 +op 𝑈) −op 𝑈) = 𝑇 | ||
| Theorem | honpcani 31807 | Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ & ⊢ 𝑈: ℋ⟶ ℋ ⇒ ⊢ ((𝑇 −op 𝑈) +op 𝑈) = 𝑇 | ||
| Theorem | hosubeq0i 31808 | If the difference between two operators is zero, they are equal. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ & ⊢ 𝑈: ℋ⟶ ℋ ⇒ ⊢ ((𝑇 −op 𝑈) = 0hop ↔ 𝑇 = 𝑈) | ||
| Theorem | honpncani 31809 | Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 −op 𝑆) +op (𝑆 −op 𝑇)) = (𝑅 −op 𝑇) | ||
| Theorem | ho01i 31810* | A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S8) of [Beran] p. 95. (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = 0 ↔ 𝑇 = 0hop ) | ||
| Theorem | ho02i 31811* | A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S10) of [Beran] p. 95. (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = 0 ↔ 𝑇 = 0hop ) | ||
| Theorem | hoeq1 31812* | A condition implying that two Hilbert space operators are equal. Lemma 3.2(S9) of [Beran] p. 95. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑆‘𝑥) ·ih 𝑦) = ((𝑇‘𝑥) ·ih 𝑦) ↔ 𝑆 = 𝑇)) | ||
| Theorem | hoeq2 31813* | A condition implying that two Hilbert space operators are equal. Lemma 3.2(S11) of [Beran] p. 95. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑆‘𝑦)) = (𝑥 ·ih (𝑇‘𝑦)) ↔ 𝑆 = 𝑇)) | ||
| Theorem | adjmo 31814* | Every Hilbert space operator has at most one adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
| ⊢ ∃*𝑢(𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦)) | ||
| Theorem | adjsym 31815* | Symmetry property of an adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦))) | ||
| Theorem | eigrei 31816 | A necessary and sufficient condition (that holds when 𝑇 is a Hermitian operator) for an eigenvalue 𝐵 to be real. Generalization of Equation 1.30 of [Hughes] p. 49. (Contributed by NM, 21-Jan-2005.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ) → ((𝐴 ·ih (𝑇‘𝐴)) = ((𝑇‘𝐴) ·ih 𝐴) ↔ 𝐵 ∈ ℝ)) | ||
| Theorem | eigre 31817 | A necessary and sufficient condition (that holds when 𝑇 is a Hermitian operator) for an eigenvalue 𝐵 to be real. Generalization of Equation 1.30 of [Hughes] p. 49. (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → ((𝐴 ·ih (𝑇‘𝐴)) = ((𝑇‘𝐴) ·ih 𝐴) ↔ 𝐵 ∈ ℝ)) | ||
| Theorem | eigposi 31818 | A sufficient condition (first conjunct pair, that holds when 𝑇 is a positive operator) for an eigenvalue 𝐵 (second conjunct pair) to be nonnegative. Remark (ii) in [Hughes] p. 137. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((((𝐴 ·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴 ·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) | ||
| Theorem | eigorthi 31819 | A necessary and sufficient condition (that holds when 𝑇 is a Hermitian operator) for two eigenvectors 𝐴 and 𝐵 to be orthogonal. Generalization of Equation 1.31 of [Hughes] p. 49. (Contributed by NM, 23-Jan-2005.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈ ℂ ⇒ ⊢ ((((𝑇‘𝐴) = (𝐶 ·ℎ 𝐴) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ∧ 𝐶 ≠ (∗‘𝐷)) → ((𝐴 ·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵) ↔ (𝐴 ·ih 𝐵) = 0)) | ||
| Theorem | eigorth 31820 | A necessary and sufficient condition (that holds when 𝑇 is a Hermitian operator) for two eigenvectors 𝐴 and 𝐵 to be orthogonal. Generalization of Equation 1.31 of [Hughes] p. 49. (Contributed by NM, 23-Mar-2006.) (New usage is discouraged.) |
| ⊢ ((((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) ∧ (((𝑇‘𝐴) = (𝐶 ·ℎ 𝐴) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ∧ 𝐶 ≠ (∗‘𝐷))) → ((𝐴 ·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵) ↔ (𝐴 ·ih 𝐵) = 0)) | ||
| Definition | df-nmop 31821* | Define the norm of a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
| ⊢ normop = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑡‘𝑧)))}, ℝ*, < )) | ||
| Definition | df-cnop 31822* | Define the set of continuous operators on Hilbert space. For every "epsilon" (𝑦) there is a "delta" (𝑧) such that... (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.) |
| ⊢ ContOp = {𝑡 ∈ ( ℋ ↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦)} | ||
| Definition | df-lnop 31823* | Define the set of linear operators on Hilbert space. (See df-hosum 31712 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
| ⊢ LinOp = {𝑡 ∈ ( ℋ ↑m ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑡‘𝑦)) +ℎ (𝑡‘𝑧))} | ||
| Definition | df-bdop 31824 | Define the set of bounded linear Hilbert space operators. (See df-hosum 31712 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
| ⊢ BndLinOp = {𝑡 ∈ LinOp ∣ (normop‘𝑡) < +∞} | ||
| Definition | df-unop 31825* | Define the set of unitary operators on Hilbert space. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
| ⊢ UniOp = {𝑡 ∣ (𝑡: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡‘𝑥) ·ih (𝑡‘𝑦)) = (𝑥 ·ih 𝑦))} | ||
| Definition | df-hmop 31826* | Define the set of Hermitian operators on Hilbert space. Some books call these "symmetric operators" and others call them "self-adjoint operators", sometimes with slightly different technical meanings. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
| ⊢ HrmOp = {𝑡 ∈ ( ℋ ↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦)} | ||
| Definition | df-nmfn 31827* | Define the norm of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
| ⊢ normfn = (𝑡 ∈ (ℂ ↑m ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (abs‘(𝑡‘𝑧)))}, ℝ*, < )) | ||
| Definition | df-nlfn 31828 | Define the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
| ⊢ null = (𝑡 ∈ (ℂ ↑m ℋ) ↦ (◡𝑡 “ {0})) | ||
| Definition | df-cnfn 31829* | Define the set of continuous functionals on Hilbert space. For every "epsilon" (𝑦) there is a "delta" (𝑧) such that... (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
| ⊢ ContFn = {𝑡 ∈ (ℂ ↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (abs‘((𝑡‘𝑤) − (𝑡‘𝑥))) < 𝑦)} | ||
| Definition | df-lnfn 31830* | Define the set of linear functionals on Hilbert space. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
| ⊢ LinFn = {𝑡 ∈ (ℂ ↑m ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))} | ||
| Definition | df-adjh 31831* | Define the adjoint of a Hilbert space operator (if it exists). The domain of adjℎ is the set of all adjoint operators. Definition of adjoint in [Kalmbach2] p. 8. Unlike Kalmbach (and most authors), we do not demand that the operator be linear, but instead show (in adjbdln 32065) that the adjoint exists for a bounded linear operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
| ⊢ adjℎ = {⟨𝑡, 𝑢⟩ ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢‘𝑦)))} | ||
| Definition | df-bra 31832* |
Define the bra of a vector used by Dirac notation. Based on definition
of bra in [Prugovecki] p. 186 (p.
180 in 1971 edition). In Dirac
bra-ket notation, ⟨𝐴 ∣ 𝐵⟩ is a complex number equal to
the inner
product (𝐵 ·ih 𝐴). But physicists like
to talk about the
individual components ⟨𝐴 ∣ and ∣
𝐵⟩, called bra
and ket
respectively. In order for their properties to make sense formally, we
define the ket ∣ 𝐵⟩ as the vector 𝐵 itself,
and the bra
⟨𝐴 ∣ as a functional from ℋ to ℂ. We represent the
Dirac notation ⟨𝐴 ∣ 𝐵⟩ by ((bra‘𝐴)‘𝐵); see
braval 31926. The reversal of the inner product
arguments not only makes
the bra-ket behavior consistent with physics literature (see comments
under ax-his3 31066) but is also required in order for the
associative law
kbass2 32099 to work.
Our definition of bra and the associated outer product df-kb 31833 differs from, but is equivalent to, a common approach in the literature that makes use of mappings to a dual space. Our approach eliminates the need to have a parallel development of this dual space and instead keeps everything in Hilbert space. For an extensive discussion about how our notation maps to the bra-ket notation in physics textbooks, see mmnotes.txt 31833, under the 17-May-2006 entry. (Contributed by NM, 15-May-2006.) (New usage is discouraged.) |
| ⊢ bra = (𝑥 ∈ ℋ ↦ (𝑦 ∈ ℋ ↦ (𝑦 ·ih 𝑥))) | ||
| Definition | df-kb 31833* | Define a commuted bra and ket juxtaposition used by Dirac notation. In Dirac notation, ∣ 𝐴⟩⟨𝐵 ∣ is an operator known as the outer product of 𝐴 and 𝐵, which we represent by (𝐴 ketbra 𝐵). Based on Equation 8.1 of [Prugovecki] p. 376. This definition, combined with Definition df-bra 31832, allows any legal juxtaposition of bras and kets to make sense formally and also to obey the associative law when mapped back to Dirac notation. (Contributed by NM, 15-May-2006.) (New usage is discouraged.) |
| ⊢ ketbra = (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑧 ∈ ℋ ↦ ((𝑧 ·ih 𝑦) ·ℎ 𝑥))) | ||
| Definition | df-leop 31834* | Define positive operator ordering. Definition VI.1 of [Retherford] p. 49. Note that ( ℋ × 0ℋ) ≤op 𝑇 means that 𝑇 is a positive operator. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
| ⊢ ≤op = {⟨𝑡, 𝑢⟩ ∣ ((𝑢 −op 𝑡) ∈ HrmOp ∧ ∀𝑥 ∈ ℋ 0 ≤ (((𝑢 −op 𝑡)‘𝑥) ·ih 𝑥))} | ||
| Definition | df-eigvec 31835* | Define the eigenvector function. Theorem eleigveccl 31941 shows that eigvec‘𝑇, the set of eigenvectors of Hilbert space operator 𝑇, are Hilbert space vectors. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
| ⊢ eigvec = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ( ℋ ∖ 0ℋ) ∣ ∃𝑧 ∈ ℂ (𝑡‘𝑥) = (𝑧 ·ℎ 𝑥)}) | ||
| Definition | df-eigval 31836* | Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 31943 shows that (eigval‘𝑇)‘𝐴, the eigenvalue associated with eigenvector 𝐴, is a complex number. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
| ⊢ eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))) | ||
| Definition | df-spec 31837* | Define the spectrum of an operator. Definition of spectrum in [Halmos] p. 50. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.) |
| ⊢ Lambda = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ℂ ∣ ¬ (𝑡 −op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ}) | ||
| Theorem | nmopval 31838* | Value of the norm of a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (normop‘𝑇) = sup({𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}, ℝ*, < )) | ||
| Theorem | elcnop 31839* | Property defining a continuous Hilbert space operator. (Contributed by NM, 28-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ ContOp ↔ (𝑇: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (normℎ‘((𝑇‘𝑤) −ℎ (𝑇‘𝑥))) < 𝑦))) | ||
| Theorem | ellnop 31840* | Property defining a linear Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ LinOp ↔ (𝑇: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑇‘𝑦)) +ℎ (𝑇‘𝑧)))) | ||
| Theorem | lnopf 31841 | A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ LinOp → 𝑇: ℋ⟶ ℋ) | ||
| Theorem | elbdop 31842 | Property defining a bounded linear Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ BndLinOp ↔ (𝑇 ∈ LinOp ∧ (normop‘𝑇) < +∞)) | ||
| Theorem | bdopln 31843 | A bounded linear Hilbert space operator is a linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ BndLinOp → 𝑇 ∈ LinOp) | ||
| Theorem | bdopf 31844 | A bounded linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ BndLinOp → 𝑇: ℋ⟶ ℋ) | ||
| Theorem | nmopsetretALT 31845* | The set in the supremum of the operator norm definition df-nmop 31821 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆ ℝ) | ||
| Theorem | nmopsetretHIL 31846* | The set in the supremum of the operator norm definition df-nmop 31821 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆ ℝ) | ||
| Theorem | nmopsetn0 31847* | The set in the supremum of the operator norm definition df-nmop 31821 is nonempty. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
| ⊢ (normℎ‘(𝑇‘0ℎ)) ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} | ||
| Theorem | nmopxr 31848 | The norm of a Hilbert space operator is an extended real. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (normop‘𝑇) ∈ ℝ*) | ||
| Theorem | nmoprepnf 31849 | The norm of a Hilbert space operator is either real or plus infinity. (Contributed by NM, 5-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → ((normop‘𝑇) ∈ ℝ ↔ (normop‘𝑇) ≠ +∞)) | ||
| Theorem | nmopgtmnf 31850 | The norm of a Hilbert space operator is not minus infinity. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → -∞ < (normop‘𝑇)) | ||
| Theorem | nmopreltpnf 31851 | The norm of a Hilbert space operator is real iff it is less than infinity. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → ((normop‘𝑇) ∈ ℝ ↔ (normop‘𝑇) < +∞)) | ||
| Theorem | nmopre 31852 | The norm of a bounded operator is a real number. (Contributed by NM, 29-Jan-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ BndLinOp → (normop‘𝑇) ∈ ℝ) | ||
| Theorem | elbdop2 31853 | Property defining a bounded linear Hilbert space operator. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ BndLinOp ↔ (𝑇 ∈ LinOp ∧ (normop‘𝑇) ∈ ℝ)) | ||
| Theorem | elunop 31854* | Property defining a unitary Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ UniOp ↔ (𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih (𝑇‘𝑦)) = (𝑥 ·ih 𝑦))) | ||
| Theorem | elhmop 31855* | Property defining a Hermitian Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ HrmOp ↔ (𝑇: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦))) | ||
| Theorem | hmopf 31856 | A Hermitian operator is a Hilbert space operator (mapping). (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ HrmOp → 𝑇: ℋ⟶ ℋ) | ||
| Theorem | hmopex 31857 | The class of Hermitian operators is a set. (Contributed by NM, 17-Aug-2006.) (New usage is discouraged.) |
| ⊢ HrmOp ∈ V | ||
| Theorem | nmfnval 31858* | Value of the norm of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ℂ → (normfn‘𝑇) = sup({𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘(𝑇‘𝑦)))}, ℝ*, < )) | ||
| Theorem | nmfnsetre 31859* | The set in the supremum of the functional norm definition df-nmfn 31827 is a set of reals. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ℂ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘(𝑇‘𝑦)))} ⊆ ℝ) | ||
| Theorem | nmfnsetn0 31860* | The set in the supremum of the functional norm definition df-nmfn 31827 is nonempty. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
| ⊢ (abs‘(𝑇‘0ℎ)) ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘(𝑇‘𝑦)))} | ||
| Theorem | nmfnxr 31861 | The norm of any Hilbert space functional is an extended real. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ℂ → (normfn‘𝑇) ∈ ℝ*) | ||
| Theorem | nmfnrepnf 31862 | The norm of a Hilbert space functional is either real or plus infinity. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ℂ → ((normfn‘𝑇) ∈ ℝ ↔ (normfn‘𝑇) ≠ +∞)) | ||
| Theorem | nlfnval 31863 | Value of the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ℂ → (null‘𝑇) = (◡𝑇 “ {0})) | ||
| Theorem | elcnfn 31864* | Property defining a continuous functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ ContFn ↔ (𝑇: ℋ⟶ℂ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (abs‘((𝑇‘𝑤) − (𝑇‘𝑥))) < 𝑦))) | ||
| Theorem | ellnfn 31865* | Property defining a linear functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ LinFn ↔ (𝑇: ℋ⟶ℂ ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑇‘𝑦)) + (𝑇‘𝑧)))) | ||
| Theorem | lnfnf 31866 | A linear Hilbert space functional is a functional. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ LinFn → 𝑇: ℋ⟶ℂ) | ||
| Theorem | dfadj2 31867* | Alternate definition of the adjoint of a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
| ⊢ adjℎ = {⟨𝑡, 𝑢⟩ ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))} | ||
| Theorem | funadj 31868 | Functionality of the adjoint function. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
| ⊢ Fun adjℎ | ||
| Theorem | dmadjss 31869 | The domain of the adjoint function is a subset of the maps from ℋ to ℋ. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
| ⊢ dom adjℎ ⊆ ( ℋ ↑m ℋ) | ||
| Theorem | dmadjop 31870 | A member of the domain of the adjoint function is a Hilbert space operator. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ dom adjℎ → 𝑇: ℋ⟶ ℋ) | ||
| Theorem | adjeu 31871* | Elementhood in the domain of the adjoint function. (Contributed by Mario Carneiro, 11-Sep-2015.) (Revised by Mario Carneiro, 24-Dec-2016.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (𝑇 ∈ dom adjℎ ↔ ∃!𝑢 ∈ ( ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))) | ||
| Theorem | adjval 31872* | Value of the adjoint function for 𝑇 in the domain of adjℎ. (Contributed by NM, 19-Feb-2006.) (Revised by Mario Carneiro, 24-Dec-2016.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ dom adjℎ → (adjℎ‘𝑇) = (℩𝑢 ∈ ( ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))) | ||
| Theorem | adjval2 31873* | Value of the adjoint function. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ dom adjℎ → (adjℎ‘𝑇) = (℩𝑢 ∈ ( ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢‘𝑦)))) | ||
| Theorem | cnvadj 31874 | The adjoint function equals its converse. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
| ⊢ ◡adjℎ = adjℎ | ||
| Theorem | funcnvadj 31875 | The converse of the adjoint function is a function. (Contributed by NM, 25-Jan-2006.) (New usage is discouraged.) |
| ⊢ Fun ◡adjℎ | ||
| Theorem | adj1o 31876 | The adjoint function maps one-to-one onto its domain. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
| ⊢ adjℎ:dom adjℎ–1-1-onto→dom adjℎ | ||
| Theorem | dmadjrn 31877 | The adjoint of an operator belongs to the adjoint function's domain. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ dom adjℎ → (adjℎ‘𝑇) ∈ dom adjℎ) | ||
| Theorem | eigvecval 31878* | The set of eigenvectors of a Hilbert space operator. (Contributed by NM, 11-Mar-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (eigvec‘𝑇) = {𝑥 ∈ ( ℋ ∖ 0ℋ) ∣ ∃𝑦 ∈ ℂ (𝑇‘𝑥) = (𝑦 ·ℎ 𝑥)}) | ||
| Theorem | eigvalfval 31879* | The eigenvalues of eigenvectors of a Hilbert space operator. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (eigval‘𝑇) = (𝑥 ∈ (eigvec‘𝑇) ↦ (((𝑇‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))) | ||
| Theorem | specval 31880* | The value of the spectrum of an operator. (Contributed by NM, 11-Apr-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (Lambda‘𝑇) = {𝑥 ∈ ℂ ∣ ¬ (𝑇 −op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ}) | ||
| Theorem | speccl 31881 | The spectrum of an operator is a set of complex numbers. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (Lambda‘𝑇) ⊆ ℂ) | ||
| Theorem | hhlnoi 31882 | The linear operators of Hilbert space. (Contributed by NM, 19-Nov-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝐿 = (𝑈 LnOp 𝑈) ⇒ ⊢ LinOp = 𝐿 | ||
| Theorem | hhnmoi 31883 | The norm of an operator in Hilbert space. (Contributed by NM, 19-Nov-2007.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑁 = (𝑈 normOpOLD 𝑈) ⇒ ⊢ normop = 𝑁 | ||
| Theorem | hhbloi 31884 | A bounded linear operator in Hilbert space. (Contributed by NM, 19-Nov-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝐵 = (𝑈 BLnOp 𝑈) ⇒ ⊢ BndLinOp = 𝐵 | ||
| Theorem | hh0oi 31885 | The zero operator in Hilbert space. (Contributed by NM, 7-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑍 = (𝑈 0op 𝑈) ⇒ ⊢ 0hop = 𝑍 | ||
| Theorem | hhcno 31886 | The continuous operators of Hilbert space. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
| ⊢ 𝐷 = (normℎ ∘ −ℎ ) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ContOp = (𝐽 Cn 𝐽) | ||
| Theorem | hhcnf 31887 | The continuous functionals of Hilbert space. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
| ⊢ 𝐷 = (normℎ ∘ −ℎ ) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ ContFn = (𝐽 Cn 𝐾) | ||
| Theorem | dmadjrnb 31888 | The adjoint of an operator belongs to the adjoint function's domain. (Note: the converse is dependent on our definition of function value, since it uses ndmfv 6860.) (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ dom adjℎ ↔ (adjℎ‘𝑇) ∈ dom adjℎ) | ||
| Theorem | nmoplb 31889 | A lower bound for an operator norm. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ ℋ ∧ (normℎ‘𝐴) ≤ 1) → (normℎ‘(𝑇‘𝐴)) ≤ (normop‘𝑇)) | ||
| Theorem | nmopub 31890* | An upper bound for an operator norm. (Contributed by NM, 7-Mar-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ ℝ*) → ((normop‘𝑇) ≤ 𝐴 ↔ ∀𝑥 ∈ ℋ ((normℎ‘𝑥) ≤ 1 → (normℎ‘(𝑇‘𝑥)) ≤ 𝐴))) | ||
| Theorem | nmopub2tALT 31891* | An upper bound for an operator norm. (Contributed by NM, 12-Apr-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ ∀𝑥 ∈ ℋ (normℎ‘(𝑇‘𝑥)) ≤ (𝐴 · (normℎ‘𝑥))) → (normop‘𝑇) ≤ 𝐴) | ||
| Theorem | nmopub2tHIL 31892* | An upper bound for an operator norm. (Contributed by NM, 13-Dec-2007.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ ∀𝑥 ∈ ℋ (normℎ‘(𝑇‘𝑥)) ≤ (𝐴 · (normℎ‘𝑥))) → (normop‘𝑇) ≤ 𝐴) | ||
| Theorem | nmopge0 31893 | The norm of any Hilbert space operator is nonnegative. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → 0 ≤ (normop‘𝑇)) | ||
| Theorem | nmopgt0 31894 | A linear Hilbert space operator that is not identically zero has a positive norm. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → ((normop‘𝑇) ≠ 0 ↔ 0 < (normop‘𝑇))) | ||
| Theorem | cnopc 31895* | Basic continuity property of a continuous Hilbert space operator. (Contributed by NM, 2-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ ContOp ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℝ+) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ ℋ ((normℎ‘(𝑦 −ℎ 𝐴)) < 𝑥 → (normℎ‘((𝑇‘𝑦) −ℎ (𝑇‘𝐴))) < 𝐵)) | ||
| Theorem | lnopl 31896 | Basic linearity property of a linear Hilbert space operator. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
| ⊢ (((𝑇 ∈ LinOp ∧ 𝐴 ∈ ℂ) ∧ (𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)) → (𝑇‘((𝐴 ·ℎ 𝐵) +ℎ 𝐶)) = ((𝐴 ·ℎ (𝑇‘𝐵)) +ℎ (𝑇‘𝐶))) | ||
| Theorem | unop 31897 | Basic inner product property of a unitary operator. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ UniOp ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝑇‘𝐴) ·ih (𝑇‘𝐵)) = (𝐴 ·ih 𝐵)) | ||
| Theorem | unopf1o 31898 | A unitary operator in Hilbert space is one-to-one and onto. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ UniOp → 𝑇: ℋ–1-1-onto→ ℋ) | ||
| Theorem | unopnorm 31899 | A unitary operator is idempotent in the norm. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ UniOp ∧ 𝐴 ∈ ℋ) → (normℎ‘(𝑇‘𝐴)) = (normℎ‘𝐴)) | ||
| Theorem | cnvunop 31900 | The inverse (converse) of a unitary operator in Hilbert space is unitary. Theorem in [AkhiezerGlazman] p. 72. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ UniOp → ◡𝑇 ∈ UniOp) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |