Measurement of finite-dimensional quantum states

A pure state of a finite-dimensional quantum system with computational basis ι is a unit vector of the Euclidean space ℂ^ι, with basis states |x⟩ (Cslib.Quantum.ket). Measuring a unit state ψ in the computational basis gives outcome y with probability |ψ_y|² (Cslib.Quantum.measure); the probability of an outcome in a set S is ∑_{y ∈ S} |ψ_y|² (Cslib.Quantum.measureProb) Arora, Barak, Chapter 10.

Both quantum models of the library measure through this API: the circuit model on ι = Fin n → Bool (Complexity/Computability/Circuit/Quantum/Basic.lean), and the query model, whose register probability Cslib.Quantum.regProb is measureProb of the outcomes with a given query index (Complexity/Computability/QueryComplexity/Quantum/Search.lean).

Main definitions

• Cslib.Quantum.ket: the computational basis state |x⟩.
• Cslib.Quantum.measureProb: the probability of measuring an outcome in a set.
• Cslib.Quantum.measure: the outcome distribution of measuring a unit state.

Main results

• Cslib.Quantum.measureProb_univ: the outcome probabilities sum to ‖ψ‖².
• Cslib.Quantum.measure_toOuterMeasure_apply: the measurement probabilities are measureProb.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach

noncomputable def Cslib.Quantum.ket {ι : Type u_1} [DecidableEq ι] (x : ι) : EuclideanSpace ℂ ι

The computational basis state |x⟩.

@[simp]

theorem Cslib.Quantum.ket_apply {ι : Type u_1} [DecidableEq ι] (x y : ι) : (ket x).ofLp y = if y = x then 1 else 0

@[simp]

theorem Cslib.Quantum.norm_ket {ι : Type u_1} [Fintype ι] [DecidableEq ι] (x : ι) : ‖ket x‖ = 1

noncomputable def Cslib.Quantum.measureProb {ι : Type u_1} (ψ : EuclideanSpace ℂ ι) (S : Finset ι) : ℝ

The probability ∑_{y ∈ S} |ψ_y|² that measuring ψ in the computational basis gives an outcome in S.

theorem Cslib.Quantum.measureProb_nonneg {ι : Type u_1} (ψ : EuclideanSpace ℂ ι) (S : Finset ι) : 0 ≤ measureProb ψ S

theorem Cslib.Quantum.measureProb_univ {ι : Type u_1} [Fintype ι] (ψ : EuclideanSpace ℂ ι) : measureProb ψ Finset.univ = ‖ψ‖ ^ 2

The outcome probabilities of a state sum to its squared norm.

theorem Cslib.Quantum.measureProb_le_measureProb_univ {ι : Type u_1} [Fintype ι] (ψ : EuclideanSpace ℂ ι) (S : Finset ι) : measureProb ψ S ≤ measureProb ψ Finset.univ

noncomputable def Cslib.Quantum.measure {ι : Type u_1} [Fintype ι] (ψ : EuclideanSpace ℂ ι) (hψ : ‖ψ‖ = 1) : PMF ι

Measurement in the computational basis: a unit state ψ gives outcome y with probability |ψ_y|².

@[simp]

theorem Cslib.Quantum.measure_apply {ι : Type u_1} [Fintype ι] (ψ : EuclideanSpace ℂ ι) (hψ : ‖ψ‖ = 1) (y : ι) : (measure ψ hψ) y = ENNReal.ofReal (‖ψ.ofLp y‖ ^ 2)

theorem Cslib.Quantum.measure_toOuterMeasure_apply {ι : Type u_1} [Fintype ι] (ψ : EuclideanSpace ℂ ι) (hψ : ‖ψ‖ = 1) (S : Finset ι) : (measure ψ hψ).toOuterMeasure ↑S = ENNReal.ofReal (measureProb ψ S)

The measurement gives an outcome in S with probability measureProb ψ S.