Lean, informalized

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

Exercise 2.57 - Two successive measurements leave the same state as their cascade

Two measurements in succession make one measurement.

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 is measured twice. The first measurement LL has operators LlL_l and gives an outcome ll; the second, MM, with operators MmM_m, is made on the state the first one leaves and gives an outcome mm. The exercise is to show that the two measurements in succession act as a single one, the measurement with operators MmLlM_m L_l, one for each pair of outcomes (l,m)(l, m): made once on the original state, it leaves after the outcome (l,m)(l, m) the same state that LL and MM leave after ll and then mm.✦

A Quantum System

A quantum system SS is described by its state space ℋS\mathcal{H}_S, a finite dimensional complex Hilbert space.✦ A state ρ\rho of SS is a positive operator of unit trace on ℋS\mathcal{H}_S.✦

Measurements

A measurement MM on SS with a finite set Ω\Omega of outcomes is a family of operators MmM_m on ℋS\mathcal{H}_S, one for each outcome m∈Ωm \in \Omega, that satisfies the completeness relation ∑m∈ΩMm†Mm=I.\sum_{m \in \Omega} M_m^\dagger M_m = I .(1)✦ The positive operator valued measure (POVM) of MM is the family of positive operators Em=Mm†MmE_m = M_m^\dagger M_m, which sum to the identity by (1).✦

The probability pρM(m)p^M_\rho(m) of the outcome mm when MM is performed on a state ρ\rho of SS is given by the Born rule, pρM(m)=Tr⁡(Emρ)=Tr⁡(MmρMm†).p^M_\rho(m) = \operatorname{Tr}(E_m \rho) = \operatorname{Tr}(M_m \rho M_m^\dagger) .(2)✦ When pρM(m)≠0p^M_\rho(m) \neq 0, the state ρmM\rho^M_m of SS after the outcome mm of MM on ρ\rho is the collapsed state, renormalised: ρmM=MmρMm†pρM(m).\rho^M_m = \frac{M_m \rho M_m^\dagger}{p^M_\rho(m)} .(3)✦

Cascaded Measurements

The cascaded measurement NN of two measurements LL and MM on SS, with outcome sets ΩL\Omega_L and ΩM\Omega_M, is the measurement on SS with outcome set ΩL×ΩM\Omega_L \times \Omega_M whose operator for the outcome (l,m)(l, m) is the composite of LlL_l followed by MmM_m: N(l,m)=MmLl.N_{(l,m)} = M_m L_l .(4)✦

When the outcome ll of LL on ρ\rho has nonzero probability, the probability of the outcome (l,m)(l, m) of the cascade is the probability of ll times the conditional probability p(m∣l)p(m \mid l) of mm given ll, the probability of mm when MM is performed on the state ρlL\rho^L_l that ll leaves: pρN(l,m)=pρL(l)pρlLM(m).p^N_\rho(l, m) = p^L_\rho(l)\, p^M_{\rho^L_l}(m) .(5)✦

The Claim

Theorem 1. Let LL and MM be measurements on a quantum system SS, let NN be their cascade, and let ρ\rho be a state of SS. Let ll be an outcome of LL with pρL(l)≠0p^L_\rho(l) \neq 0, and mm an outcome of MM with pρlLM(m)≠0p^M_{\rho^L_l}(m) \neq 0. Then the outcome (l,m)(l, m) of NN has nonzero probability, by (5), and the state it leaves is the state left by the outcome ll of LL followed by the outcome mm of MM: ρ(l,m)N=(ρlL)mM.\rho^N_{(l,m)} = \bigl(\rho^L_l\bigr)^M_m .(6)✦

What Is Checked

The claim is stated over a state ρ\rho of a finite dimensional quantum system, two measurements LL and MM on it, their cascade NN of (4), the Born probabilities (2) and the states after an outcome (3).

The library proves that the operators MmLlM_m L_l of the cascade satisfy the completeness relation, as ∑l,mLl†Mm†MmLl=∑lLl†Ll=I\sum_{l,m} L_l^\dagger M_m^\dagger M_m L_l = \sum_l L_l^\dagger L_l = I by (1) for MM and then for LL, so that the cascade is a measurement. It proves that the state (3) after an outcome of nonzero probability is again a positive operator of unit trace, and it proves the factorization (5) of the cascade’s probabilities.