The Exercise

A qubit is prepared in the computational basis state $|0\rangle$, and the Pauli observable $X$ is measured on it. The exercise asks for the average value of $X$ in this state and for its standard deviation, the spread of the measured values about that average.

The average value is the expectation value of $X$ in the state $|0\rangle$, and the spread is the standard deviation of $X$ in that state.

A Quantum System

A quantum system $S$ is given by its state space, a finite dimensional complex Hilbert space. The qubit is the two level system whose state space is $\mathbb{C}^2$, the two dimensional complex space with its standard inner product.^✦

A pure state $|\psi\rangle$ of $S$ is a vector of unit norm in the state space of $S$, $\lVert \psi \rVert = 1$.^✦ For a bit $i$, the basis state $|i\rangle$ of the qubit is the pure state whose vector is the standard basis vector $e_i$ of $\mathbb{C}^2$; these are the computational basis states $|0\rangle = e_0 = (1, 0)$ and $|1\rangle = e_1 = (0, 1)$.^✦

Observables

An observable $A$ of $S$ is a self adjoint operator on the state space of $S$, $A^\dagger = A$; its eigenvalues, which are real, are the possible outcomes of a measurement of $A$.^✦ The square $A^2$ of an observable $A$ is the observable whose operator is the square of the operator of $A$.^✦

The Pauli matrices are the complex $2 \times 2$ matrices $$X = \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}, \qquad Y = \begin{pmatrix} 0 & -i \\ i & 0 \end{pmatrix}, \qquad Z = \begin{pmatrix} 1 & 0 \\ 0 & -1 \end{pmatrix},$$(1) with $i$ the imaginary unit. The Pauli vector is $\vec{\sigma} = (X, Y, Z)$; for a real vector $\vec{n} = (n_1, n_2, n_3)$ in three dimensions, the matrix $\vec{n} \cdot \vec{\sigma}$ is $$\vec{n} \cdot \vec{\sigma} = n_1 X + n_2 Y + n_3 Z .$$(2) The Pauli observable $\vec{n} \cdot \vec{\sigma}$ is the observable of the qubit whose operator is the matrix (2) acting on $\mathbb{C}^2$.^✦ The observable $X$ is the Pauli observable for the unit vector $\hat{n} = (1, 0, 0)$; its operator is the matrix $X$ of (1).^✦

Average Value and Standard Deviation

The expectation value $\langle A \rangle_\psi$ of an observable $A$ of $S$ in a pure state $|\psi\rangle$ of $S$ is the inner product of $|\psi\rangle$ with its image under $A$, a real number because $A$ is self adjoint: $$\langle A \rangle_\psi = \langle \psi | A | \psi \rangle .$$(3)^✦ The variance $[\Delta(A)]^2$ of $A$ in $|\psi\rangle$ is the expectation value of $A^2$ less the square of the expectation value of $A$, $$[\Delta(A)]^2 = \langle A^2 \rangle_\psi - \langle A \rangle_\psi^2 ,$$(4) and the standard deviation $\Delta(A)$ of $A$ in $|\psi\rangle$ is its square root.

The Claim

What Is Checked

The claim is stated over the qubit, its basis state $|0\rangle$, the Pauli observable $X$, and the expectation value and standard deviation of an observable in a pure state.

The library proves that each basis vector $e_i$ has unit norm, so that $|i\rangle$ is a pure state, and that the matrix $\vec{n} \cdot \vec{\sigma}$ is Hermitian for every real $\vec{n}$, so that the Pauli observable is self adjoint. It proves as well that the square of a self adjoint operator is self adjoint, so that $A^2$ is again an observable.