Lean, informalized

Nielsen & Chuang · Chapter 2, Introduction to quantum mechanics · p. 70

Exercise 2.14 - The adjoint of a finite linear combination of operators between inner product spaces

The adjoint conjugates the coefficients of a sum.

Hover over a blue or green term in the text, or a node in the graph, to find it in the other. Select it to read its declaration both in Lean and in words.

The Exercise

Take linear operators A1,…,AnA_1, \dots, A_n and complex numbers a1,…,ana_1, \dots, a_n, and form the operator ∑iaiAi\sum_i a_i A_i. The exercise asks to show that taking the adjoint is antilinear: the adjoint of this combination is the combination of the adjoints of the AiA_i, each coefficient aia_i replaced by its complex conjugate.✦

Operators and Their Adjoints

Let VV and WW be finite-dimensional complex Hilbert spaces, with inner product (⋅,⋅)(\cdot, \cdot), and for a scalar aa write a*a^* for its complex conjugate. The adjoint of a linear operator AA from VV to WW is the linear operator A†A^\dagger from WW to VV such that (|w⟩,A|v⟩)=(A†|w⟩,|v⟩)for all |v⟩∈V,|w⟩∈W.(|w\rangle, A|v\rangle) = (A^\dagger |w\rangle, |v\rangle) \quad \text{for all } |v\rangle \in V,\ |w\rangle \in W .(1)

The Claim

Theorem 1. Let SS be a finite index set, and for each i∈Si \in S let AiA_i be a linear operator from VV to WW and aia_i a scalar. Then (∑i∈SaiAi)†=∑i∈Sai*Ai†.\Bigl( \sum_{i \in S} a_i A_i \Bigr)^\dagger = \sum_{i \in S} a_i^* A_i^\dagger .(2)✦

What Is Checked

The claim is stated over two inner product spaces VV and WW with a common field of scalars, the linear operators from VV to WW and their finite linear combinations, and the adjoint of (1).

About these the library proves (2) for every finite family of operators and every choice of coefficients, under no further hypothesis.