Projective measurements on ℂ^n are coordinate patterns in a unitary frame

The measurement operators {M a} of one question of a projective measurement on ℂ^n (MIPRE.ProjectiveMeasurement on Matrix n n ℂ) are commuting orthogonal projections summing to the identity. This file proves the structure theorem behind the enumeration of lem:value-lower-approx: there are a unitary U and an outcome pattern r : n → A with

M a = U * diagonal (fun i => if r i = a then 1 else 0) * Uᴴ

for every outcome a (IsPVM.exists_unitary_pattern). So a projective measurement is exactly "a unitary and a pattern", and enumerating unitaries with Gaussian-rational entries together with patterns enumerates exact projective measurements — the route to approximating the quantum value from below without approximate POVMs, matrix square roots or Naimark dilation.

The proof diagonalizes the single Hermitian matrix H = ∑ a, w a • M a for distinct real weights w: an eigenvector u of H with eigenvalue λ satisfies (w a - λ) • M a u = 0, so M a u = 0 unless λ = w a, and ∑ a, M a u = u ≠ 0 forces λ = w a for exactly one a, which is the pattern at u.

theorem MIPRE.ValueApprox.dotProduct_conjTranspose_mul_self {n : Type u_1} [Fintype n] (N : Matrix n n ℂ) (v : n → ℂ) : star v ⬝ᵥ (N.conjTranspose * N).mulVec v = star (N.mulVec v) ⬝ᵥ N.mulVec v

⟨v, Nᴴ N v⟩ = ⟨N v, N v⟩.

structure MIPRE.ValueApprox.IsPVM {n : Type u_1} [Fintype n] [DecidableEq n] {A : Type u_2} [Fintype A] (M : A → Matrix n n ℂ) : Prop

The measurement operators of one question of a projective measurement on ℂ^n: self-adjoint idempotents summing to the identity.

• conjTranspose_eq (a : A) : (M a).conjTranspose = M a

  Each operator is self-adjoint.

• mul_self (a : A) : M a * M a = M a

  Each operator is idempotent.

• sum_eq_one : ∑ a : A, M a = 1

  The operators sum to the identity.

theorem MIPRE.ProjectiveMeasurement.isPVM {n : Type u_1} [Fintype n] [DecidableEq n] {A : Type u_2} [Fintype A] {X : Type u_3} (P : ProjectiveMeasurement X A (Matrix n n ℂ)) (x : X) : ValueApprox.IsPVM (P.M x)

The operators of a ProjectiveMeasurement on a matrix algebra, at a question x.

theorem MIPRE.ValueApprox.IsPVM.conj {n : Type u_1} [Fintype n] [DecidableEq n] {A : Type u_2} [Fintype A] {M : A → Matrix n n ℂ} (hM : IsPVM M) (U : ↥(Matrix.unitaryGroup n ℂ)) : IsPVM fun (a : A) => ↑U * M a * star ↑U

Conjugating by a unitary preserves the structure.

theorem MIPRE.ValueApprox.IsPVM.mul_eq_zero {n : Type u_1} [Fintype n] [DecidableEq n] {A : Type u_2} [Fintype A] [DecidableEq A] {M : A → Matrix n n ℂ} (hM : IsPVM M) {a b : A} (hab : a ≠ b) : M b * M a = 0

Distinct outcomes are orthogonal: M b * M a = 0 for a ≠ b.

def MIPRE.ValueApprox.patternProj {n : Type u_1} [DecidableEq n] {A : Type u_2} [DecidableEq A] (r : n → A) (a : A) : Matrix n n ℂ

The coordinate pattern projections of r : n → A: patternProj r a projects onto the coordinates i with r i = a.

Equations

• MIPRE.ValueApprox.patternProj r a = Matrix.diagonal fun (i : n) => if r i = a then 1 else 0

theorem MIPRE.ValueApprox.isPVM_patternProj {n : Type u_1} [Fintype n] [DecidableEq n] {A : Type u_2} [Fintype A] [DecidableEq A] (r : n → A) : IsPVM (patternProj r)

theorem MIPRE.ValueApprox.IsPVM.exists_unitary_pattern {n : Type u_1} [Fintype n] [DecidableEq n] {A : Type u_2} [Fintype A] [DecidableEq A] {M : A → Matrix n n ℂ} (hM : IsPVM M) : ∃ (U : ↥(Matrix.unitaryGroup n ℂ)) (r : n → A), ∀ (a : A), M a = ↑U * patternProj r a * star ↑U

Structure theorem. A projective measurement on ℂ^n is a coordinate pattern in a unitary frame: M a = U * patternProj r a * Uᴴ for a unitary U and a pattern r.