Lean, informalized

Nielsen & Chuang · Chapter 8, Quantum noise and quantum operations · p. 357

Exercise 8.2 - The probability of an outcome and the state after it, both read off one operator

Outcome probability and collapse from a single operator.

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

A system in the state ρ\rho is measured with measurement operators MmM_m, one for each outcome mm. Sandwiching the state between MmM_m and its adjoint gives an operator for each outcome. The exercise is to show that this one operator holds everything the outcome mm tells about the system: its trace is the probability of obtaining mm, and divided by its trace it is the state of the system just after mm is obtained.

A Quantum System and a Measurement

A quantum system SS is given by its state space, a finite dimensional complex Hilbert space.✦ A state ρ\rho of SS is a positive operator of unit trace on the state space of SS.✦

A measurement {Mm}\{M_m\} on SS with finitely many outcomes is a family of operators MmM_m on the state space of SS, one for each outcome mm, satisfying the completeness relation ∑mMm†Mm=I.\sum_m M_m^\dagger M_m = I.(1)✦

The positive operator valued measure (POVM) of a measurement {Mm}\{M_m\} on SS is the family of its effects Em=Mm†MmE_m = M_m^\dagger M_m, one for each outcome mm.✦

The probability p(m)p(m) of the outcome mm, when the measurement is performed on a state ρ\rho of SS, is given by the Born rule as the expectation of the effect of that outcome: p(m)=tr(Emρ).p(m) = \mathrm{tr}(E_m \rho).(2)✦

The state ρm\rho_m of SS after an outcome mm of nonzero probability is the renormalised operator ρm=MmρMm†p(m).\rho_m = \frac{M_m \rho M_m^\dagger}{p(m)}.(3)✦

The Claim

The operation element ℰm(ρ)\mathcal{E}_m(\rho) of the outcome mm of a measurement {Mm}\{M_m\} on a state ρ\rho of SS is the operator ℰm(ρ)=MmρMm†\mathcal{E}_m(\rho) = M_m \rho M_m^\dagger(4)✦ on the state space of SS.

Theorem 1. Let {Mm}\{M_m\} be a measurement with finitely many outcomes on a quantum system SS, let ρ\rho be a state of SS, and let mm be an outcome. Then the probability of mm is the trace of the operation element, p(m)=tr(ℰm(ρ)).p(m) = \mathrm{tr}\bigl(\mathcal{E}_m(\rho)\bigr).(5)✦ If moreover p(m)≠0p(m) \neq 0, the state of SS after the outcome mm is the operation element divided by its trace, ρm=ℰm(ρ)tr(ℰm(ρ)).\rho_m = \frac{\mathcal{E}_m(\rho)}{\mathrm{tr}\bigl(\mathcal{E}_m(\rho)\bigr)}.(6)✦

What Is Checked

The two equations are stated over a measurement on a quantum system SS and a state of SS, through the probability (2) of an outcome, the state (3) after it and the operation element (4).

About these constructions the library proves that each effect EmE_m is positive and that, by (1), the effects sum to the identity, so that they form a POVM; and that the state ρm\rho_m after an outcome of nonzero probability is a positive operator of unit trace, a state of SS.