Positive Operator-Valued Measures

A Positive Operator-Valued Measures, or POVM, is the most general notion of a quantum "measurement": a collection of positive semidefinite (PSD) operators that sum to the identity. These induce a distribution, POVM.measure, of measurement outcomes; and they induce a CPTP map, POVM.measurement_map, which changes the state but adds learned information.

Developing this theory is important if one wants to discuss classical information across quantum channels, as POVMs are the route to get back to classical information (a Distribution of outcomes).

TODO: They can also evolve under CPTP maps themselves (the Heisenberg picture of quantum evolution), they might commute with each other or not, they might be projective or not.

structure POVM (X : Type u_1) (d : Type u_2) [Fintype X] [Fintype d] [DecidableEq d] : Type (max u_1 u_2)

A POVM is a (finite) collection of PSD matrices on the same Hilbert space that sum to the identity. Here X indexes the matrices, and d is the space dimension.

Applied to an MState on that on that space with POVM.measure, this produces a distribution of outcomes indexed by the same type as the collection.

This measurement action can be composed with MState.of_classical, in which case it is equal to a CPTP map measurement_map.

• mats : X → HermitianMat d ℂ
• zero_le (x : X) : 0 ≤ self.mats x
• normalized : ∑ x : X, self.mats x = 1

def POVM.measurementMap {X : Type u_1} {d : Type u_2} [Fintype X] [Fintype d] [DecidableEq d] [DecidableEq X] (Λ : POVM X d) : CPTPMap d (d × X) ℂ

The act of measuring is a quantum channel, that maps a d-dimensional quantum state to an d × X-dimensional quantum-classical state.

Equations

• One or more equations did not get rendered due to their size.

theorem POVM.measurementMap_apply_matrix {X : Type u_1} {d : Type u_2} [Fintype X] [Fintype d] [DecidableEq d] [DecidableEq X] (Λ : POVM X d) (m : Matrix d d ℂ) : (((Λ.measurementMap.toPTPMap ℂ).toPMap ℂ).toHPMap ℂ).map m = ∑ x : X, Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (↑(Λ.mats x ^ (1 / 2)) * m * ↑(Λ.mats x ^ (1 / 2))) (Matrix.single x x 1)

theorem POVM.measurementMap_apply_hermitianMat {X : Type u_1} {d : Type u_2} [Fintype X] [Fintype d] [DecidableEq d] [DecidableEq X] (Λ : POVM X d) (m : HermitianMat d ℂ) : (((Λ.measurementMap.toPTPMap ℂ).toPMap ℂ).toHPMap ℂ) m = ∑ x : X, ((HermitianMat.conj ↑(Λ.mats x ^ (1 / 2))) m).kronecker (HermitianMat.diagonal fun (y : X) => if x = y then 1 else 0)

def POVM.measure {X : Type u_1} {d : Type u_2} [Fintype X] [Fintype d] [DecidableEq d] (Λ : POVM X d) (ρ : MState d) : Distribution X

A POVM leads to a distribution of outcomes on any given mixed state ρ.

Equations

• Λ.measure ρ = Distribution.mk' (fun (x : X) => (Λ.mats x).inner ↑ρ) ⋯ ⋯

theorem POVM.traceLeft_measurementMap_eq_measure {X : Type u_1} {d : Type u_2} [Fintype X] [Fintype d] [DecidableEq d] [DecidableEq X] (Λ : POVM X d) (ρ : MState d) : (Λ.measurementMap ρ).traceLeft = MState.ofClassical (Λ.measure ρ)

The quantum-classical POVM.measurement_map, gives a marginal on the right equal to POVM.measure.

noncomputable def POVM.measureDiscard {X : Type u_1} {d : Type u_2} [Fintype X] [Fintype d] [DecidableEq d] [DecidableEq X] (Λ : POVM X d) : CPTPMap d X ℂ

The action of measuring a state with the POVM Λ, discarding the resulting state, and keeping the mixed state recording the outcome. This resulting state is purely diagonal, as given in POVM.measureDiscard_apply.

Equations

• Λ.measureDiscard = CPTPMap.traceLeft∘ₘΛ.measurementMap

theorem POVM.measureDiscard_apply {X : Type u_1} {d : Type u_2} [Fintype X] [Fintype d] [DecidableEq d] [DecidableEq X] (Λ : POVM X d) (ρ : MState d) : Λ.measureDiscard ρ = MState.ofClassical (Λ.measure ρ)

noncomputable def POVM.measureForget {X : Type u_1} {d : Type u_2} [Fintype X] [Fintype d] [DecidableEq d] [DecidableEq X] (Λ : POVM X d) : CPTPMap d d ℂ

The action of measuring a state with the POVM Λ, forgetting the measurement outcome, and keeping the disturbed state.

Equations

• Λ.measureForget = CPTPMap.traceRight∘ₘΛ.measurementMap