Lean, informalized

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

Exercise 2.62 - Measurement operators that coincide with their POVM elements are projectors

A measurement equal to its own POVM is projective.

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 general measurement on a quantum system is described by measurement operators MiM_i, one for each outcome ii, and the operators Mi†MiM_i^\dagger M_i are the elements of its positive operator-valued measure (POVM). In general the two families differ, and a measurement operator need not even be Hermitian. The exercise takes a measurement for which they coincide, each measurement operator equal to its own POVM element, and asks to show that the measurement is projective: every MiM_i is a projector.

Measurements on a Quantum System

A quantum system SS is a physical system whose state space ℋS\mathcal{H}_S is a finite dimensional complex Hilbert space.✦

A measurement {Mi}\{M_i\} on SS with a finite set of outcomes is a family of measurement operators MiM_i on ℋS\mathcal{H}_S, one for each outcome ii, satisfying the completeness relation ∑iMi†Mi=I.\sum_i M_i^\dagger M_i = I .(1)✦

The POVM of a measurement {Mi}\{M_i\} on SS is the family of operators EiE_i on ℋS\mathcal{H}_S, one for each outcome, given by Ei=Mi†Mi.E_i = M_i^\dagger M_i .(2)✦

A measurement {Mi}\{M_i\} on SS coincides with its POVM when every measurement operator equals the corresponding POVM element, Mi=EiM_i = E_i for every outcome ii.✦

A projective measurement on SS is a measurement whose operators are all projectors, Mi†=Mi=Mi2M_i^\dagger = M_i = M_i^2 for every outcome ii.✦

The Claim

Theorem 1. Let {Mi}\{M_i\} be a measurement with finitely many outcomes on a quantum system SS. If every measurement operator equals its POVM element, then every measurement operator is a projector: Mi=Mi†Mifor every i⇒Mi†=Mi=Mi2for every i.M_i = M_i^\dagger M_i \quad \text{for every } i \qquad\Longrightarrow\qquad M_i^\dagger = M_i = M_i^2 \quad \text{for every } i .(3)✦

What Is Checked

The claim is stated over a measurement {Mi}\{M_i\} on a quantum system and over its POVM, the operators EiE_i of (2). About these constructions the library proves that the operators EiE_i of any measurement form a POVM: each is a positive operator, and the completeness relation (1) makes them sum to the identity, ∑iEi=I\sum_i E_i = I.