Home | Metamath
Proof Explorer Theorem List (p. 299 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 | bdophsi 29801 | 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 29802 | 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 29803 | The composition of two bounded linear operators is bounded. (Contributed by NM, 9-Mar-2006.) (New usage is discouraged.) |
⊢ 𝑆 ∈ BndLinOp & ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (𝑆 ∘ 𝑇) ∈ BndLinOp | ||
Theorem | nmoptri2i 29804 | 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 29805 | 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 29806 | 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 29807 | 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 29808 | 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 29809 | 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 29810 | The norm of the bra function. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (normfn‘(bra‘𝐴)) = (normℎ‘𝐴)) | ||
Theorem | brabn 29811 | The bra of a vector is a bounded functional. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (normfn‘(bra‘𝐴)) ∈ ℝ) | ||
Theorem | rnbra 29812 | 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 29813 | 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 29814 | A bra is a continuous linear functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (bra‘𝐴) ∈ (LinFn ∩ ContFn)) | ||
Theorem | cnvbraval 29815* | Value of the converse of the bra function. Based on the Riesz Lemma riesz4 29769, 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 29816 | Closure of the converse of the bra function. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ (LinFn ∩ ContFn) → (◡bra‘𝑇) ∈ ℋ) | ||
Theorem | cnvbrabra 29817 | 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 29818 | 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 29819* | 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 29820 | Multiplication property of the converse bra function. (Contributed by NM, 31-May-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑇 ∈ (LinFn ∩ ContFn)) → (◡bra‘(𝐴 ·fn 𝑇)) = ((∗‘𝐴) ·ℎ (◡bra‘𝑇))) | ||
Theorem | kbass1 29821 | 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 29822 | 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 29823 | Dirac bra-ket associative law 〈𝐴 ∣ 𝐵〉 〈𝐶 ∣ 𝐷〉 = (〈𝐴 ∣ 𝐵〉 〈𝐶 ∣ ) ∣ 𝐷〉. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝐷)) = ((((bra‘𝐴)‘𝐵) ·fn (bra‘𝐶))‘𝐷)) | ||
Theorem | kbass4 29824 | Dirac bra-ket associative law 〈𝐴 ∣ 𝐵〉 〈𝐶 ∣ 𝐷〉 = 〈𝐴 ∣ ( ∣ 𝐵〉 〈𝐶 ∣ 𝐷〉). (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝐷)) = ((bra‘𝐴)‘(((bra‘𝐶)‘𝐷) ·ℎ 𝐵))) | ||
Theorem | kbass5 29825 | Dirac bra-ket associative law ( ∣ 𝐴〉 〈𝐵 ∣ )( ∣ 𝐶〉 〈𝐷 ∣ ) = (( ∣ 𝐴〉 〈𝐵 ∣ ) ∣ 𝐶〉)〈𝐷 ∣. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 ketbra 𝐵) ∘ (𝐶 ketbra 𝐷)) = (((𝐴 ketbra 𝐵)‘𝐶) ketbra 𝐷)) | ||
Theorem | kbass6 29826 | Dirac bra-ket associative law ( ∣ 𝐴〉 〈𝐵 ∣ )( ∣ 𝐶〉 〈𝐷 ∣ ) = ∣ 𝐴〉 (〈𝐵 ∣ ( ∣ 𝐶〉 〈𝐷 ∣ )). (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 ketbra 𝐵) ∘ (𝐶 ketbra 𝐷)) = (𝐴 ketbra (◡bra‘((bra‘𝐵) ∘ (𝐶 ketbra 𝐷))))) | ||
Theorem | leopg 29827* | 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 29828* | 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 29829* | 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 29830 | 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 29831* | 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 29832 | The ordering relation for operators is reflexive. (Contributed by NM, 24-Jul-2006.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ ℋ → 𝑇 ≤op 𝑇) | ||
Theorem | leoprf 29833 | The ordering relation for operators is reflexive. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ HrmOp → 𝑇 ≤op 𝑇) | ||
Theorem | leopsq 29834 | The square of a Hermitian operator is positive. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ HrmOp → 0hop ≤op (𝑇 ∘ 𝑇)) | ||
Theorem | 0leop 29835 | 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 29836 | 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 29837 | 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 29838 | 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 29839 | 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 29840 | 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 29841 | 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 29842 | 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 29843 | 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 29844 | 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 29845* | 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 29846* | 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 29847* | 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 29848* | 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 29849* | 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 29850* | 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 29851 | A projector is a Hermitian operator. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (projℎ‘𝐻) ∈ HrmOp | ||
Theorem | pjlnopi 29852 | A projector is a linear operator. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (projℎ‘𝐻) ∈ LinOp | ||
Theorem | pjnmopi 29853 | 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 29854 | A projector is a bounded linear operator. (Contributed by NM, 3-Jun-2006.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (projℎ‘𝐻) ∈ BndLinOp | ||
Theorem | pjhmop 29855 | A projection is a Hermitian operator. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
⊢ (𝐻 ∈ Cℋ → (projℎ‘𝐻) ∈ HrmOp) | ||
Theorem | hmopidmchi 29856 | 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 29857 | 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 29856 shows.) (Contributed by NM, 22-Apr-2006.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
⊢ 𝑇 ∈ HrmOp & ⊢ (𝑇 ∘ 𝑇) = 𝑇 ⇒ ⊢ 𝑇 = (projℎ‘ran 𝑇) | ||
Theorem | hmopidmch 29858 | 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 29859 | 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 29860 | 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 29861 | 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 29862 | 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 29863 | Composition of projections. (Contributed by NM, 16-Aug-2000.) (New usage is discouraged.) |
⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ ℋ → (((projℎ‘𝐺) ∘ (projℎ‘𝐻))‘𝐴) = ((projℎ‘𝐺)‘((projℎ‘𝐻)‘𝐴))) | ||
Theorem | pjcocli 29864 | Closure of composition of projections. (Contributed by NM, 29-Nov-2000.) (New usage is discouraged.) |
⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ ℋ → (((projℎ‘𝐺) ∘ (projℎ‘𝐻))‘𝐴) ∈ 𝐺) | ||
Theorem | pjcohcli 29865 | Closure of composition of projections. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.) |
⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ ℋ → (((projℎ‘𝐺) ∘ (projℎ‘𝐻))‘𝐴) ∈ ℋ) | ||
Theorem | pjadjcoi 29866 | 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 29867 | Functionality of composition of projections. (Contributed by NM, 1-Oct-2000.) (New usage is discouraged.) |
⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ((projℎ‘𝐺) ∘ (projℎ‘𝐻)) Fn ℋ | ||
Theorem | pjss1coi 29868 | 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 29869 | 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 29870 | 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 29871 | 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 29872 | 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 29873* | 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 29874 | 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 29875 | 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 29876 | 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 29877* | 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 29878* | 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 29877). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (∀𝑥 ∈ ℋ 0 ≤ ((((projℎ‘𝐻) −op (projℎ‘𝐺))‘𝑥) ·ih 𝑥) ↔ ((projℎ‘𝐺) “ ℋ) ⊆ ((projℎ‘𝐻) “ ℋ)) | ||
Theorem | pjssdif2i 29879 | The projection subspace of the difference between two projectors. Part 2 of Theorem 29.3 of [Halmos] p. 48 (shortened with pjssposi 29877). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐺 ⊆ 𝐻 ↔ ((projℎ‘𝐻) −op (projℎ‘𝐺)) = (projℎ‘(𝐻 ∩ (⊥‘𝐺)))) | ||
Theorem | pjssdif1i 29880 | A necessary and sufficient condition for the difference between two projectors to be a projector. Part 1 of Theorem 29.3 of [Halmos] p. 48 (shortened with pjssposi 29877). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐺 ⊆ 𝐻 ↔ ((projℎ‘𝐻) −op (projℎ‘𝐺)) ∈ ran projℎ) | ||
Theorem | pjimai 29881 | The image of a projection. Lemma 5 in Daniel Lehmann, "A presentation of Quantum Logic based on an and then connective" http://www.arxiv.org/pdf/quant-ph/0701113 p. 20. (Contributed by NM, 20-Jan-2007.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ ((projℎ‘𝐵) “ 𝐴) = ((𝐴 +ℋ (⊥‘𝐵)) ∩ 𝐵) | ||
Theorem | pjidmcoi 29882 | A projection is idempotent. Property (ii) of [Beran] p. 109. (Contributed by NM, 1-Oct-2000.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ((projℎ‘𝐻) ∘ (projℎ‘𝐻)) = (projℎ‘𝐻) | ||
Theorem | pjoccoi 29883 | Composition of projections of a subspace and its orthocomplement. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ((projℎ‘𝐻) ∘ (projℎ‘(⊥‘𝐻))) = 0hop | ||
Theorem | pjtoi 29884 | Subspace sum of projection and projection of orthocomplement. (Contributed by NM, 16-Nov-2000.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ((projℎ‘𝐻) +op (projℎ‘(⊥‘𝐻))) = (projℎ‘ ℋ) | ||
Theorem | pjoci 29885 | Projection of orthocomplement. First part of Theorem 27.3 of [Halmos] p. 45. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ((projℎ‘ ℋ) −op (projℎ‘𝐻)) = (projℎ‘(⊥‘𝐻)) | ||
Theorem | pjidmco 29886 | A projection operator is idempotent. Property (ii) of [Beran] p. 109. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
⊢ (𝐻 ∈ Cℋ → ((projℎ‘𝐻) ∘ (projℎ‘𝐻)) = (projℎ‘𝐻)) | ||
Theorem | dfpjop 29887 | Definition of projection operator in [Hughes] p. 47, except that we do not need linearity to be explicit by virtue of hmoplin 29647. (Contributed by NM, 24-Apr-2006.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
⊢ (𝑇 ∈ ran projℎ ↔ (𝑇 ∈ HrmOp ∧ (𝑇 ∘ 𝑇) = 𝑇)) | ||
Theorem | pjhmopidm 29888 | Two ways to express the set of all projection operators. (Contributed by NM, 24-Apr-2006.) (Proof shortened by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
⊢ ran projℎ = {𝑡 ∈ HrmOp ∣ (𝑡 ∘ 𝑡) = 𝑡} | ||
Theorem | elpjidm 29889 | A projection operator is idempotent. Part of Theorem 26.1 of [Halmos] p. 43. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ ran projℎ → (𝑇 ∘ 𝑇) = 𝑇) | ||
Theorem | elpjhmop 29890 | A projection operator is Hermitian. Part of Theorem 26.1 of [Halmos] p. 43. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ ran projℎ → 𝑇 ∈ HrmOp) | ||
Theorem | 0leopj 29891 | A projector is a positive operator. (Contributed by NM, 27-Sep-2008.) (New usage is discouraged.) |
⊢ (𝑇 ∈ ran projℎ → 0hop ≤op 𝑇) | ||
Theorem | pjadj2 29892 | A projector is self-adjoint. Property (i) of [Beran] p. 109. (Contributed by NM, 3-Jun-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ ran projℎ → (adjℎ‘𝑇) = 𝑇) | ||
Theorem | pjadj3 29893 | A projector is self-adjoint. Property (i) of [Beran] p. 109. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
⊢ (𝐻 ∈ Cℋ → (adjℎ‘(projℎ‘𝐻)) = (projℎ‘𝐻)) | ||
Theorem | elpjch 29894 | Reconstruction of the subspace of a projection operator. Part of Theorem 26.2 of [Halmos] p. 44. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ ran projℎ → (ran 𝑇 ∈ Cℋ ∧ 𝑇 = (projℎ‘ran 𝑇))) | ||
Theorem | elpjrn 29895* | Reconstruction of the subspace of a projection operator. (Contributed by NM, 24-Apr-2006.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
⊢ (𝑇 ∈ ran projℎ → ran 𝑇 = {𝑥 ∈ ℋ ∣ (𝑇‘𝑥) = 𝑥}) | ||
Theorem | pjinvari 29896 | A closed subspace 𝐻 with projection 𝑇 is invariant under an operator 𝑆 iff 𝑆𝑇 = 𝑇𝑆𝑇. Theorem 27.1 of [Halmos] p. 45. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝐻 ∈ Cℋ & ⊢ 𝑇 = (projℎ‘𝐻) ⇒ ⊢ ((𝑆 ∘ 𝑇): ℋ⟶𝐻 ↔ (𝑆 ∘ 𝑇) = (𝑇 ∘ (𝑆 ∘ 𝑇))) | ||
Theorem | pjin1i 29897 | Lemma for Theorem 1.22 of Mittelstaedt, p. 20. (Contributed by NM, 22-Apr-2001.) (New usage is discouraged.) |
⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (projℎ‘(𝐺 ∩ 𝐻)) = ((projℎ‘𝐺) ∘ (projℎ‘(𝐺 ∩ 𝐻))) | ||
Theorem | pjin2i 29898 | Lemma for Theorem 1.22 of Mittelstaedt, p. 20. (Contributed by NM, 22-Apr-2001.) (New usage is discouraged.) |
⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (((projℎ‘𝐺) = ((projℎ‘𝐺) ∘ (projℎ‘𝐻)) ∧ (projℎ‘𝐻) = ((projℎ‘𝐻) ∘ (projℎ‘𝐺))) ↔ (projℎ‘𝐺) = (projℎ‘𝐻)) | ||
Theorem | pjin3i 29899 | Lemma for Theorem 1.22 of Mittelstaedt, p. 20. (Contributed by NM, 22-Apr-2001.) (New usage is discouraged.) |
⊢ 𝐹 ∈ Cℋ & ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (((projℎ‘𝐹) = ((projℎ‘𝐹) ∘ (projℎ‘𝐺)) ∧ (projℎ‘𝐹) = ((projℎ‘𝐹) ∘ (projℎ‘𝐻))) ↔ (projℎ‘𝐹) = ((projℎ‘𝐹) ∘ (projℎ‘(𝐺 ∩ 𝐻)))) | ||
Theorem | pjclem1 29900 | Lemma for projection commutation theorem. (Contributed by NM, 16-Nov-2000.) (New usage is discouraged.) |
⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐺 𝐶ℋ 𝐻 → ((projℎ‘𝐺) ∘ (projℎ‘𝐻)) = (projℎ‘(𝐺 ∩ 𝐻))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |