Home | Metamath
Proof Explorer Theorem List (p. 284 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | imaelshi 28301 | The image of a subspace under a linear operator is a subspace. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp & ⊢ 𝐴 ∈ Sℋ ⇒ ⊢ (𝑇 “ 𝐴) ∈ Sℋ | ||
Theorem | rnelshi 28302 | The range of a linear operator is a subspace. (Contributed by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ ran 𝑇 ∈ Sℋ | ||
Theorem | nlelshi 28303 | The null space of a linear functional is a subspace. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinFn ⇒ ⊢ (null‘𝑇) ∈ Sℋ | ||
Theorem | nlelchi 28304 | The null space of a continuous linear functional is a closed subspace. Remark 3.8 of [Beran] p. 103. (Contributed by NM, 11-Feb-2006.) (Proof shortened by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinFn & ⊢ 𝑇 ∈ ConFn ⇒ ⊢ (null‘𝑇) ∈ Cℋ | ||
Theorem | riesz3i 28305* | A continuous linear functional can be expressed as an inner product. Existence part of Theorem 3.9 of [Beran] p. 104. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinFn & ⊢ 𝑇 ∈ ConFn ⇒ ⊢ ∃𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤) | ||
Theorem | riesz4i 28306* | A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinFn & ⊢ 𝑇 ∈ ConFn ⇒ ⊢ ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤) | ||
Theorem | riesz4 28307* | A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104. See riesz2 28309 for the bounded linear functional version. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ (LinFn ∩ ConFn) → ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤)) | ||
Theorem | riesz1 28308* | Part 1 of the Riesz representation theorem for bounded linear functionals. A linear functional is bounded iff its value can be expressed as an inner product. Part of Theorem 17.3 of [Halmos] p. 31. For part 2, see riesz2 28309. For the continuous linear functional version, see riesz3i 28305 and riesz4 28307. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ LinFn → ((normfn‘𝑇) ∈ ℝ ↔ ∃𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦))) | ||
Theorem | riesz2 28309* | Part 2 of the Riesz representation theorem for bounded linear functionals. The value of a bounded linear functional corresponds to a unique inner product. Part of Theorem 17.3 of [Halmos] p. 31. For part 1, see riesz1 28308. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ LinFn ∧ (normfn‘𝑇) ∈ ℝ) → ∃!𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦)) | ||
Theorem | cnlnadjlem1 28310* | Lemma for cnlnadji 28319 (Theorem 3.10 of [Beran] p. 104: every continuous linear operator has an adjoint). The value of the auxiliary functional 𝐺. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ConOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) ⇒ ⊢ (𝐴 ∈ ℋ → (𝐺‘𝐴) = ((𝑇‘𝐴) ·ih 𝑦)) | ||
Theorem | cnlnadjlem2 28311* | Lemma for cnlnadji 28319. 𝐺 is a continuous linear functional. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ConOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) ⇒ ⊢ (𝑦 ∈ ℋ → (𝐺 ∈ LinFn ∧ 𝐺 ∈ ConFn)) | ||
Theorem | cnlnadjlem3 28312* | Lemma for cnlnadji 28319. By riesz4 28307, 𝐵 is the unique vector such that (𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤) for all 𝑣. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ConOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) & ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) ⇒ ⊢ (𝑦 ∈ ℋ → 𝐵 ∈ ℋ) | ||
Theorem | cnlnadjlem4 28313* | Lemma for cnlnadji 28319. The values of auxiliary function 𝐹 are vectors. (Contributed by NM, 17-Feb-2006.) (Proof shortened by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ConOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) & ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) & ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵) ⇒ ⊢ (𝐴 ∈ ℋ → (𝐹‘𝐴) ∈ ℋ) | ||
Theorem | cnlnadjlem5 28314* | Lemma for cnlnadji 28319. 𝐹 is an adjoint of 𝑇 (later, we will show it is unique). (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ConOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) & ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) & ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵) ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝑇‘𝐶) ·ih 𝐴) = (𝐶 ·ih (𝐹‘𝐴))) | ||
Theorem | cnlnadjlem6 28315* | Lemma for cnlnadji 28319. 𝐹 is linear. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ConOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) & ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) & ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵) ⇒ ⊢ 𝐹 ∈ LinOp | ||
Theorem | cnlnadjlem7 28316* | Lemma for cnlnadji 28319. Helper lemma to show that 𝐹 is continuous. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ConOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) & ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) & ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵) ⇒ ⊢ (𝐴 ∈ ℋ → (normℎ‘(𝐹‘𝐴)) ≤ ((normop‘𝑇) · (normℎ‘𝐴))) | ||
Theorem | cnlnadjlem8 28317* | Lemma for cnlnadji 28319. 𝐹 is continuous. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ConOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) & ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) & ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵) ⇒ ⊢ 𝐹 ∈ ConOp | ||
Theorem | cnlnadjlem9 28318* | Lemma for cnlnadji 28319. 𝐹 provides an example showing the existence of a continuous linear adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ConOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) & ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) & ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵) ⇒ ⊢ ∃𝑡 ∈ (LinOp ∩ ConOp)∀𝑥 ∈ ℋ ∀𝑧 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑧) = (𝑥 ·ih (𝑡‘𝑧)) | ||
Theorem | cnlnadji 28319* | 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 & ⊢ 𝑇 ∈ ConOp ⇒ ⊢ ∃𝑡 ∈ (LinOp ∩ ConOp)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡‘𝑦)) | ||
Theorem | cnlnadjeui 28320* | 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 & ⊢ 𝑇 ∈ ConOp ⇒ ⊢ ∃!𝑡 ∈ (LinOp ∩ ConOp)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡‘𝑦)) | ||
Theorem | cnlnadjeu 28321* | 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 ∩ ConOp) → ∃!𝑡 ∈ (LinOp ∩ ConOp)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡‘𝑦))) | ||
Theorem | cnlnadj 28322* | 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 ∩ ConOp) → ∃𝑡 ∈ (LinOp ∩ ConOp)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡‘𝑦))) | ||
Theorem | cnlnssadj 28323 | Every continuous linear Hilbert space operator has an adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
⊢ (LinOp ∩ ConOp) ⊆ dom adjℎ | ||
Theorem | bdopssadj 28324 | Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
⊢ BndLinOp ⊆ dom adjℎ | ||
Theorem | bdopadj 28325 | Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ BndLinOp → 𝑇 ∈ dom adjℎ) | ||
Theorem | adjbdln 28326 | 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 28327 | 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 28328 | 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 28329 | 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 28330 | Every operator with an adjoint is linear. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.) |
⊢ dom adjℎ ⊆ LinOp | ||
Theorem | nmopadjlei 28331 | 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 28332 | Lemma for nmopadji 28333. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (normop‘(adjℎ‘𝑇)) ≤ (normop‘𝑇) | ||
Theorem | nmopadji 28333 | 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 28334 | 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 28335 | 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 28336 | 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 28337 | 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 28338 | 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 28339 | 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 28340 | 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 28341 | The composition of two bounded linear operators is bounded. (Contributed by NM, 9-Mar-2006.) (New usage is discouraged.) |
⊢ 𝑆 ∈ BndLinOp & ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (𝑆 ∘ 𝑇) ∈ BndLinOp | ||
Theorem | nmoptri2i 28342 | 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 28343 | 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 28344 | 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 28345 | 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 28346 | 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 28347 | 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 28348 | The norm of the bra function. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (normfn‘(bra‘𝐴)) = (normℎ‘𝐴)) | ||
Theorem | brabn 28349 | The bra of a vector is a bounded functional. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (normfn‘(bra‘𝐴)) ∈ ℝ) | ||
Theorem | rnbra 28350 | The set of bras equals the set of continuous linear functionals. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
⊢ ran bra = (LinFn ∩ ConFn) | ||
Theorem | bra11 28351 | 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 ∩ ConFn) | ||
Theorem | bracnln 28352 | A bra is a continuous linear functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (bra‘𝐴) ∈ (LinFn ∩ ConFn)) | ||
Theorem | cnvbraval 28353* | Value of the converse of the bra function. Based on the Riesz Lemma riesz4 28307, this very important theorem not only justifies the Dirac bra-ket notation, but allows us 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 ∩ ConFn) → (◡bra‘𝑇) = (℩𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦))) | ||
Theorem | cnvbracl 28354 | Closure of the converse of the bra function. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ (LinFn ∩ ConFn) → (◡bra‘𝑇) ∈ ℋ) | ||
Theorem | cnvbrabra 28355 | 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 28356 | The bra of the converse bra of a continuous linear functional. (Contributed by NM, 31-May-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ (LinFn ∩ ConFn) → (bra‘(◡bra‘𝑇)) = 𝑇) | ||
Theorem | bracnlnval 28357* | The vector that a continuous linear functional is the bra of. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ (LinFn ∩ ConFn) → 𝑇 = (bra‘(℩𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦)))) | ||
Theorem | cnvbramul 28358 | Multiplication property of the converse bra function. (Contributed by NM, 31-May-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑇 ∈ (LinFn ∩ ConFn)) → (◡bra‘(𝐴 ·fn 𝑇)) = ((∗‘𝐴) ·ℎ (◡bra‘𝑇))) | ||
Theorem | kbass1 28359 | 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 28360 | 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 28361 | Dirac bra-ket associative law 〈𝐴 ∣ 𝐵〉 〈𝐶 ∣ 𝐷〉 = (〈𝐴 ∣ 𝐵〉 〈𝐶 ∣ ) ∣ 𝐷〉. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝐷)) = ((((bra‘𝐴)‘𝐵) ·fn (bra‘𝐶))‘𝐷)) | ||
Theorem | kbass4 28362 | Dirac bra-ket associative law 〈𝐴 ∣ 𝐵〉 〈𝐶 ∣ 𝐷〉 = 〈𝐴 ∣ ( ∣ 𝐵〉 〈𝐶 ∣ 𝐷〉). (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝐷)) = ((bra‘𝐴)‘(((bra‘𝐶)‘𝐷) ·ℎ 𝐵))) | ||
Theorem | kbass5 28363 | Dirac bra-ket associative law ( ∣ 𝐴〉 〈𝐵 ∣ )( ∣ 𝐶〉 〈𝐷 ∣ ) = (( ∣ 𝐴〉 〈𝐵 ∣ ) ∣ 𝐶〉)〈𝐷 ∣. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 ketbra 𝐵) ∘ (𝐶 ketbra 𝐷)) = (((𝐴 ketbra 𝐵)‘𝐶) ketbra 𝐷)) | ||
Theorem | kbass6 28364 | Dirac bra-ket associative law ( ∣ 𝐴〉 〈𝐵 ∣ )( ∣ 𝐶〉 〈𝐷 ∣ ) = ∣ 𝐴〉 (〈𝐵 ∣ ( ∣ 𝐶〉 〈𝐷 ∣ )). (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 ketbra 𝐵) ∘ (𝐶 ketbra 𝐷)) = (𝐴 ketbra (◡bra‘((bra‘𝐵) ∘ (𝐶 ketbra 𝐷))))) | ||
Theorem | leopg 28365* | 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 28366* | 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 28367* | 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 28368 | 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 28369* | 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 28370 | The ordering relation for operators is reflexive. (Contributed by NM, 24-Jul-2006.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ ℋ → 𝑇 ≤op 𝑇) | ||
Theorem | leoprf 28371 | The ordering relation for operators is reflexive. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ HrmOp → 𝑇 ≤op 𝑇) | ||
Theorem | leopsq 28372 | The square of a Hermitian operator is positive. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ HrmOp → 0hop ≤op (𝑇 ∘ 𝑇)) | ||
Theorem | 0leop 28373 | 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 28374 | 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 28375 | 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 28376 | 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 28377 | 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 28378 | 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 28379 | 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 28380 | 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 28381 | 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 28382 | 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 28383* | 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 28384* | 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 28385* | 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 28386* | 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 28387* | 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 28388* | 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 28389 | A projector is a Hermitian operator. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (projℎ‘𝐻) ∈ HrmOp | ||
Theorem | pjlnopi 28390 | A projector is a linear operator. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (projℎ‘𝐻) ∈ LinOp | ||
Theorem | pjnmopi 28391 | 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 28392 | A projector is a bounded linear operator. (Contributed by NM, 3-Jun-2006.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (projℎ‘𝐻) ∈ BndLinOp | ||
Theorem | pjhmop 28393 | A projection is a Hermitian operator. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
⊢ (𝐻 ∈ Cℋ → (projℎ‘𝐻) ∈ HrmOp) | ||
Theorem | hmopidmchi 28394 | 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 28395 | 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 28394 shows.) (Contributed by NM, 22-Apr-2006.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
⊢ 𝑇 ∈ HrmOp & ⊢ (𝑇 ∘ 𝑇) = 𝑇 ⇒ ⊢ 𝑇 = (projℎ‘ran 𝑇) | ||
Theorem | hmopidmch 28396 | 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 28397 | 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 28398 | 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 28399 | 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 28400 | 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ℎ‘𝐻) ∘ 𝑅) ∘ 𝑇))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |