Projector Measurement Systems

This module defines the concept of a projector-valued measurement (PVM) in a general star-ring. A measurement system is a family of self-adjoint, idempotent, and mutually orthogonal elements that sum to the identity.

Key Definitions

• IsMeasurementSystem: A property of a family of elements $\{E_i\}_{i \in I}$ indicating they form a valid measurement system.
• inducedMeasurementSystem: A construction to build a measurement over a smaller outcome space given a function $g : I \to J$.

Key Lemmas

• IsMeasurementSystem.commute: Projectors in a measurement system always commute with each other.
• IsMeasurementSystem.sum_mul_sum: The product of two sums of projectors corresponds to the sum over the intersection of the outcome sets.

structure MIPRE.LCS.IsMeasurementSystem {R : Type u_1} [Ring R] [StarRing R] {I : Type u_2} [Fintype I] (f : I → R) : Prop

A projector-valued measurement in a star-ring: a family of self-adjoint, idempotent, mutually orthogonal elements that sum to the identity.

• sum_one : ∑ x : I, f x = 1

  The measurement operators sum to one.

• idempotent (x : I) : f x * f x = f x

  Each measurement operator is idempotent.

• orthogonal (x y : I) : x ≠ y → f x * f y = 0

  Distinct measurement operators are orthogonal.

• self_adjoint (x : I) : star (f x) = f x

  Each measurement operator is self-adjoint.

noncomputable def MIPRE.LCS.inducedMeasurementSystem {R : Type u_1} [Ring R] {I : Type u_2} {J : Type u_3} [Fintype I] [Fintype J] [DecidableEq J] (f : I → R) (g : I → J) : J → R

The measurement on outcome space J induced by pushing a measurement on I forward along g : I → J, summing the operators over each fiber.

Equations

• MIPRE.LCS.inducedMeasurementSystem f g j = ∑ i : I with g i = j, f i

theorem MIPRE.LCS.IsMeasurementSystem.induced {R : Type u_1} [Ring R] [StarRing R] {I : Type u_2} {J : Type u_3} [Fintype I] [Fintype J] [DecidableEq J] (f : I → R) (h : IsMeasurementSystem f) (g : I → J) : IsMeasurementSystem (inducedMeasurementSystem f g)

theorem MIPRE.LCS.IsMeasurementSystem.commute {R : Type u_1} [Ring R] [StarRing R] {I : Type u_2} [Fintype I] {f : I → R} (h : IsMeasurementSystem f) (x y : I) : Commute (f x) (f y)

theorem MIPRE.LCS.IsMeasurementSystem.commute_sum {R : Type u_1} [Ring R] [StarRing R] {I : Type u_2} [Fintype I] {f : I → R} (h : IsMeasurementSystem f) (A B : Finset I) : Commute (∑ x ∈ A, f x) (∑ y ∈ B, f y)

theorem MIPRE.LCS.IsMeasurementSystem.sum_mul_sum {R : Type u_1} [Ring R] [StarRing R] {I : Type u_2} [Fintype I] [DecidableEq I] {f : I → R} (h : IsMeasurementSystem f) (S T : Finset I) : (∑ x ∈ S, f x) * ∑ y ∈ T, f y = ∑ x ∈ S ∩ T, f x

theorem MIPRE.LCS.IsMeasurementSystem.eq_of_forall_mul_eq {R : Type u_1} [Ring R] [StarRing R] {I : Type u_2} [Fintype I] {f : I → R} (h : IsMeasurementSystem f) {T U : R} (heq : ∀ (x : I), T * f x = U * f x) : T = U

theorem MIPRE.LCS.IsMeasurementSystem.sum_mul_single {R : Type u_1} [Ring R] [StarRing R] {I : Type u_2} [Fintype I] [DecidableEq I] {f : I → R} (h : IsMeasurementSystem f) (S : Finset I) (x : I) : (∑ y ∈ S, f y) * f x = if x ∈ S then f x else 0