Home | Metamath
Proof Explorer Theorem List (p. 290 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lnfn0i 28901 | The value of a linear Hilbert space functional at zero is zero. Remark in [Beran] p. 99. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinFn ⇒ ⊢ (𝑇‘0ℎ) = 0 | ||
Theorem | lnfnaddi 28902 | Additive property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinFn ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 +ℎ 𝐵)) = ((𝑇‘𝐴) + (𝑇‘𝐵))) | ||
Theorem | lnfnmuli 28903 | Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinFn ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 · (𝑇‘𝐵))) | ||
Theorem | lnfnaddmuli 28904 | Sum/product property of a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinFn ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘(𝐵 +ℎ (𝐴 ·ℎ 𝐶))) = ((𝑇‘𝐵) + (𝐴 · (𝑇‘𝐶)))) | ||
Theorem | lnfnsubi 28905 | Subtraction property for a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinFn ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 −ℎ 𝐵)) = ((𝑇‘𝐴) − (𝑇‘𝐵))) | ||
Theorem | lnfn0 28906 | The value of a linear Hilbert space functional at zero is zero. Remark in [Beran] p. 99. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ LinFn → (𝑇‘0ℎ) = 0) | ||
Theorem | lnfnmul 28907 | Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ LinFn ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 · (𝑇‘𝐵))) | ||
Theorem | nmbdfnlbi 28908 | A lower bound for the norm of a bounded linear functional. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ LinFn ∧ (normfn‘𝑇) ∈ ℝ) ⇒ ⊢ (𝐴 ∈ ℋ → (abs‘(𝑇‘𝐴)) ≤ ((normfn‘𝑇) · (normℎ‘𝐴))) | ||
Theorem | nmbdfnlb 28909 | A lower bound for the norm of a bounded linear functional. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ LinFn ∧ (normfn‘𝑇) ∈ ℝ ∧ 𝐴 ∈ ℋ) → (abs‘(𝑇‘𝐴)) ≤ ((normfn‘𝑇) · (normℎ‘𝐴))) | ||
Theorem | nmcfnexi 28910 | The norm of a continuous linear Hilbert space functional exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinFn & ⊢ 𝑇 ∈ ContFn ⇒ ⊢ (normfn‘𝑇) ∈ ℝ | ||
Theorem | nmcfnlbi 28911 | A lower bound for the norm of a continuous linear functional. Theorem 3.5(ii) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinFn & ⊢ 𝑇 ∈ ContFn ⇒ ⊢ (𝐴 ∈ ℋ → (abs‘(𝑇‘𝐴)) ≤ ((normfn‘𝑇) · (normℎ‘𝐴))) | ||
Theorem | nmcfnex 28912 | The norm of a continuous linear Hilbert space functional exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ LinFn ∧ 𝑇 ∈ ContFn) → (normfn‘𝑇) ∈ ℝ) | ||
Theorem | nmcfnlb 28913 | A lower bound of the norm of a continuous linear Hilbert space functional. Theorem 3.5(ii) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ LinFn ∧ 𝑇 ∈ ContFn ∧ 𝐴 ∈ ℋ) → (abs‘(𝑇‘𝐴)) ≤ ((normfn‘𝑇) · (normℎ‘𝐴))) | ||
Theorem | lnfnconi 28914* | A condition equivalent to "𝑇 is continuous" when 𝑇 is linear. Theorem 3.5(iii) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinFn ⇒ ⊢ (𝑇 ∈ ContFn ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (abs‘(𝑇‘𝑦)) ≤ (𝑥 · (normℎ‘𝑦))) | ||
Theorem | lnfncon 28915* | A condition equivalent to "𝑇 is continuous" when 𝑇 is linear. Theorem 3.5(iii) of [Beran] p. 99. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ LinFn → (𝑇 ∈ ContFn ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (abs‘(𝑇‘𝑦)) ≤ (𝑥 · (normℎ‘𝑦)))) | ||
Theorem | lnfncnbd 28916 | A linear functional is continuous iff it is bounded. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ LinFn → (𝑇 ∈ ContFn ↔ (normfn‘𝑇) ∈ ℝ)) | ||
Theorem | imaelshi 28917 | 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 28918 | 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 28919 | 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 28920 | 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 & ⊢ 𝑇 ∈ ContFn ⇒ ⊢ (null‘𝑇) ∈ Cℋ | ||
Theorem | riesz3i 28921* | 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 & ⊢ 𝑇 ∈ ContFn ⇒ ⊢ ∃𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤) | ||
Theorem | riesz4i 28922* | 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 & ⊢ 𝑇 ∈ ContFn ⇒ ⊢ ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤) | ||
Theorem | riesz4 28923* | A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104. See riesz2 28925 for the bounded linear functional version. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ (LinFn ∩ ContFn) → ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤)) | ||
Theorem | riesz1 28924* | 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 28925. For the continuous linear functional version, see riesz3i 28921 and riesz4 28923. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ LinFn → ((normfn‘𝑇) ∈ ℝ ↔ ∃𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦))) | ||
Theorem | riesz2 28925* | 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 28924. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ LinFn ∧ (normfn‘𝑇) ∈ ℝ) → ∃!𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦)) | ||
Theorem | cnlnadjlem1 28926* | Lemma for cnlnadji 28935 (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 & ⊢ 𝑇 ∈ ContOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) ⇒ ⊢ (𝐴 ∈ ℋ → (𝐺‘𝐴) = ((𝑇‘𝐴) ·ih 𝑦)) | ||
Theorem | cnlnadjlem2 28927* | Lemma for cnlnadji 28935. 𝐺 is a continuous linear functional. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ContOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) ⇒ ⊢ (𝑦 ∈ ℋ → (𝐺 ∈ LinFn ∧ 𝐺 ∈ ContFn)) | ||
Theorem | cnlnadjlem3 28928* | Lemma for cnlnadji 28935. By riesz4 28923, 𝐵 is the unique vector such that (𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤) for all 𝑣. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ContOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) & ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) ⇒ ⊢ (𝑦 ∈ ℋ → 𝐵 ∈ ℋ) | ||
Theorem | cnlnadjlem4 28929* | Lemma for cnlnadji 28935. 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 & ⊢ 𝑇 ∈ ContOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) & ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) & ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵) ⇒ ⊢ (𝐴 ∈ ℋ → (𝐹‘𝐴) ∈ ℋ) | ||
Theorem | cnlnadjlem5 28930* | Lemma for cnlnadji 28935. 𝐹 is an adjoint of 𝑇 (later, we will show it is unique). (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ContOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) & ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) & ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵) ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝑇‘𝐶) ·ih 𝐴) = (𝐶 ·ih (𝐹‘𝐴))) | ||
Theorem | cnlnadjlem6 28931* | Lemma for cnlnadji 28935. 𝐹 is linear. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ContOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) & ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) & ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵) ⇒ ⊢ 𝐹 ∈ LinOp | ||
Theorem | cnlnadjlem7 28932* | Lemma for cnlnadji 28935. Helper lemma to show that 𝐹 is continuous. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ContOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) & ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) & ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵) ⇒ ⊢ (𝐴 ∈ ℋ → (normℎ‘(𝐹‘𝐴)) ≤ ((normop‘𝑇) · (normℎ‘𝐴))) | ||
Theorem | cnlnadjlem8 28933* | Lemma for cnlnadji 28935. 𝐹 is continuous. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ContOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) & ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) & ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵) ⇒ ⊢ 𝐹 ∈ ContOp | ||
Theorem | cnlnadjlem9 28934* | Lemma for cnlnadji 28935. 𝐹 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 28935* | 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 28936* | 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 28937* | 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 28938* | 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 28939 | 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 28940 | Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
⊢ BndLinOp ⊆ dom adjℎ | ||
Theorem | bdopadj 28941 | Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ BndLinOp → 𝑇 ∈ dom adjℎ) | ||
Theorem | adjbdln 28942 | 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 28943 | 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 28944 | 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 28945 | 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 28946 | Every operator with an adjoint is linear. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.) |
⊢ dom adjℎ ⊆ LinOp | ||
Theorem | nmopadjlei 28947 | 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 28948 | Lemma for nmopadji 28949. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (normop‘(adjℎ‘𝑇)) ≤ (normop‘𝑇) | ||
Theorem | nmopadji 28949 | 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 28950 | 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 28951 | 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 28952 | 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 28953 | 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 28954 | 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 28955 | 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 28956 | 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 28957 | The composition of two bounded linear operators is bounded. (Contributed by NM, 9-Mar-2006.) (New usage is discouraged.) |
⊢ 𝑆 ∈ BndLinOp & ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (𝑆 ∘ 𝑇) ∈ BndLinOp | ||
Theorem | nmoptri2i 28958 | 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 28959 | 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 28960 | 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 28961 | 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 28962 | 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 28963 | 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 28964 | The norm of the bra function. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (normfn‘(bra‘𝐴)) = (normℎ‘𝐴)) | ||
Theorem | brabn 28965 | The bra of a vector is a bounded functional. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (normfn‘(bra‘𝐴)) ∈ ℝ) | ||
Theorem | rnbra 28966 | 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 28967 | 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 28968 | A bra is a continuous linear functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (bra‘𝐴) ∈ (LinFn ∩ ContFn)) | ||
Theorem | cnvbraval 28969* | Value of the converse of the bra function. Based on the Riesz Lemma riesz4 28923, 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 ∩ ContFn) → (◡bra‘𝑇) = (℩𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦))) | ||
Theorem | cnvbracl 28970 | Closure of the converse of the bra function. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ (LinFn ∩ ContFn) → (◡bra‘𝑇) ∈ ℋ) | ||
Theorem | cnvbrabra 28971 | 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 28972 | 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 28973* | 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 28974 | Multiplication property of the converse bra function. (Contributed by NM, 31-May-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑇 ∈ (LinFn ∩ ContFn)) → (◡bra‘(𝐴 ·fn 𝑇)) = ((∗‘𝐴) ·ℎ (◡bra‘𝑇))) | ||
Theorem | kbass1 28975 | 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 28976 | 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 28977 | Dirac bra-ket associative law 〈𝐴 ∣ 𝐵〉 〈𝐶 ∣ 𝐷〉 = (〈𝐴 ∣ 𝐵〉 〈𝐶 ∣ ) ∣ 𝐷〉. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝐷)) = ((((bra‘𝐴)‘𝐵) ·fn (bra‘𝐶))‘𝐷)) | ||
Theorem | kbass4 28978 | Dirac bra-ket associative law 〈𝐴 ∣ 𝐵〉 〈𝐶 ∣ 𝐷〉 = 〈𝐴 ∣ ( ∣ 𝐵〉 〈𝐶 ∣ 𝐷〉). (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝐷)) = ((bra‘𝐴)‘(((bra‘𝐶)‘𝐷) ·ℎ 𝐵))) | ||
Theorem | kbass5 28979 | Dirac bra-ket associative law ( ∣ 𝐴〉 〈𝐵 ∣ )( ∣ 𝐶〉 〈𝐷 ∣ ) = (( ∣ 𝐴〉 〈𝐵 ∣ ) ∣ 𝐶〉)〈𝐷 ∣. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 ketbra 𝐵) ∘ (𝐶 ketbra 𝐷)) = (((𝐴 ketbra 𝐵)‘𝐶) ketbra 𝐷)) | ||
Theorem | kbass6 28980 | Dirac bra-ket associative law ( ∣ 𝐴〉 〈𝐵 ∣ )( ∣ 𝐶〉 〈𝐷 ∣ ) = ∣ 𝐴〉 (〈𝐵 ∣ ( ∣ 𝐶〉 〈𝐷 ∣ )). (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 ketbra 𝐵) ∘ (𝐶 ketbra 𝐷)) = (𝐴 ketbra (◡bra‘((bra‘𝐵) ∘ (𝐶 ketbra 𝐷))))) | ||
Theorem | leopg 28981* | 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 28982* | 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 28983* | 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 28984 | 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 28985* | 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 28986 | The ordering relation for operators is reflexive. (Contributed by NM, 24-Jul-2006.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ ℋ → 𝑇 ≤op 𝑇) | ||
Theorem | leoprf 28987 | The ordering relation for operators is reflexive. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ HrmOp → 𝑇 ≤op 𝑇) | ||
Theorem | leopsq 28988 | The square of a Hermitian operator is positive. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ HrmOp → 0hop ≤op (𝑇 ∘ 𝑇)) | ||
Theorem | 0leop 28989 | 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 28990 | 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 28991 | 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 28992 | 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 28993 | 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 28994 | 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 28995 | 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 28996 | 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 28997 | 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 28998 | 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 28999* | 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 29000* | 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 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |