Observables in LCS Games

This module defines the algebraic properties of quantum observables in the context of Linear Constraint System (LCS) games. An observable is represented as a self-adjoint, involutive operator.

Key Definitions

• IsObservable: A property of an element $O$ in a star-ring if $O^2=1$ and $O^\dagger=O$.
• ObservableOfMeasurementSystem: Constructs an observable from a binary projector measurement $P$ as $O = P_0 - P_1$.

Key Lemmas

• is_observable_of_measurement_system: Verifies that the difference of projectors in a binary measurement forms a valid observable.

structure IsObservable {R : Type u_1} [Ring R] [StarRing R] (O : R) : Prop

• involutive : O * O = 1
• self_adjoint : star O = O

def ObservableOfMeasurementSystem {R : Type u_1} [Ring R] (f : Fin 2 → R) : R

Equations

• ObservableOfMeasurementSystem f = f 0 - f 1

theorem is_observable_of_measurement_system {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] (f : Fin 2 → R) (h : IsMeasurementSystem f) : IsObservable (ObservableOfMeasurementSystem f)

theorem binary_measurement_eq_projector {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] (f : Fin 2 → R) (h : IsMeasurementSystem f) (y : Fin 2) : f y = (1 / 2) • (1 + (-1) ^ ↑y • ObservableOfMeasurementSystem f)