HomeTheorem List (p. 321 of 497)
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. 321 of 497) | < 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-30845) |
Hilbert Space Explorer
(30846-32368) |
Users' Mathboxes
(32369-49617) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cnlnadjlem8 32001* | Lemma for cnlnadji 32003. 𝐹 is continuous. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ContOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) & ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) & ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵) ⇒ ⊢ 𝐹 ∈ ContOp | ||
| Theorem | cnlnadjlem9 32002* | Lemma for cnlnadji 32003. 𝐹 provides an example showing the existence of a continuous linear adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ContOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) & ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) & ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵) ⇒ ⊢ ∃𝑡 ∈ (LinOp ∩ ContOp)∀𝑥 ∈ ℋ ∀𝑧 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑧) = (𝑥 ·ih (𝑡‘𝑧)) | ||
| Theorem | cnlnadji 32003* | Every continuous linear operator has an adjoint. Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ContOp ⇒ ⊢ ∃𝑡 ∈ (LinOp ∩ ContOp)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡‘𝑦)) | ||
| Theorem | cnlnadjeui 32004* | Every continuous linear operator has a unique adjoint. Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ContOp ⇒ ⊢ ∃!𝑡 ∈ (LinOp ∩ ContOp)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡‘𝑦)) | ||
| Theorem | cnlnadjeu 32005* | Every continuous linear operator has a unique adjoint. Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ (LinOp ∩ ContOp) → ∃!𝑡 ∈ (LinOp ∩ ContOp)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡‘𝑦))) | ||
| Theorem | cnlnadj 32006* | Every continuous linear operator has an adjoint. Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ (LinOp ∩ ContOp) → ∃𝑡 ∈ (LinOp ∩ ContOp)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡‘𝑦))) | ||
| Theorem | cnlnssadj 32007 | Every continuous linear Hilbert space operator has an adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
| ⊢ (LinOp ∩ ContOp) ⊆ dom adjℎ | ||
| Theorem | bdopssadj 32008 | Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
| ⊢ BndLinOp ⊆ dom adjℎ | ||
| Theorem | bdopadj 32009 | Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ BndLinOp → 𝑇 ∈ dom adjℎ) | ||
| Theorem | adjbdln 32010 | The adjoint of a bounded linear operator is a bounded linear operator. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ BndLinOp → (adjℎ‘𝑇) ∈ BndLinOp) | ||
| Theorem | adjbdlnb 32011 | An operator is bounded and linear iff its adjoint is. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ BndLinOp ↔ (adjℎ‘𝑇) ∈ BndLinOp) | ||
| Theorem | adjbd1o 32012 | The mapping of adjoints of bounded linear operators is one-to-one onto. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
| ⊢ (adjℎ ↾ BndLinOp):BndLinOp–1-1-onto→BndLinOp | ||
| Theorem | adjlnop 32013 | The adjoint of an operator is linear. Proposition 1 of [AkhiezerGlazman] p. 80. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ dom adjℎ → (adjℎ‘𝑇) ∈ LinOp) | ||
| Theorem | adjsslnop 32014 | Every operator with an adjoint is linear. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.) |
| ⊢ dom adjℎ ⊆ LinOp | ||
| Theorem | nmopadjlei 32015 | Property of the norm of an adjoint. Part of proof of Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (𝐴 ∈ ℋ → (normℎ‘((adjℎ‘𝑇)‘𝐴)) ≤ ((normop‘𝑇) · (normℎ‘𝐴))) | ||
| Theorem | nmopadjlem 32016 | Lemma for nmopadji 32017. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (normop‘(adjℎ‘𝑇)) ≤ (normop‘𝑇) | ||
| Theorem | nmopadji 32017 | Property of the norm of an adjoint. Theorem 3.11(v) of [Beran] p. 106. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (normop‘(adjℎ‘𝑇)) = (normop‘𝑇) | ||
| Theorem | adjeq0 32018 | An operator is zero iff its adjoint is zero. Theorem 3.11(i) of [Beran] p. 106. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 = 0hop ↔ (adjℎ‘𝑇) = 0hop ) | ||
| Theorem | adjmul 32019 | The adjoint of the scalar product of an operator. Theorem 3.11(ii) of [Beran] p. 106. (Contributed by NM, 21-Feb-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑇 ∈ dom adjℎ) → (adjℎ‘(𝐴 ·op 𝑇)) = ((∗‘𝐴) ·op (adjℎ‘𝑇))) | ||
| Theorem | adjadd 32020 | The adjoint of the sum of two operators. Theorem 3.11(iii) of [Beran] p. 106. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ) → (adjℎ‘(𝑆 +op 𝑇)) = ((adjℎ‘𝑆) +op (adjℎ‘𝑇))) | ||
| Theorem | nmoptrii 32021 | Triangle inequality for the norms of bounded linear operators. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑆 ∈ BndLinOp & ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (normop‘(𝑆 +op 𝑇)) ≤ ((normop‘𝑆) + (normop‘𝑇)) | ||
| Theorem | nmopcoi 32022 | Upper bound for the norm of the composition of two bounded linear operators. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑆 ∈ BndLinOp & ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (normop‘(𝑆 ∘ 𝑇)) ≤ ((normop‘𝑆) · (normop‘𝑇)) | ||
| Theorem | bdophsi 32023 | The sum of two bounded linear operators is a bounded linear operator. (Contributed by NM, 9-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑆 ∈ BndLinOp & ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (𝑆 +op 𝑇) ∈ BndLinOp | ||
| Theorem | bdophdi 32024 | The difference between two bounded linear operators is bounded. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑆 ∈ BndLinOp & ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (𝑆 −op 𝑇) ∈ BndLinOp | ||
| Theorem | bdopcoi 32025 | The composition of two bounded linear operators is bounded. (Contributed by NM, 9-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑆 ∈ BndLinOp & ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (𝑆 ∘ 𝑇) ∈ BndLinOp | ||
| Theorem | nmoptri2i 32026 | Triangle-type inequality for the norms of bounded linear operators. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑆 ∈ BndLinOp & ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ ((normop‘𝑆) − (normop‘𝑇)) ≤ (normop‘(𝑆 +op 𝑇)) | ||
| Theorem | adjcoi 32027 | The adjoint of a composition of bounded linear operators. Theorem 3.11(viii) of [Beran] p. 106. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑆 ∈ BndLinOp & ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (adjℎ‘(𝑆 ∘ 𝑇)) = ((adjℎ‘𝑇) ∘ (adjℎ‘𝑆)) | ||
| Theorem | nmopcoadji 32028 | The norm of an operator composed with its adjoint. Part of Theorem 3.11(vi) of [Beran] p. 106. (Contributed by NM, 8-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (normop‘((adjℎ‘𝑇) ∘ 𝑇)) = ((normop‘𝑇)↑2) | ||
| Theorem | nmopcoadj2i 32029 | The norm of an operator composed with its adjoint. Part of Theorem 3.11(vi) of [Beran] p. 106. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (normop‘(𝑇 ∘ (adjℎ‘𝑇))) = ((normop‘𝑇)↑2) | ||
| Theorem | nmopcoadj0i 32030 | An operator composed with its adjoint is zero iff the operator is zero. Theorem 3.11(vii) of [Beran] p. 106. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ ((𝑇 ∘ (adjℎ‘𝑇)) = 0hop ↔ 𝑇 = 0hop ) | ||
| Theorem | unierri 32031 | If we approximate a chain of unitary transformations (quantum computer gates) 𝐹, 𝐺 by other unitary transformations 𝑆, 𝑇, the error increases at most additively. Equation 4.73 of [NielsenChuang] p. 195. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝐹 ∈ UniOp & ⊢ 𝐺 ∈ UniOp & ⊢ 𝑆 ∈ UniOp & ⊢ 𝑇 ∈ UniOp ⇒ ⊢ (normop‘((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝑇))) ≤ ((normop‘(𝐹 −op 𝑆)) + (normop‘(𝐺 −op 𝑇))) | ||
| Theorem | branmfn 32032 | The norm of the bra function. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (normfn‘(bra‘𝐴)) = (normℎ‘𝐴)) | ||
| Theorem | brabn 32033 | The bra of a vector is a bounded functional. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (normfn‘(bra‘𝐴)) ∈ ℝ) | ||
| Theorem | rnbra 32034 | The set of bras equals the set of continuous linear functionals. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
| ⊢ ran bra = (LinFn ∩ ContFn) | ||
| Theorem | bra11 32035 | The bra function maps vectors one-to-one onto the set of continuous linear functionals. (Contributed by NM, 26-May-2006.) (Proof shortened by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ bra: ℋ–1-1-onto→(LinFn ∩ ContFn) | ||
| Theorem | bracnln 32036 | A bra is a continuous linear functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (bra‘𝐴) ∈ (LinFn ∩ ContFn)) | ||
| Theorem | cnvbraval 32037* | Value of the converse of the bra function. Based on the Riesz Lemma riesz4 31991, this very important theorem not only justifies the Dirac bra-ket notation, but allows to extract a unique vector from any continuous linear functional from which the functional can be recovered; i.e. a single vector can "store" all of the information contained in any entire continuous linear functional (mapping from ℋ to ℂ). (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ (LinFn ∩ ContFn) → (◡bra‘𝑇) = (℩𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦))) | ||
| Theorem | cnvbracl 32038 | Closure of the converse of the bra function. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ (LinFn ∩ ContFn) → (◡bra‘𝑇) ∈ ℋ) | ||
| Theorem | cnvbrabra 32039 | The converse bra of the bra of a vector is the vector itself. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (◡bra‘(bra‘𝐴)) = 𝐴) | ||
| Theorem | bracnvbra 32040 | The bra of the converse bra of a continuous linear functional. (Contributed by NM, 31-May-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ (LinFn ∩ ContFn) → (bra‘(◡bra‘𝑇)) = 𝑇) | ||
| Theorem | bracnlnval 32041* | The vector that a continuous linear functional is the bra of. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ (LinFn ∩ ContFn) → 𝑇 = (bra‘(℩𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦)))) | ||
| Theorem | cnvbramul 32042 | Multiplication property of the converse bra function. (Contributed by NM, 31-May-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑇 ∈ (LinFn ∩ ContFn)) → (◡bra‘(𝐴 ·fn 𝑇)) = ((∗‘𝐴) ·ℎ (◡bra‘𝑇))) | ||
| Theorem | kbass1 32043 | Dirac bra-ket associative law ( ∣ 𝐴⟩⟨𝐵 ∣ ) ∣ 𝐶⟩ = ∣ 𝐴⟩(⟨𝐵 ∣ 𝐶⟩), i.e., the juxtaposition of an outer product with a ket equals a bra juxtaposed with an inner product. Since ⟨𝐵 ∣ 𝐶⟩ is a complex number, it is the first argument in the inner product ·ℎ that it is mapped to, although in Dirac notation it is placed after the ket. (Contributed by NM, 15-May-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ketbra 𝐵)‘𝐶) = (((bra‘𝐵)‘𝐶) ·ℎ 𝐴)) | ||
| Theorem | kbass2 32044 | Dirac bra-ket associative law (⟨𝐴 ∣ 𝐵⟩)⟨𝐶 ∣ = ⟨𝐴 ∣ ( ∣ 𝐵⟩⟨𝐶 ∣ ), i.e., the juxtaposition of an inner product with a bra equals a ket juxtaposed with an outer product. (Contributed by NM, 23-May-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (((bra‘𝐴)‘𝐵) ·fn (bra‘𝐶)) = ((bra‘𝐴) ∘ (𝐵 ketbra 𝐶))) | ||
| Theorem | kbass3 32045 | Dirac bra-ket associative law ⟨𝐴 ∣ 𝐵⟩⟨𝐶 ∣ 𝐷⟩ = (⟨𝐴 ∣ 𝐵⟩⟨𝐶 ∣ ) ∣ 𝐷⟩. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝐷)) = ((((bra‘𝐴)‘𝐵) ·fn (bra‘𝐶))‘𝐷)) | ||
| Theorem | kbass4 32046 | Dirac bra-ket associative law ⟨𝐴 ∣ 𝐵⟩⟨𝐶 ∣ 𝐷⟩ = ⟨𝐴 ∣ ( ∣ 𝐵⟩⟨𝐶 ∣ 𝐷⟩). (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝐷)) = ((bra‘𝐴)‘(((bra‘𝐶)‘𝐷) ·ℎ 𝐵))) | ||
| Theorem | kbass5 32047 | Dirac bra-ket associative law ( ∣ 𝐴⟩⟨𝐵 ∣ )( ∣ 𝐶⟩⟨𝐷 ∣ ) = (( ∣ 𝐴⟩⟨𝐵 ∣ ) ∣ 𝐶⟩)⟨𝐷 ∣. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 ketbra 𝐵) ∘ (𝐶 ketbra 𝐷)) = (((𝐴 ketbra 𝐵)‘𝐶) ketbra 𝐷)) | ||
| Theorem | kbass6 32048 | Dirac bra-ket associative law ( ∣ 𝐴⟩⟨𝐵 ∣ )( ∣ 𝐶⟩⟨𝐷 ∣ ) = ∣ 𝐴⟩(⟨𝐵 ∣ ( ∣ 𝐶⟩⟨𝐷 ∣ )). (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 ketbra 𝐵) ∘ (𝐶 ketbra 𝐷)) = (𝐴 ketbra (◡bra‘((bra‘𝐵) ∘ (𝐶 ketbra 𝐷))))) | ||
| Theorem | leopg 32049* | Ordering relation for positive operators. Definition of positive operator ordering in [Kreyszig] p. 470. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐵) → (𝑇 ≤op 𝑈 ↔ ((𝑈 −op 𝑇) ∈ HrmOp ∧ ∀𝑥 ∈ ℋ 0 ≤ (((𝑈 −op 𝑇)‘𝑥) ·ih 𝑥)))) | ||
| Theorem | leop 32050* | Ordering relation for operators. Definition of positive operator ordering in [Kreyszig] p. 470. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 ≤op 𝑈 ↔ ∀𝑥 ∈ ℋ 0 ≤ (((𝑈 −op 𝑇)‘𝑥) ·ih 𝑥))) | ||
| Theorem | leop2 32051* | Ordering relation for operators. Definition of operator ordering in [Young] p. 141. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 ≤op 𝑈 ↔ ∀𝑥 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑥) ≤ ((𝑈‘𝑥) ·ih 𝑥))) | ||
| Theorem | leop3 32052 | Operator ordering in terms of a positive operator. Definition of operator ordering in [Retherford] p. 49. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 ≤op 𝑈 ↔ 0hop ≤op (𝑈 −op 𝑇))) | ||
| Theorem | leoppos 32053* | Binary relation defining a positive operator. Definition VI.1 of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ HrmOp → ( 0hop ≤op 𝑇 ↔ ∀𝑥 ∈ ℋ 0 ≤ ((𝑇‘𝑥) ·ih 𝑥))) | ||
| Theorem | leoprf2 32054 | The ordering relation for operators is reflexive. (Contributed by NM, 24-Jul-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → 𝑇 ≤op 𝑇) | ||
| Theorem | leoprf 32055 | The ordering relation for operators is reflexive. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ HrmOp → 𝑇 ≤op 𝑇) | ||
| Theorem | leopsq 32056 | The square of a Hermitian operator is positive. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ HrmOp → 0hop ≤op (𝑇 ∘ 𝑇)) | ||
| Theorem | 0leop 32057 | The zero operator is a positive operator. (The literature calls it "positive", even though in some sense it is really "nonnegative".) Part of Example 12.2(i) in [Young] p. 142. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
| ⊢ 0hop ≤op 0hop | ||
| Theorem | idleop 32058 | The identity operator is a positive operator. Part of Example 12.2(i) in [Young] p. 142. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
| ⊢ 0hop ≤op Iop | ||
| Theorem | leopadd 32059 | The sum of two positive operators is positive. Exercise 1(i) of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
| ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ ( 0hop ≤op 𝑇 ∧ 0hop ≤op 𝑈)) → 0hop ≤op (𝑇 +op 𝑈)) | ||
| Theorem | leopmuli 32060 | The scalar product of a nonnegative real and a positive operator is a positive operator. Exercise 1(ii) of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp) ∧ (0 ≤ 𝐴 ∧ 0hop ≤op 𝑇)) → 0hop ≤op (𝐴 ·op 𝑇)) | ||
| Theorem | leopmul 32061 | The scalar product of a positive real and a positive operator is a positive operator. Exercise 1(ii) of [Retherford] p. 49. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 0 < 𝐴) → ( 0hop ≤op 𝑇 ↔ 0hop ≤op (𝐴 ·op 𝑇))) | ||
| Theorem | leopmul2i 32062 | Scalar product applied to operator ordering. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (0 ≤ 𝐴 ∧ 𝑇 ≤op 𝑈)) → (𝐴 ·op 𝑇) ≤op (𝐴 ·op 𝑈)) | ||
| Theorem | leoptri 32063 | The positive operator ordering relation satisfies trichotomy. Exercise 1(iii) of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → ((𝑇 ≤op 𝑈 ∧ 𝑈 ≤op 𝑇) ↔ 𝑇 = 𝑈)) | ||
| Theorem | leoptr 32064 | The positive operator ordering relation is transitive. Exercise 1(iv) of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
| ⊢ (((𝑆 ∈ HrmOp ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑆 ≤op 𝑇 ∧ 𝑇 ≤op 𝑈)) → 𝑆 ≤op 𝑈) | ||
| Theorem | leopnmid 32065 | A bounded Hermitian operator is less than or equal to its norm times the identity operator. (Contributed by NM, 11-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ HrmOp ∧ (normop‘𝑇) ∈ ℝ) → 𝑇 ≤op ((normop‘𝑇) ·op Iop )) | ||
| Theorem | nmopleid 32066 | A nonzero, bounded Hermitian operator divided by its norm is less than or equal to the identity operator. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ HrmOp ∧ (normop‘𝑇) ∈ ℝ ∧ 𝑇 ≠ 0hop ) → ((1 / (normop‘𝑇)) ·op 𝑇) ≤op Iop ) | ||
| Theorem | opsqrlem1 32067* | Lemma for opsqri . (Contributed by NM, 9-Aug-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ HrmOp & ⊢ (normop‘𝑇) ∈ ℝ & ⊢ 0hop ≤op 𝑇 & ⊢ 𝑅 = ((1 / (normop‘𝑇)) ·op 𝑇) & ⊢ (𝑇 ≠ 0hop → ∃𝑢 ∈ HrmOp ( 0hop ≤op 𝑢 ∧ (𝑢 ∘ 𝑢) = 𝑅)) ⇒ ⊢ (𝑇 ≠ 0hop → ∃𝑣 ∈ HrmOp ( 0hop ≤op 𝑣 ∧ (𝑣 ∘ 𝑣) = 𝑇)) | ||
| Theorem | opsqrlem2 32068* | Lemma for opsqri . 𝐹‘𝑁 is the recursive function An (starting at n=1 instead of 0) of Theorem 9.4-2 of [Kreyszig] p. 476. (Contributed by NM, 17-Aug-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ HrmOp & ⊢ 𝑆 = (𝑥 ∈ HrmOp, 𝑦 ∈ HrmOp ↦ (𝑥 +op ((1 / 2) ·op (𝑇 −op (𝑥 ∘ 𝑥))))) & ⊢ 𝐹 = seq1(𝑆, (ℕ × { 0hop })) ⇒ ⊢ (𝐹‘1) = 0hop | ||
| Theorem | opsqrlem3 32069* | Lemma for opsqri . (Contributed by NM, 22-Aug-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ HrmOp & ⊢ 𝑆 = (𝑥 ∈ HrmOp, 𝑦 ∈ HrmOp ↦ (𝑥 +op ((1 / 2) ·op (𝑇 −op (𝑥 ∘ 𝑥))))) & ⊢ 𝐹 = seq1(𝑆, (ℕ × { 0hop })) ⇒ ⊢ ((𝐺 ∈ HrmOp ∧ 𝐻 ∈ HrmOp) → (𝐺𝑆𝐻) = (𝐺 +op ((1 / 2) ·op (𝑇 −op (𝐺 ∘ 𝐺))))) | ||
| Theorem | opsqrlem4 32070* | Lemma for opsqri . (Contributed by NM, 17-Aug-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ HrmOp & ⊢ 𝑆 = (𝑥 ∈ HrmOp, 𝑦 ∈ HrmOp ↦ (𝑥 +op ((1 / 2) ·op (𝑇 −op (𝑥 ∘ 𝑥))))) & ⊢ 𝐹 = seq1(𝑆, (ℕ × { 0hop })) ⇒ ⊢ 𝐹:ℕ⟶HrmOp | ||
| Theorem | opsqrlem5 32071* | Lemma for opsqri . (Contributed by NM, 17-Aug-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ HrmOp & ⊢ 𝑆 = (𝑥 ∈ HrmOp, 𝑦 ∈ HrmOp ↦ (𝑥 +op ((1 / 2) ·op (𝑇 −op (𝑥 ∘ 𝑥))))) & ⊢ 𝐹 = seq1(𝑆, (ℕ × { 0hop })) ⇒ ⊢ (𝑁 ∈ ℕ → (𝐹‘(𝑁 + 1)) = ((𝐹‘𝑁) +op ((1 / 2) ·op (𝑇 −op ((𝐹‘𝑁) ∘ (𝐹‘𝑁)))))) | ||
| Theorem | opsqrlem6 32072* | Lemma for opsqri . (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ HrmOp & ⊢ 𝑆 = (𝑥 ∈ HrmOp, 𝑦 ∈ HrmOp ↦ (𝑥 +op ((1 / 2) ·op (𝑇 −op (𝑥 ∘ 𝑥))))) & ⊢ 𝐹 = seq1(𝑆, (ℕ × { 0hop })) & ⊢ 𝑇 ≤op Iop ⇒ ⊢ (𝑁 ∈ ℕ → (𝐹‘𝑁) ≤op Iop ) | ||
| Theorem | pjhmopi 32073 | A projector is a Hermitian operator. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (projℎ‘𝐻) ∈ HrmOp | ||
| Theorem | pjlnopi 32074 | A projector is a linear operator. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (projℎ‘𝐻) ∈ LinOp | ||
| Theorem | pjnmopi 32075 | The operator norm of a projector on a nonzero closed subspace is one. Part of Theorem 26.1 of [Halmos] p. 43. (Contributed by NM, 9-Apr-2006.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐻 ≠ 0ℋ → (normop‘(projℎ‘𝐻)) = 1) | ||
| Theorem | pjbdlni 32076 | A projector is a bounded linear operator. (Contributed by NM, 3-Jun-2006.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (projℎ‘𝐻) ∈ BndLinOp | ||
| Theorem | pjhmop 32077 | A projection is a Hermitian operator. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
| ⊢ (𝐻 ∈ Cℋ → (projℎ‘𝐻) ∈ HrmOp) | ||
| Theorem | hmopidmchi 32078 | An idempotent Hermitian operator generates a closed subspace. Part of proof of Theorem of [AkhiezerGlazman] p. 64. (Contributed by NM, 21-Apr-2006.) (Proof shortened by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ HrmOp & ⊢ (𝑇 ∘ 𝑇) = 𝑇 ⇒ ⊢ ran 𝑇 ∈ Cℋ | ||
| Theorem | hmopidmpji 32079 | An idempotent Hermitian operator is a projection operator. Theorem 26.4 of [Halmos] p. 44. (Halmos seems to omit the proof that 𝐻 is a closed subspace, which is not trivial as hmopidmchi 32078 shows.) (Contributed by NM, 22-Apr-2006.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ HrmOp & ⊢ (𝑇 ∘ 𝑇) = 𝑇 ⇒ ⊢ 𝑇 = (projℎ‘ran 𝑇) | ||
| Theorem | hmopidmch 32080 | An idempotent Hermitian operator generates a closed subspace. Part of proof of Theorem of [AkhiezerGlazman] p. 64. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ HrmOp ∧ (𝑇 ∘ 𝑇) = 𝑇) → ran 𝑇 ∈ Cℋ ) | ||
| Theorem | hmopidmpj 32081 | An idempotent Hermitian operator is a projection operator. Theorem 26.4 of [Halmos] p. 44. (Contributed by NM, 22-Apr-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ HrmOp ∧ (𝑇 ∘ 𝑇) = 𝑇) → 𝑇 = (projℎ‘ran 𝑇)) | ||
| Theorem | pjsdii 32082 | Distributive law for Hilbert space operator sum. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((projℎ‘𝐻) ∘ (𝑆 +op 𝑇)) = (((projℎ‘𝐻) ∘ 𝑆) +op ((projℎ‘𝐻) ∘ 𝑇)) | ||
| Theorem | pjddii 32083 | Distributive law for Hilbert space operator difference. (Contributed by NM, 24-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((projℎ‘𝐻) ∘ (𝑆 −op 𝑇)) = (((projℎ‘𝐻) ∘ 𝑆) −op ((projℎ‘𝐻) ∘ 𝑇)) | ||
| Theorem | pjsdi2i 32084 | Chained distributive law for Hilbert space operator difference. (Contributed by NM, 30-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 ∘ (𝑆 +op 𝑇)) = ((𝑅 ∘ 𝑆) +op (𝑅 ∘ 𝑇)) → (((projℎ‘𝐻) ∘ 𝑅) ∘ (𝑆 +op 𝑇)) = ((((projℎ‘𝐻) ∘ 𝑅) ∘ 𝑆) +op (((projℎ‘𝐻) ∘ 𝑅) ∘ 𝑇))) | ||
| Theorem | pjcoi 32085 | Composition of projections. (Contributed by NM, 16-Aug-2000.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ ℋ → (((projℎ‘𝐺) ∘ (projℎ‘𝐻))‘𝐴) = ((projℎ‘𝐺)‘((projℎ‘𝐻)‘𝐴))) | ||
| Theorem | pjcocli 32086 | Closure of composition of projections. (Contributed by NM, 29-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ ℋ → (((projℎ‘𝐺) ∘ (projℎ‘𝐻))‘𝐴) ∈ 𝐺) | ||
| Theorem | pjcohcli 32087 | Closure of composition of projections. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ ℋ → (((projℎ‘𝐺) ∘ (projℎ‘𝐻))‘𝐴) ∈ ℋ) | ||
| Theorem | pjadjcoi 32088 | Adjoint of composition of projections. Special case of Theorem 3.11(viii) of [Beran] p. 106. (Contributed by NM, 6-Oct-2000.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((((projℎ‘𝐺) ∘ (projℎ‘𝐻))‘𝐴) ·ih 𝐵) = (𝐴 ·ih (((projℎ‘𝐻) ∘ (projℎ‘𝐺))‘𝐵))) | ||
| Theorem | pjcofni 32089 | Functionality of composition of projections. (Contributed by NM, 1-Oct-2000.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ((projℎ‘𝐺) ∘ (projℎ‘𝐻)) Fn ℋ | ||
| Theorem | pjss1coi 32090 | Subset relationship for projections. Theorem 4.5(i)<->(iii) of [Beran] p. 112. (Contributed by NM, 1-Oct-2000.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐺 ⊆ 𝐻 ↔ ((projℎ‘𝐻) ∘ (projℎ‘𝐺)) = (projℎ‘𝐺)) | ||
| Theorem | pjss2coi 32091 | Subset relationship for projections. Theorem 4.5(i)<->(ii) of [Beran] p. 112. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐺 ⊆ 𝐻 ↔ ((projℎ‘𝐺) ∘ (projℎ‘𝐻)) = (projℎ‘𝐺)) | ||
| Theorem | pjssmi 32092 | Projection meet property. Remark in [Kalmbach] p. 66. Also Theorem 4.5(i)->(iv) of [Beran] p. 112. (Contributed by NM, 26-Sep-2001.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ ℋ → (𝐻 ⊆ 𝐺 → (((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) = ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴))) | ||
| Theorem | pjssge0i 32093 | Theorem 4.5(iv)->(v) of [Beran] p. 112. (Contributed by NM, 26-Sep-2001.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ ℋ → ((((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) = ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴) → 0 ≤ ((((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) ·ih 𝐴))) | ||
| Theorem | pjdifnormi 32094 | Theorem 4.5(v)<->(vi) of [Beran] p. 112. (Contributed by NM, 26-Sep-2001.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ ℋ → (0 ≤ ((((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) ·ih 𝐴) ↔ (normℎ‘((projℎ‘𝐻)‘𝐴)) ≤ (normℎ‘((projℎ‘𝐺)‘𝐴)))) | ||
| Theorem | pjnormssi 32095* | Theorem 4.5(i)<->(vi) of [Beran] p. 112. (Contributed by NM, 26-Sep-2001.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐺 ⊆ 𝐻 ↔ ∀𝑥 ∈ ℋ (normℎ‘((projℎ‘𝐺)‘𝑥)) ≤ (normℎ‘((projℎ‘𝐻)‘𝑥))) | ||
| Theorem | pjorthcoi 32096 | Composition of projections of orthogonal subspaces. Part (i)->(iia) of Theorem 27.4 of [Halmos] p. 45. (Contributed by NM, 6-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐺 ⊆ (⊥‘𝐻) → ((projℎ‘𝐺) ∘ (projℎ‘𝐻)) = 0hop ) | ||
| Theorem | pjscji 32097 | The projection of orthogonal subspaces is the sum of the projections. (Contributed by NM, 11-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐺 ⊆ (⊥‘𝐻) → (projℎ‘(𝐺 ∨ℋ 𝐻)) = ((projℎ‘𝐺) +op (projℎ‘𝐻))) | ||
| Theorem | pjssumi 32098 | The projection on a subspace sum is the sum of the projections. (Contributed by NM, 11-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐺 ⊆ (⊥‘𝐻) → (projℎ‘(𝐺 +ℋ 𝐻)) = ((projℎ‘𝐺) +op (projℎ‘𝐻))) | ||
| Theorem | pjssposi 32099* | Projector ordering can be expressed by the subset relationship between their projection subspaces. (i)<->(iii) of Theorem 29.2 of [Halmos] p. 48. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (∀𝑥 ∈ ℋ 0 ≤ ((((projℎ‘𝐻) −op (projℎ‘𝐺))‘𝑥) ·ih 𝑥) ↔ 𝐺 ⊆ 𝐻) | ||
| Theorem | pjordi 32100* | The definition of projector ordering in [Halmos] p. 42 is equivalent to the definition of projector ordering in [Beran] p. 110. (We will usually express projector ordering with the even simpler equivalent 𝐺 ⊆ 𝐻; see pjssposi 32099). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (∀𝑥 ∈ ℋ 0 ≤ ((((projℎ‘𝐻) −op (projℎ‘𝐺))‘𝑥) ·ih 𝑥) ↔ ((projℎ‘𝐺) “ ℋ) ⊆ ((projℎ‘𝐻) “ ℋ)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |