Home | Metamath
Proof Explorer Theorem List (p. 297 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eigvecval 29601* | 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 29602* | 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 29603* | 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 29604 | The spectrum of an operator is a set of complex numbers. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ ℋ → (Lambda‘𝑇) ⊆ ℂ) | ||
Theorem | hhlnoi 29605 | 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 29606 | 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 29607 | 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 29608 | The zero operator in Hilbert space. (Contributed by NM, 7-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑍 = (𝑈 0op 𝑈) ⇒ ⊢ 0hop = 𝑍 | ||
Theorem | hhcno 29609 | The continuous operators of Hilbert space. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
⊢ 𝐷 = (normℎ ∘ −ℎ ) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ContOp = (𝐽 Cn 𝐽) | ||
Theorem | hhcnf 29610 | 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 29611 | 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 6694.) (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ dom adjℎ ↔ (adjℎ‘𝑇) ∈ dom adjℎ) | ||
Theorem | nmoplb 29612 | A lower bound for an operator norm. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ ℋ ∧ (normℎ‘𝐴) ≤ 1) → (normℎ‘(𝑇‘𝐴)) ≤ (normop‘𝑇)) | ||
Theorem | nmopub 29613* | An upper bound for an operator norm. (Contributed by NM, 7-Mar-2006.) (New usage is discouraged.) |
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ ℝ*) → ((normop‘𝑇) ≤ 𝐴 ↔ ∀𝑥 ∈ ℋ ((normℎ‘𝑥) ≤ 1 → (normℎ‘(𝑇‘𝑥)) ≤ 𝐴))) | ||
Theorem | nmopub2tALT 29614* | 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 29615* | An upper bound for an operator norm. (Contributed by NM, 13-Dec-2007.) (New usage is discouraged.) |
⊢ ((𝑇: ℋ⟶ ℋ ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ ∀𝑥 ∈ ℋ (normℎ‘(𝑇‘𝑥)) ≤ (𝐴 · (normℎ‘𝑥))) → (normop‘𝑇) ≤ 𝐴) | ||
Theorem | nmopge0 29616 | The norm of any Hilbert space operator is nonnegative. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ ℋ → 0 ≤ (normop‘𝑇)) | ||
Theorem | nmopgt0 29617 | 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 29618* | 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 29619 | Basic linearity property of a linear Hilbert space operator. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
⊢ (((𝑇 ∈ LinOp ∧ 𝐴 ∈ ℂ) ∧ (𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)) → (𝑇‘((𝐴 ·ℎ 𝐵) +ℎ 𝐶)) = ((𝐴 ·ℎ (𝑇‘𝐵)) +ℎ (𝑇‘𝐶))) | ||
Theorem | unop 29620 | Basic inner product property of a unitary operator. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ UniOp ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝑇‘𝐴) ·ih (𝑇‘𝐵)) = (𝐴 ·ih 𝐵)) | ||
Theorem | unopf1o 29621 | 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 29622 | A unitary operator is idempotent in the norm. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ UniOp ∧ 𝐴 ∈ ℋ) → (normℎ‘(𝑇‘𝐴)) = (normℎ‘𝐴)) | ||
Theorem | cnvunop 29623 | 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) | ||
Theorem | unopadj 29624 | The inverse (converse) of a unitary operator is its adjoint. Equation 2 of [AkhiezerGlazman] p. 72. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ UniOp ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝑇‘𝐴) ·ih 𝐵) = (𝐴 ·ih (◡𝑇‘𝐵))) | ||
Theorem | unoplin 29625 | A unitary operator is linear. Theorem in [AkhiezerGlazman] p. 72. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ UniOp → 𝑇 ∈ LinOp) | ||
Theorem | counop 29626 | The composition of two unitary operators is unitary. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
⊢ ((𝑆 ∈ UniOp ∧ 𝑇 ∈ UniOp) → (𝑆 ∘ 𝑇) ∈ UniOp) | ||
Theorem | hmop 29627 | Basic inner product property of a Hermitian operator. (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ HrmOp ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵)) | ||
Theorem | hmopre 29628 | The inner product of the value and argument of a Hermitian operator is real. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ HrmOp ∧ 𝐴 ∈ ℋ) → ((𝑇‘𝐴) ·ih 𝐴) ∈ ℝ) | ||
Theorem | nmfnlb 29629 | A lower bound for a functional norm. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
⊢ ((𝑇: ℋ⟶ℂ ∧ 𝐴 ∈ ℋ ∧ (normℎ‘𝐴) ≤ 1) → (abs‘(𝑇‘𝐴)) ≤ (normfn‘𝑇)) | ||
Theorem | nmfnleub 29630* | An upper bound for the norm of a functional. (Contributed by NM, 24-May-2006.) (Revised by Mario Carneiro, 7-Sep-2014.) (New usage is discouraged.) |
⊢ ((𝑇: ℋ⟶ℂ ∧ 𝐴 ∈ ℝ*) → ((normfn‘𝑇) ≤ 𝐴 ↔ ∀𝑥 ∈ ℋ ((normℎ‘𝑥) ≤ 1 → (abs‘(𝑇‘𝑥)) ≤ 𝐴))) | ||
Theorem | nmfnleub2 29631* | An upper bound for the norm of a functional. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
⊢ ((𝑇: ℋ⟶ℂ ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ ∀𝑥 ∈ ℋ (abs‘(𝑇‘𝑥)) ≤ (𝐴 · (normℎ‘𝑥))) → (normfn‘𝑇) ≤ 𝐴) | ||
Theorem | nmfnge0 29632 | The norm of any Hilbert space functional is nonnegative. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ℂ → 0 ≤ (normfn‘𝑇)) | ||
Theorem | elnlfn 29633 | Membership in the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ℂ → (𝐴 ∈ (null‘𝑇) ↔ (𝐴 ∈ ℋ ∧ (𝑇‘𝐴) = 0))) | ||
Theorem | elnlfn2 29634 | Membership in the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
⊢ ((𝑇: ℋ⟶ℂ ∧ 𝐴 ∈ (null‘𝑇)) → (𝑇‘𝐴) = 0) | ||
Theorem | cnfnc 29635* | Basic continuity property of a continuous functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ ContFn ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℝ+) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ ℋ ((normℎ‘(𝑦 −ℎ 𝐴)) < 𝑥 → (abs‘((𝑇‘𝑦) − (𝑇‘𝐴))) < 𝐵)) | ||
Theorem | lnfnl 29636 | Basic linearity property of a linear functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
⊢ (((𝑇 ∈ LinFn ∧ 𝐴 ∈ ℂ) ∧ (𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)) → (𝑇‘((𝐴 ·ℎ 𝐵) +ℎ 𝐶)) = ((𝐴 · (𝑇‘𝐵)) + (𝑇‘𝐶))) | ||
Theorem | adjcl 29637 | Closure of the adjoint of a Hilbert space operator. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ) → ((adjℎ‘𝑇)‘𝐴) ∈ ℋ) | ||
Theorem | adj1 29638 | Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih (𝑇‘𝐵)) = (((adjℎ‘𝑇)‘𝐴) ·ih 𝐵)) | ||
Theorem | adj2 29639 | Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝑇‘𝐴) ·ih 𝐵) = (𝐴 ·ih ((adjℎ‘𝑇)‘𝐵))) | ||
Theorem | adjeq 29640* | A property that determines the adjoint of a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑆‘𝑦))) → (adjℎ‘𝑇) = 𝑆) | ||
Theorem | adjadj 29641 | Double adjoint. Theorem 3.11(iv) of [Beran] p. 106. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ dom adjℎ → (adjℎ‘(adjℎ‘𝑇)) = 𝑇) | ||
Theorem | adjvalval 29642* | Value of the value of the adjoint function. (Contributed by NM, 22-Feb-2006.) (Proof shortened by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ) → ((adjℎ‘𝑇)‘𝐴) = (℩𝑤 ∈ ℋ ∀𝑥 ∈ ℋ ((𝑇‘𝑥) ·ih 𝐴) = (𝑥 ·ih 𝑤))) | ||
Theorem | unopadj2 29643 | The adjoint of a unitary operator is its inverse (converse). Equation 2 of [AkhiezerGlazman] p. 72. (Contributed by NM, 23-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ UniOp → (adjℎ‘𝑇) = ◡𝑇) | ||
Theorem | hmopadj 29644 | A Hermitian operator is self-adjoint. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ HrmOp → (adjℎ‘𝑇) = 𝑇) | ||
Theorem | hmdmadj 29645 | Every Hermitian operator has an adjoint. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ HrmOp → 𝑇 ∈ dom adjℎ) | ||
Theorem | hmopadj2 29646 | An operator is Hermitian iff it is self-adjoint. Definition of Hermitian in [Halmos] p. 41. (Contributed by NM, 9-Apr-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ dom adjℎ → (𝑇 ∈ HrmOp ↔ (adjℎ‘𝑇) = 𝑇)) | ||
Theorem | hmoplin 29647 | A Hermitian operator is linear. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ HrmOp → 𝑇 ∈ LinOp) | ||
Theorem | brafval 29648* | The bra of a vector, expressed as 〈𝐴 ∣ in Dirac notation. See df-bra 29555. (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (bra‘𝐴) = (𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐴))) | ||
Theorem | braval 29649 | A bra-ket juxtaposition, expressed as 〈𝐴 ∣ 𝐵〉 in Dirac notation, equals the inner product of the vectors. Based on definition of bra in [Prugovecki] p. 186. (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((bra‘𝐴)‘𝐵) = (𝐵 ·ih 𝐴)) | ||
Theorem | braadd 29650 | Linearity property of bra for addition. (Contributed by NM, 23-May-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((bra‘𝐴)‘(𝐵 +ℎ 𝐶)) = (((bra‘𝐴)‘𝐵) + ((bra‘𝐴)‘𝐶))) | ||
Theorem | bramul 29651 | Linearity property of bra for multiplication. (Contributed by NM, 23-May-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((bra‘𝐴)‘(𝐵 ·ℎ 𝐶)) = (𝐵 · ((bra‘𝐴)‘𝐶))) | ||
Theorem | brafn 29652 | The bra function is a functional. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (bra‘𝐴): ℋ⟶ℂ) | ||
Theorem | bralnfn 29653 | The Dirac bra function is a linear functional. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (bra‘𝐴) ∈ LinFn) | ||
Theorem | bracl 29654 | Closure of the bra function. (Contributed by NM, 23-May-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((bra‘𝐴)‘𝐵) ∈ ℂ) | ||
Theorem | bra0 29655 | The Dirac bra of the zero vector. (Contributed by NM, 25-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
⊢ (bra‘0ℎ) = ( ℋ × {0}) | ||
Theorem | brafnmul 29656 | Anti-linearity property of bra functional for multiplication. (Contributed by NM, 31-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (bra‘(𝐴 ·ℎ 𝐵)) = ((∗‘𝐴) ·fn (bra‘𝐵))) | ||
Theorem | kbfval 29657* | The outer product of two vectors, expressed as ∣ 𝐴〉 〈𝐵 ∣ in Dirac notation. See df-kb 29556. (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ketbra 𝐵) = (𝑥 ∈ ℋ ↦ ((𝑥 ·ih 𝐵) ·ℎ 𝐴))) | ||
Theorem | kbop 29658 | The outer product of two vectors, expressed as ∣ 𝐴〉 〈𝐵 ∣ in Dirac notation, is an operator. (Contributed by NM, 30-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ketbra 𝐵): ℋ⟶ ℋ) | ||
Theorem | kbval 29659 | The value of the operator resulting from the outer product ∣ 𝐴〉 〈𝐵 ∣ of two vectors. Equation 8.1 of [Prugovecki] p. 376. (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ketbra 𝐵)‘𝐶) = ((𝐶 ·ih 𝐵) ·ℎ 𝐴)) | ||
Theorem | kbmul 29660 | Multiplication property of outer product. (Contributed by NM, 31-May-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ketbra 𝐶) = (𝐵 ketbra ((∗‘𝐴) ·ℎ 𝐶))) | ||
Theorem | kbpj 29661 | If a vector 𝐴 has norm 1, the outer product ∣ 𝐴〉 〈𝐴 ∣ is the projector onto the subspace spanned by 𝐴. http://en.wikipedia.org/wiki/Bra-ket#Linear%5Foperators. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ (normℎ‘𝐴) = 1) → (𝐴 ketbra 𝐴) = (projℎ‘(span‘{𝐴}))) | ||
Theorem | eleigvec 29662* | Membership in 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 | eleigvec2 29663 | Membership in the set of eigenvectors of a Hilbert space operator. (Contributed by NM, 18-Mar-2006.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ ℋ → (𝐴 ∈ (eigvec‘𝑇) ↔ (𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ∧ (𝑇‘𝐴) ∈ (span‘{𝐴})))) | ||
Theorem | eleigveccl 29664 | Closure of an eigenvector of a Hilbert space operator. (Contributed by NM, 23-Mar-2006.) (New usage is discouraged.) |
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ (eigvec‘𝑇)) → 𝐴 ∈ ℋ) | ||
Theorem | eigvalval 29665 | The eigenvalue of an eigenvector of a Hilbert space operator. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ (eigvec‘𝑇)) → ((eigval‘𝑇)‘𝐴) = (((𝑇‘𝐴) ·ih 𝐴) / ((normℎ‘𝐴)↑2))) | ||
Theorem | eigvalcl 29666 | An eigenvalue is a complex number. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ (eigvec‘𝑇)) → ((eigval‘𝑇)‘𝐴) ∈ ℂ) | ||
Theorem | eigvec1 29667 | Property of an eigenvector. (Contributed by NM, 12-Mar-2006.) (New usage is discouraged.) |
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ (eigvec‘𝑇)) → ((𝑇‘𝐴) = (((eigval‘𝑇)‘𝐴) ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) | ||
Theorem | eighmre 29668 | The eigenvalues of a Hermitian operator are real. Equation 1.30 of [Hughes] p. 49. (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ HrmOp ∧ 𝐴 ∈ (eigvec‘𝑇)) → ((eigval‘𝑇)‘𝐴) ∈ ℝ) | ||
Theorem | eighmorth 29669 | Eigenvectors of a Hermitian operator with distinct eigenvalues are orthogonal. Equation 1.31 of [Hughes] p. 49. (Contributed by NM, 23-Mar-2006.) (New usage is discouraged.) |
⊢ (((𝑇 ∈ HrmOp ∧ 𝐴 ∈ (eigvec‘𝑇)) ∧ (𝐵 ∈ (eigvec‘𝑇) ∧ ((eigval‘𝑇)‘𝐴) ≠ ((eigval‘𝑇)‘𝐵))) → (𝐴 ·ih 𝐵) = 0) | ||
Theorem | nmopnegi 29670 | Value of the norm of the negative of a Hilbert space operator. Unlike nmophmi 29736, the operator does not have to be bounded. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (normop‘(-1 ·op 𝑇)) = (normop‘𝑇) | ||
Theorem | lnop0 29671 | The value of a linear Hilbert space operator at zero is zero. Remark in [Beran] p. 99. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ LinOp → (𝑇‘0ℎ) = 0ℎ) | ||
Theorem | lnopmul 29672 | Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ LinOp ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 ·ℎ (𝑇‘𝐵))) | ||
Theorem | lnopli 29673 | Basic scalar product property of a linear Hilbert space operator. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘((𝐴 ·ℎ 𝐵) +ℎ 𝐶)) = ((𝐴 ·ℎ (𝑇‘𝐵)) +ℎ (𝑇‘𝐶))) | ||
Theorem | lnopfi 29674 | A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ 𝑇: ℋ⟶ ℋ | ||
Theorem | lnop0i 29675 | The value of a linear Hilbert space operator at zero is zero. Remark in [Beran] p. 99. (Contributed by NM, 11-May-2005.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ (𝑇‘0ℎ) = 0ℎ | ||
Theorem | lnopaddi 29676 | Additive property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 +ℎ 𝐵)) = ((𝑇‘𝐴) +ℎ (𝑇‘𝐵))) | ||
Theorem | lnopmuli 29677 | Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 ·ℎ (𝑇‘𝐵))) | ||
Theorem | lnopaddmuli 29678 | Sum/product property of a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘(𝐵 +ℎ (𝐴 ·ℎ 𝐶))) = ((𝑇‘𝐵) +ℎ (𝐴 ·ℎ (𝑇‘𝐶)))) | ||
Theorem | lnopsubi 29679 | Subtraction property for a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 −ℎ 𝐵)) = ((𝑇‘𝐴) −ℎ (𝑇‘𝐵))) | ||
Theorem | lnopsubmuli 29680 | Subtraction/product property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘(𝐵 −ℎ (𝐴 ·ℎ 𝐶))) = ((𝑇‘𝐵) −ℎ (𝐴 ·ℎ (𝑇‘𝐶)))) | ||
Theorem | lnopmulsubi 29681 | Product/subtraction property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘((𝐴 ·ℎ 𝐵) −ℎ 𝐶)) = ((𝐴 ·ℎ (𝑇‘𝐵)) −ℎ (𝑇‘𝐶))) | ||
Theorem | homco2 29682 | Move a scalar product out of a composition of operators. The operator 𝑇 must be linear, unlike homco1 29506 that works for any operators. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 ∘ (𝐴 ·op 𝑈)) = (𝐴 ·op (𝑇 ∘ 𝑈))) | ||
Theorem | idunop 29683 | The identity function (restricted to Hilbert space) is a unitary operator. (Contributed by NM, 21-Jan-2006.) (New usage is discouraged.) |
⊢ ( I ↾ ℋ) ∈ UniOp | ||
Theorem | 0cnop 29684 | The identically zero function is a continuous Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
⊢ 0hop ∈ ContOp | ||
Theorem | 0cnfn 29685 | The identically zero function is a continuous Hilbert space functional. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
⊢ ( ℋ × {0}) ∈ ContFn | ||
Theorem | idcnop 29686 | The identity function (restricted to Hilbert space) is a continuous operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
⊢ ( I ↾ ℋ) ∈ ContOp | ||
Theorem | idhmop 29687 | The Hilbert space identity operator is a Hermitian operator. (Contributed by NM, 22-Apr-2006.) (New usage is discouraged.) |
⊢ Iop ∈ HrmOp | ||
Theorem | 0hmop 29688 | The identically zero function is a Hermitian operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.) |
⊢ 0hop ∈ HrmOp | ||
Theorem | 0lnop 29689 | The identically zero function is a linear Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
⊢ 0hop ∈ LinOp | ||
Theorem | 0lnfn 29690 | The identically zero function is a linear Hilbert space functional. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
⊢ ( ℋ × {0}) ∈ LinFn | ||
Theorem | nmop0 29691 | The norm of the zero operator is zero. (Contributed by NM, 8-Feb-2006.) (New usage is discouraged.) |
⊢ (normop‘ 0hop ) = 0 | ||
Theorem | nmfn0 29692 | The norm of the identically zero functional is zero. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
⊢ (normfn‘( ℋ × {0})) = 0 | ||
Theorem | hmopbdoptHIL 29693 | A Hermitian operator is a bounded linear operator (Hellinger-Toeplitz Theorem). (Contributed by NM, 18-Jan-2008.) (New usage is discouraged.) |
⊢ (𝑇 ∈ HrmOp → 𝑇 ∈ BndLinOp) | ||
Theorem | hoddii 29694 | Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 29485 does not require linearity.) (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
⊢ 𝑅 ∈ LinOp & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑅 ∘ (𝑆 −op 𝑇)) = ((𝑅 ∘ 𝑆) −op (𝑅 ∘ 𝑇)) | ||
Theorem | hoddi 29695 | Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 29485 does not require linearity.) (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝑅 ∈ LinOp ∧ 𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑅 ∘ (𝑆 −op 𝑇)) = ((𝑅 ∘ 𝑆) −op (𝑅 ∘ 𝑇))) | ||
Theorem | nmop0h 29696 | The norm of any operator on the trivial Hilbert space is zero. (This is the reason we need ℋ ≠ 0ℋ in nmopun 29719.) (Contributed by NM, 24-Feb-2006.) (New usage is discouraged.) |
⊢ (( ℋ = 0ℋ ∧ 𝑇: ℋ⟶ ℋ) → (normop‘𝑇) = 0) | ||
Theorem | idlnop 29697 | The identity function (restricted to Hilbert space) is a linear operator. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.) |
⊢ ( I ↾ ℋ) ∈ LinOp | ||
Theorem | 0bdop 29698 | The identically zero operator is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
⊢ 0hop ∈ BndLinOp | ||
Theorem | adj0 29699 | Adjoint of the zero operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
⊢ (adjℎ‘ 0hop ) = 0hop | ||
Theorem | nmlnop0iALT 29700 | A linear operator with a zero norm is identically zero. (Contributed by NM, 8-Feb-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((normop‘𝑇) = 0 ↔ 𝑇 = 0hop ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |