Home | Metamath
Proof Explorer Theorem List (p. 296 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 | honegsubi 29501 | Relationship between Hilbert operator addition and subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 +op (-1 ·op 𝑇)) = (𝑆 −op 𝑇) | ||
Theorem | ho0sub 29502 | Subtraction of Hilbert space operators expressed in terms of difference from zero. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆 −op 𝑇) = (𝑆 +op ( 0hop −op 𝑇))) | ||
Theorem | hosubid1 29503 | The zero operator subtracted from a Hilbert space operator. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ ℋ → (𝑇 −op 0hop ) = 𝑇) | ||
Theorem | honegsub 29504 | Relationship between Hilbert space operator addition and subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 +op (-1 ·op 𝑈)) = (𝑇 −op 𝑈)) | ||
Theorem | homulid2 29505 | An operator equals its scalar product with one. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ ℋ → (1 ·op 𝑇) = 𝑇) | ||
Theorem | homco1 29506 | Associative law for scalar product and composition of operators. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝐴 ·op 𝑇) ∘ 𝑈) = (𝐴 ·op (𝑇 ∘ 𝑈))) | ||
Theorem | homulass 29507 | Scalar product associative law for Hilbert space operators. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → ((𝐴 · 𝐵) ·op 𝑇) = (𝐴 ·op (𝐵 ·op 𝑇))) | ||
Theorem | hoadddi 29508 | Scalar product distributive law for Hilbert space operators. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝐴 ·op (𝑇 +op 𝑈)) = ((𝐴 ·op 𝑇) +op (𝐴 ·op 𝑈))) | ||
Theorem | hoadddir 29509 | Scalar product reverse distributive law for Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → ((𝐴 + 𝐵) ·op 𝑇) = ((𝐴 ·op 𝑇) +op (𝐵 ·op 𝑇))) | ||
Theorem | homul12 29510 | Swap first and second factors in a nested operator scalar product. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → (𝐴 ·op (𝐵 ·op 𝑇)) = (𝐵 ·op (𝐴 ·op 𝑇))) | ||
Theorem | honegneg 29511 | Double negative of a Hilbert space operator. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ ℋ → (-1 ·op (-1 ·op 𝑇)) = 𝑇) | ||
Theorem | hosubneg 29512 | Relationship between operator subtraction and negative. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 −op (-1 ·op 𝑈)) = (𝑇 +op 𝑈)) | ||
Theorem | hosubdi 29513 | Scalar product distributive law for operator difference. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝐴 ·op (𝑇 −op 𝑈)) = ((𝐴 ·op 𝑇) −op (𝐴 ·op 𝑈))) | ||
Theorem | honegdi 29514 | Distribution of negative over addition. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (-1 ·op (𝑇 +op 𝑈)) = ((-1 ·op 𝑇) +op (-1 ·op 𝑈))) | ||
Theorem | honegsubdi 29515 | Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (-1 ·op (𝑇 −op 𝑈)) = ((-1 ·op 𝑇) +op 𝑈)) | ||
Theorem | honegsubdi2 29516 | Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (-1 ·op (𝑇 −op 𝑈)) = (𝑈 −op 𝑇)) | ||
Theorem | hosubsub2 29517 | Law for double subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑆 −op (𝑇 −op 𝑈)) = (𝑆 +op (𝑈 −op 𝑇))) | ||
Theorem | hosub4 29518 | Rearrangement of 4 terms in a mixed addition and subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
⊢ (((𝑅: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ) ∧ (𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ)) → ((𝑅 +op 𝑆) −op (𝑇 +op 𝑈)) = ((𝑅 −op 𝑇) +op (𝑆 −op 𝑈))) | ||
Theorem | hosubadd4 29519 | Rearrangement of 4 terms in a mixed addition and subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
⊢ (((𝑅: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ) ∧ (𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ)) → ((𝑅 −op 𝑆) −op (𝑇 −op 𝑈)) = ((𝑅 +op 𝑈) −op (𝑆 +op 𝑇))) | ||
Theorem | hoaddsubass 29520 | Associative-type law for addition and subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝑆 +op 𝑇) −op 𝑈) = (𝑆 +op (𝑇 −op 𝑈))) | ||
Theorem | hoaddsub 29521 | Law for operator addition and subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝑆 +op 𝑇) −op 𝑈) = ((𝑆 −op 𝑈) +op 𝑇)) | ||
Theorem | hosubsub 29522 | Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑆 −op (𝑇 −op 𝑈)) = ((𝑆 −op 𝑇) +op 𝑈)) | ||
Theorem | hosubsub4 29523 | Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝑆 −op 𝑇) −op 𝑈) = (𝑆 −op (𝑇 +op 𝑈))) | ||
Theorem | ho2times 29524 | Two times a Hilbert space operator. (Contributed by NM, 26-Aug-2006.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ ℋ → (2 ·op 𝑇) = (𝑇 +op 𝑇)) | ||
Theorem | hoaddsubassi 29525 | Associativity of sum and difference of Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 +op 𝑆) −op 𝑇) = (𝑅 +op (𝑆 −op 𝑇)) | ||
Theorem | hoaddsubi 29526 | Law for sum and difference of Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 +op 𝑆) −op 𝑇) = ((𝑅 −op 𝑇) +op 𝑆) | ||
Theorem | hosd1i 29527 | Hilbert space operator sum expressed in terms of difference. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
⊢ 𝑇: ℋ⟶ ℋ & ⊢ 𝑈: ℋ⟶ ℋ ⇒ ⊢ (𝑇 +op 𝑈) = (𝑇 −op ( 0hop −op 𝑈)) | ||
Theorem | hosd2i 29528 | Hilbert space operator sum expressed in terms of difference. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
⊢ 𝑇: ℋ⟶ ℋ & ⊢ 𝑈: ℋ⟶ ℋ ⇒ ⊢ (𝑇 +op 𝑈) = (𝑇 −op ((𝑈 −op 𝑈) −op 𝑈)) | ||
Theorem | hopncani 29529 | Hilbert space operator cancellation law. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
⊢ 𝑇: ℋ⟶ ℋ & ⊢ 𝑈: ℋ⟶ ℋ ⇒ ⊢ ((𝑇 +op 𝑈) −op 𝑈) = 𝑇 | ||
Theorem | honpcani 29530 | Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
⊢ 𝑇: ℋ⟶ ℋ & ⊢ 𝑈: ℋ⟶ ℋ ⇒ ⊢ ((𝑇 −op 𝑈) +op 𝑈) = 𝑇 | ||
Theorem | hosubeq0i 29531 | If the difference between two operators is zero, they are equal. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.) |
⊢ 𝑇: ℋ⟶ ℋ & ⊢ 𝑈: ℋ⟶ ℋ ⇒ ⊢ ((𝑇 −op 𝑈) = 0hop ↔ 𝑇 = 𝑈) | ||
Theorem | honpncani 29532 | Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 −op 𝑆) +op (𝑆 −op 𝑇)) = (𝑅 −op 𝑇) | ||
Theorem | ho01i 29533* | A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S8) of [Beran] p. 95. (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.) |
⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = 0 ↔ 𝑇 = 0hop ) | ||
Theorem | ho02i 29534* | A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S10) of [Beran] p. 95. (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.) |
⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = 0 ↔ 𝑇 = 0hop ) | ||
Theorem | hoeq1 29535* | A condition implying that two Hilbert space operators are equal. Lemma 3.2(S9) of [Beran] p. 95. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑆‘𝑥) ·ih 𝑦) = ((𝑇‘𝑥) ·ih 𝑦) ↔ 𝑆 = 𝑇)) | ||
Theorem | hoeq2 29536* | A condition implying that two Hilbert space operators are equal. Lemma 3.2(S11) of [Beran] p. 95. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑆‘𝑦)) = (𝑥 ·ih (𝑇‘𝑦)) ↔ 𝑆 = 𝑇)) | ||
Theorem | adjmo 29537* | Every Hilbert space operator has at most one adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
⊢ ∃*𝑢(𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦)) | ||
Theorem | adjsym 29538* | Symmetry property of an adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦))) | ||
Theorem | eigrei 29539 | A necessary and sufficient condition (that holds when 𝑇 is a Hermitian operator) for an eigenvalue 𝐵 to be real. Generalization of Equation 1.30 of [Hughes] p. 49. (Contributed by NM, 21-Jan-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ) → ((𝐴 ·ih (𝑇‘𝐴)) = ((𝑇‘𝐴) ·ih 𝐴) ↔ 𝐵 ∈ ℝ)) | ||
Theorem | eigre 29540 | A necessary and sufficient condition (that holds when 𝑇 is a Hermitian operator) for an eigenvalue 𝐵 to be real. Generalization of Equation 1.30 of [Hughes] p. 49. (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → ((𝐴 ·ih (𝑇‘𝐴)) = ((𝑇‘𝐴) ·ih 𝐴) ↔ 𝐵 ∈ ℝ)) | ||
Theorem | eigposi 29541 | A sufficient condition (first conjunct pair, that holds when 𝑇 is a positive operator) for an eigenvalue 𝐵 (second conjunct pair) to be nonnegative. Remark (ii) in [Hughes] p. 137. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((((𝐴 ·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴 ·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) | ||
Theorem | eigorthi 29542 | A necessary and sufficient condition (that holds when 𝑇 is a Hermitian operator) for two eigenvectors 𝐴 and 𝐵 to be orthogonal. Generalization of Equation 1.31 of [Hughes] p. 49. (Contributed by NM, 23-Jan-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈ ℂ ⇒ ⊢ ((((𝑇‘𝐴) = (𝐶 ·ℎ 𝐴) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ∧ 𝐶 ≠ (∗‘𝐷)) → ((𝐴 ·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵) ↔ (𝐴 ·ih 𝐵) = 0)) | ||
Theorem | eigorth 29543 | A necessary and sufficient condition (that holds when 𝑇 is a Hermitian operator) for two eigenvectors 𝐴 and 𝐵 to be orthogonal. Generalization of Equation 1.31 of [Hughes] p. 49. (Contributed by NM, 23-Mar-2006.) (New usage is discouraged.) |
⊢ ((((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) ∧ (((𝑇‘𝐴) = (𝐶 ·ℎ 𝐴) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ∧ 𝐶 ≠ (∗‘𝐷))) → ((𝐴 ·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵) ↔ (𝐴 ·ih 𝐵) = 0)) | ||
Definition | df-nmop 29544* | Define the norm of a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
⊢ normop = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑡‘𝑧)))}, ℝ*, < )) | ||
Definition | df-cnop 29545* | Define the set of continuous operators on Hilbert space. For every "epsilon" (𝑦) there is a "delta" (𝑧) such that... (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.) |
⊢ ContOp = {𝑡 ∈ ( ℋ ↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦)} | ||
Definition | df-lnop 29546* | Define the set of linear operators on Hilbert space. (See df-hosum 29435 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
⊢ LinOp = {𝑡 ∈ ( ℋ ↑m ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑡‘𝑦)) +ℎ (𝑡‘𝑧))} | ||
Definition | df-bdop 29547 | Define the set of bounded linear Hilbert space operators. (See df-hosum 29435 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
⊢ BndLinOp = {𝑡 ∈ LinOp ∣ (normop‘𝑡) < +∞} | ||
Definition | df-unop 29548* | Define the set of unitary operators on Hilbert space. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
⊢ UniOp = {𝑡 ∣ (𝑡: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡‘𝑥) ·ih (𝑡‘𝑦)) = (𝑥 ·ih 𝑦))} | ||
Definition | df-hmop 29549* | Define the set of Hermitian operators on Hilbert space. Some books call these "symmetric operators" and others call them "self-adjoint operators", sometimes with slightly different technical meanings. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
⊢ HrmOp = {𝑡 ∈ ( ℋ ↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦)} | ||
Definition | df-nmfn 29550* | Define the norm of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
⊢ normfn = (𝑡 ∈ (ℂ ↑m ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (abs‘(𝑡‘𝑧)))}, ℝ*, < )) | ||
Definition | df-nlfn 29551 | Define the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
⊢ null = (𝑡 ∈ (ℂ ↑m ℋ) ↦ (◡𝑡 “ {0})) | ||
Definition | df-cnfn 29552* | Define the set of continuous functionals on Hilbert space. For every "epsilon" (𝑦) there is a "delta" (𝑧) such that... (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
⊢ ContFn = {𝑡 ∈ (ℂ ↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (abs‘((𝑡‘𝑤) − (𝑡‘𝑥))) < 𝑦)} | ||
Definition | df-lnfn 29553* | Define the set of linear functionals on Hilbert space. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
⊢ LinFn = {𝑡 ∈ (ℂ ↑m ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))} | ||
Definition | df-adjh 29554* | Define the adjoint of a Hilbert space operator (if it exists). The domain of adjℎ is the set of all adjoint operators. Definition of adjoint in [Kalmbach2] p. 8. Unlike Kalmbach (and most authors), we do not demand that the operator be linear, but instead show (in adjbdln 29788) that the adjoint exists for a bounded linear operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
⊢ adjℎ = {〈𝑡, 𝑢〉 ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢‘𝑦)))} | ||
Definition | df-bra 29555* |
Define the bra of a vector used by Dirac notation. Based on definition
of bra in [Prugovecki] p. 186 (p.
180 in 1971 edition). In Dirac
bra-ket notation, 〈𝐴 ∣ 𝐵〉 is a complex number equal to
the inner
product (𝐵 ·ih 𝐴). But physicists like
to talk about the
individual components 〈𝐴 ∣ and ∣
𝐵〉, called bra
and ket
respectively. In order for their properties to make sense formally, we
define the ket ∣ 𝐵〉 as the vector 𝐵 itself,
and the bra
〈𝐴 ∣ as a functional from ℋ to ℂ. We represent the
Dirac notation 〈𝐴 ∣ 𝐵〉 by ((bra‘𝐴)‘𝐵); see
braval 29649. The reversal of the inner product
arguments not only makes
the bra-ket behavior consistent with physics literature (see comments
under ax-his3 28789) but is also required in order for the
associative law
kbass2 29822 to work.
Our definition of bra and the associated outer product df-kb 29556 differs from, but is equivalent to, a common approach in the literature that makes use of mappings to a dual space. Our approach eliminates the need to have a parallel development of this dual space and instead keeps everything in Hilbert space. For an extensive discussion about how our notation maps to the bra-ket notation in physics textbooks, see mmnotes.txt 29556, under the 17-May-2006 entry. (Contributed by NM, 15-May-2006.) (New usage is discouraged.) |
⊢ bra = (𝑥 ∈ ℋ ↦ (𝑦 ∈ ℋ ↦ (𝑦 ·ih 𝑥))) | ||
Definition | df-kb 29556* | Define a commuted bra and ket juxtaposition used by Dirac notation. In Dirac notation, ∣ 𝐴〉 〈𝐵 ∣ is an operator known as the outer product of 𝐴 and 𝐵, which we represent by (𝐴 ketbra 𝐵). Based on Equation 8.1 of [Prugovecki] p. 376. This definition, combined with definition df-bra 29555, allows any legal juxtaposition of bras and kets to make sense formally and also to obey the associative law when mapped back to Dirac notation. (Contributed by NM, 15-May-2006.) (New usage is discouraged.) |
⊢ ketbra = (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑧 ∈ ℋ ↦ ((𝑧 ·ih 𝑦) ·ℎ 𝑥))) | ||
Definition | df-leop 29557* | Define positive operator ordering. Definition VI.1 of [Retherford] p. 49. Note that ( ℋ × 0ℋ) ≤op 𝑇 means that 𝑇 is a positive operator. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
⊢ ≤op = {〈𝑡, 𝑢〉 ∣ ((𝑢 −op 𝑡) ∈ HrmOp ∧ ∀𝑥 ∈ ℋ 0 ≤ (((𝑢 −op 𝑡)‘𝑥) ·ih 𝑥))} | ||
Definition | df-eigvec 29558* | Define the eigenvector function. Theorem eleigveccl 29664 shows that eigvec‘𝑇, the set of eigenvectors of Hilbert space operator 𝑇, are Hilbert space vectors. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
⊢ eigvec = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ( ℋ ∖ 0ℋ) ∣ ∃𝑧 ∈ ℂ (𝑡‘𝑥) = (𝑧 ·ℎ 𝑥)}) | ||
Definition | df-eigval 29559* | Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 29666 shows that (eigval‘𝑇)‘𝐴, the eigenvalue associated with eigenvector 𝐴, is a complex number. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
⊢ eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))) | ||
Definition | df-spec 29560* | Define the spectrum of an operator. Definition of spectrum in [Halmos] p. 50. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.) |
⊢ Lambda = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ℂ ∣ ¬ (𝑡 −op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ}) | ||
Theorem | nmopval 29561* | Value of the norm of a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ ℋ → (normop‘𝑇) = sup({𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}, ℝ*, < )) | ||
Theorem | elcnop 29562* | Property defining a continuous Hilbert space operator. (Contributed by NM, 28-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
⊢ (𝑇 ∈ ContOp ↔ (𝑇: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (normℎ‘((𝑇‘𝑤) −ℎ (𝑇‘𝑥))) < 𝑦))) | ||
Theorem | ellnop 29563* | Property defining a linear Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
⊢ (𝑇 ∈ LinOp ↔ (𝑇: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑇‘𝑦)) +ℎ (𝑇‘𝑧)))) | ||
Theorem | lnopf 29564 | A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ LinOp → 𝑇: ℋ⟶ ℋ) | ||
Theorem | elbdop 29565 | Property defining a bounded linear Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
⊢ (𝑇 ∈ BndLinOp ↔ (𝑇 ∈ LinOp ∧ (normop‘𝑇) < +∞)) | ||
Theorem | bdopln 29566 | A bounded linear Hilbert space operator is a linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ BndLinOp → 𝑇 ∈ LinOp) | ||
Theorem | bdopf 29567 | A bounded linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ BndLinOp → 𝑇: ℋ⟶ ℋ) | ||
Theorem | nmopsetretALT 29568* | The set in the supremum of the operator norm definition df-nmop 29544 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑇: ℋ⟶ ℋ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆ ℝ) | ||
Theorem | nmopsetretHIL 29569* | The set in the supremum of the operator norm definition df-nmop 29544 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ ℋ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆ ℝ) | ||
Theorem | nmopsetn0 29570* | The set in the supremum of the operator norm definition df-nmop 29544 is nonempty. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
⊢ (normℎ‘(𝑇‘0ℎ)) ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} | ||
Theorem | nmopxr 29571 | The norm of a Hilbert space operator is an extended real. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ ℋ → (normop‘𝑇) ∈ ℝ*) | ||
Theorem | nmoprepnf 29572 | The norm of a Hilbert space operator is either real or plus infinity. (Contributed by NM, 5-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ ℋ → ((normop‘𝑇) ∈ ℝ ↔ (normop‘𝑇) ≠ +∞)) | ||
Theorem | nmopgtmnf 29573 | The norm of a Hilbert space operator is not minus infinity. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ ℋ → -∞ < (normop‘𝑇)) | ||
Theorem | nmopreltpnf 29574 | The norm of a Hilbert space operator is real iff it is less than infinity. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ ℋ → ((normop‘𝑇) ∈ ℝ ↔ (normop‘𝑇) < +∞)) | ||
Theorem | nmopre 29575 | The norm of a bounded operator is a real number. (Contributed by NM, 29-Jan-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ BndLinOp → (normop‘𝑇) ∈ ℝ) | ||
Theorem | elbdop2 29576 | Property defining a bounded linear Hilbert space operator. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ BndLinOp ↔ (𝑇 ∈ LinOp ∧ (normop‘𝑇) ∈ ℝ)) | ||
Theorem | elunop 29577* | Property defining a unitary Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ UniOp ↔ (𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih (𝑇‘𝑦)) = (𝑥 ·ih 𝑦))) | ||
Theorem | elhmop 29578* | Property defining a Hermitian Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
⊢ (𝑇 ∈ HrmOp ↔ (𝑇: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦))) | ||
Theorem | hmopf 29579 | A Hermitian operator is a Hilbert space operator (mapping). (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ HrmOp → 𝑇: ℋ⟶ ℋ) | ||
Theorem | hmopex 29580 | The class of Hermitian operators is a set. (Contributed by NM, 17-Aug-2006.) (New usage is discouraged.) |
⊢ HrmOp ∈ V | ||
Theorem | nmfnval 29581* | Value of the norm of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ℂ → (normfn‘𝑇) = sup({𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘(𝑇‘𝑦)))}, ℝ*, < )) | ||
Theorem | nmfnsetre 29582* | The set in the supremum of the functional norm definition df-nmfn 29550 is a set of reals. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ℂ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘(𝑇‘𝑦)))} ⊆ ℝ) | ||
Theorem | nmfnsetn0 29583* | The set in the supremum of the functional norm definition df-nmfn 29550 is nonempty. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
⊢ (abs‘(𝑇‘0ℎ)) ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘(𝑇‘𝑦)))} | ||
Theorem | nmfnxr 29584 | The norm of any Hilbert space functional is an extended real. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ℂ → (normfn‘𝑇) ∈ ℝ*) | ||
Theorem | nmfnrepnf 29585 | The norm of a Hilbert space functional is either real or plus infinity. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ℂ → ((normfn‘𝑇) ∈ ℝ ↔ (normfn‘𝑇) ≠ +∞)) | ||
Theorem | nlfnval 29586 | Value of the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ℂ → (null‘𝑇) = (◡𝑇 “ {0})) | ||
Theorem | elcnfn 29587* | Property defining a continuous functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
⊢ (𝑇 ∈ ContFn ↔ (𝑇: ℋ⟶ℂ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (abs‘((𝑇‘𝑤) − (𝑇‘𝑥))) < 𝑦))) | ||
Theorem | ellnfn 29588* | Property defining a linear functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
⊢ (𝑇 ∈ LinFn ↔ (𝑇: ℋ⟶ℂ ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑇‘𝑦)) + (𝑇‘𝑧)))) | ||
Theorem | lnfnf 29589 | A linear Hilbert space functional is a functional. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ LinFn → 𝑇: ℋ⟶ℂ) | ||
Theorem | dfadj2 29590* | Alternate definition of the adjoint of a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
⊢ adjℎ = {〈𝑡, 𝑢〉 ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))} | ||
Theorem | funadj 29591 | Functionality of the adjoint function. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
⊢ Fun adjℎ | ||
Theorem | dmadjss 29592 | The domain of the adjoint function is a subset of the maps from ℋ to ℋ. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
⊢ dom adjℎ ⊆ ( ℋ ↑m ℋ) | ||
Theorem | dmadjop 29593 | A member of the domain of the adjoint function is a Hilbert space operator. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ dom adjℎ → 𝑇: ℋ⟶ ℋ) | ||
Theorem | adjeu 29594* | Elementhood in the domain of the adjoint function. (Contributed by Mario Carneiro, 11-Sep-2015.) (Revised by Mario Carneiro, 24-Dec-2016.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ ℋ → (𝑇 ∈ dom adjℎ ↔ ∃!𝑢 ∈ ( ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))) | ||
Theorem | adjval 29595* | Value of the adjoint function for 𝑇 in the domain of adjℎ. (Contributed by NM, 19-Feb-2006.) (Revised by Mario Carneiro, 24-Dec-2016.) (New usage is discouraged.) |
⊢ (𝑇 ∈ dom adjℎ → (adjℎ‘𝑇) = (℩𝑢 ∈ ( ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))) | ||
Theorem | adjval2 29596* | Value of the adjoint function. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ dom adjℎ → (adjℎ‘𝑇) = (℩𝑢 ∈ ( ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢‘𝑦)))) | ||
Theorem | cnvadj 29597 | The adjoint function equals its converse. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
⊢ ◡adjℎ = adjℎ | ||
Theorem | funcnvadj 29598 | The converse of the adjoint function is a function. (Contributed by NM, 25-Jan-2006.) (New usage is discouraged.) |
⊢ Fun ◡adjℎ | ||
Theorem | adj1o 29599 | The adjoint function maps one-to-one onto its domain. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
⊢ adjℎ:dom adjℎ–1-1-onto→dom adjℎ | ||
Theorem | dmadjrn 29600 | The adjoint of an operator belongs to the adjoint function's domain. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ dom adjℎ → (adjℎ‘𝑇) ∈ dom adjℎ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |