Observables of a projective measurement

A projective measurement P : Λ → Matrix n n ℂ and a weighting ε : Λ → ℂ give the operator pvmObs P ε = ∑_a ε a • P a. The one fact worth isolating is that this is a ring homomorphism in ε:

pvmObs P ε * pvmObs P δ = pvmObs P (ε * δ), pvmObs P 1 = 1,

because the projections are mutually orthogonal (IsPVM.orthogonal). Everything the rigidity arguments want about signed sums of a projective measurement follows: with ε valued in {±1}, pvmObs P ε is a self-adjoint reflection; two weightings of the same measurement commute, whatever they are; and if ε δ η is constantly s then pvmObs P ε * pvmObs P δ * pvmObs P η = s • 1 exactly.

That last one is what a linear-constraint-system game's Alice-side dilation buys: the three reflections of one constraint commute and multiply to the constraint's sign, with no error term. Blueprint lem:ms-direct-anticomm is the consumer.

The rules are those of a projective measurement in any ⋆-algebra (MIPRE/Foundations/Measurement.lean, IsPVMIn), of which a matrix projective measurement is one (IsPVM.toIn): this file proves only what is about matrices, that the elements of a matrix projective measurement are mutually orthogonal (IsPVM.orthogonal), and derives the rest.

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

A projective measurement on Matrix n n ℂ: self-adjoint idempotents summing to one. Stated as a predicate on a bare family rather than a bundled structure, because the families this is applied to arrive from exists_projective_dilation in exactly this shape.

• isSelfAdjoint (a : Λ) : (P a).conjTranspose = P a

  Each element is self-adjoint.

• idem (a : Λ) : P a * P a = P a

  Each element is idempotent.

• sum_eq_one : ∑ a : Λ, P a = 1

  The elements sum to one.

theorem MIPRE.IsPVM.posSemidef {n : Type u_1} {Λ : Type u_2} [Fintype n] [DecidableEq n] [Fintype Λ] {P : Λ → Matrix n n ℂ} (h : IsPVM P) (a : Λ) : (P a).PosSemidef

theorem MIPRE.IsPVM.nonneg {n : Type u_1} {Λ : Type u_2} [Fintype n] [DecidableEq n] [Fintype Λ] {P : Λ → Matrix n n ℂ} (h : IsPVM P) (a : Λ) : 0 ≤ P a

theorem MIPRE.IsPVM.orthogonal {n : Type u_1} {Λ : Type u_2} [Fintype n] [DecidableEq n] [Fintype Λ] [DecidableEq Λ] {P : Λ → Matrix n n ℂ} (h : IsPVM P) {a b : Λ} (hab : a ≠ b) : P a * P b = 0

The elements of a projective measurement are mutually orthogonal. Conjugating ∑_c P c = 1 by P a makes the off-diagonal compressions a family of positive matrices summing to zero, so each is zero, and P a P b P a = 0 forces P b P a = 0.

theorem MIPRE.IsPVM.toIn {n : Type u_1} {Λ : Type u_2} [Fintype n] [DecidableEq n] [Fintype Λ] [DecidableEq Λ] {P : Λ → Matrix n n ℂ} (h : IsPVM P) : IsPVMIn P

A matrix projective measurement is a projective measurement in the matrix algebra (MIPRE/Foundations/Measurement.lean), orthogonality included.

theorem MIPRE.IsPVMIn.toIsPVM {n : Type u_1} {Λ : Type u_2} [Fintype n] [DecidableEq n] [Fintype Λ] {P : Λ → Matrix n n ℂ} (h : IsPVMIn P) : IsPVM P

Conversely, a projective measurement in the matrix algebra is a matrix projective measurement.

theorem MIPRE.IsPVM.coarse {n : Type u_1} {Λ : Type u_2} [Fintype n] [DecidableEq n] [Fintype Λ] [DecidableEq Λ] {P : Λ → Matrix n n ℂ} {Λ' : Type u_3} [Fintype Λ'] [DecidableEq Λ'] (h : IsPVM P) (f : Λ → Λ') : IsPVM fun (c : Λ') => ∑ a : Λ with f a = c, P a

Coarse-graining a projective measurement gives a projective measurement. Summing the elements over a level set of f preserves self-adjointness, and mutual orthogonality (IsPVM.orthogonal) makes the sum idempotent; the level sets partition the outcomes, so the sums still add to one. This is what makes the expansion stage's convolutions projective.

theorem MIPRE.IsPVM.mul_eq_ite {n : Type u_1} {Λ : Type u_2} [Fintype n] [DecidableEq n] [Fintype Λ] [DecidableEq Λ] {P : Λ → Matrix n n ℂ} (h : IsPVM P) (a b : Λ) : P a * P b = if a = b then P a else 0

P a * P b is P a on the diagonal and zero off it.

The observable of a weighting

pvmObs P ε = ∑_a ε a • P a is defined for any measurement in any ℂ-module (MIPRE/Foundations/Measurement.lean); these are its rules for a matrix projective measurement, the instances of IsPVMIn.pvmObs_mul and its companions.