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

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

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

• sum_one : ∑ x : I, f x = 1
• idempotent (x : I) : f x * f x = f x
• orthogonal (x y : I) : x ≠ y → f x * f y = 0
• self_adjoint (x : I) : star (f x) = f x

noncomputable def 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

Equations

• InducedMeasurementSystem f g j = ∑ i : I with g i = j, f i

theorem induced_measurement_system_is_measurement_system {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 measurement_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 measurement_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 measurement_intersection {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 eq_of_mul_projectors_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 measurement_sum_mul_projector {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