Computational-basis measurement

Born rule for the computational-basis PVM {|x><x|} [dW19, qcnotes.tex:406]: measuring a state vector psi yields outcome x with probability |psi x|^2. For a 1 + n-qubit register we also provide the marginal probability of observing the first qubit, given by the projective measurement {|b><b| ⊗ I} whose outcome probability is the squared norm of the projected block [dW19, qcnotes.tex:433].

The raw StateVector definitions are available for algebraic intermediate states. The PureState wrappers automatically form probability distributions, because normalization is part of PureState.

noncomputable def QuantumAlg.StateVector.probOutcome {n : ℕ} (psi : StateVector n) (x : Fin (2 ^ n)) : ℝ

Born rule [dW19, qcnotes.tex:406]: the probability of observing outcome x when measuring psi in the computational basis.

Equations

• psi.probOutcome x = ‖psi.ofLp x‖ ^ 2

theorem QuantumAlg.StateVector.probOutcome_nonneg {n : ℕ} (psi : StateVector n) (x : Fin (2 ^ n)) : 0 ≤ psi.probOutcome x

theorem QuantumAlg.StateVector.sum_probOutcome {n : ℕ} (psi : StateVector n) : ∑ x : Fin (2 ^ n), psi.probOutcome x = ‖psi‖ ^ 2

The Born-rule weights sum to the squared norm.

@[simp]

theorem QuantumAlg.StateVector.probOutcome_ket {n : ℕ} (x y : Fin (2 ^ n)) : (PureState.ket x).vec.probOutcome y = if y = x then 1 else 0

noncomputable def QuantumAlg.StateVector.probQubit0 {n : ℕ} (psi : StateVector (1 + n)) (b : Fin (2 ^ 1)) : ℝ

Probability that measuring qubit 0 of a 1 + n-qubit raw state vector yields b, leaving the other qubits unobserved.

Equations

• psi.probQubit0 b = ∑ y : Fin (2 ^ n), ‖psi.ofLp (QuantumAlg.prodEquiv (b, y))‖ ^ 2

theorem QuantumAlg.StateVector.probQubit0_nonneg {n : ℕ} (psi : StateVector (1 + n)) (b : Fin (2 ^ 1)) : 0 ≤ psi.probQubit0 b

theorem QuantumAlg.StateVector.probQubit0_smul {n : ℕ} (c : ℂ) (psi : StateVector (1 + n)) (b : Fin (2 ^ 1)) : (c • psi).probQubit0 b = ‖c‖ ^ 2 * psi.probQubit0 b

Scaling a raw state vector scales the marginal probability by the squared scalar norm.

noncomputable def QuantumAlg.PureState.probOutcome {n : ℕ} (psi : PureState n) (x : Fin (2 ^ n)) : ℝ

Born-rule probability for a pure state.

Equations

• psi.probOutcome x = psi.vec.probOutcome x

theorem QuantumAlg.PureState.probOutcome_nonneg {n : ℕ} (psi : PureState n) (x : Fin (2 ^ n)) : 0 ≤ psi.probOutcome x

theorem QuantumAlg.PureState.sum_probOutcome {n : ℕ} (psi : PureState n) : ∑ x : Fin (2 ^ n), psi.probOutcome x = 1

Pure-state outcome probabilities form a probability distribution.

theorem QuantumAlg.PureState.sum_probOutcome_eq_one {n : ℕ} (psi : PureState n) : ∑ x : Fin (2 ^ n), psi.probOutcome x = 1

Compatibility name for the pure-state probability distribution theorem.

@[simp]

theorem QuantumAlg.PureState.probOutcome_ket {n : ℕ} (x y : Fin (2 ^ n)) : (ket x).probOutcome y = if y = x then 1 else 0

noncomputable def QuantumAlg.PureState.expVal {n : ℕ} (psi : PureState n) (O : HilbertOperator n) : ℝ

Expectation value <psi|O|psi> of an observable O, represented as a real number via the real part. Hermiticity is a property of the observable, not part of the raw HilbertOperator type.

Equations

• psi.expVal O = (inner ℂ psi.vec (O.applyVec psi.vec)).re

noncomputable def QuantumAlg.PureState.probQubit0 {n : ℕ} (psi : PureState (1 + n)) (b : Fin (2 ^ 1)) : ℝ

Probability that measuring qubit 0 of a 1 + n-qubit pure state yields b, leaving the other qubits unobserved.

Equations

• psi.probQubit0 b = psi.vec.probQubit0 b

theorem QuantumAlg.PureState.probQubit0_nonneg {n : ℕ} (psi : PureState (1 + n)) (b : Fin (2 ^ 1)) : 0 ≤ psi.probQubit0 b

theorem QuantumAlg.PureState.probQubit0_smul {n : ℕ} (c : ℂ) (psi : StateVector (1 + n)) (b : Fin (2 ^ 1)) : (c • psi).probQubit0 b = ‖c‖ ^ 2 * psi.probQubit0 b

Compatibility name for raw-vector marginal scaling.