Conversion from Observables to Projectors

This module defines the mapping from observables (self-adjoint involutive operators) to projector measurement systems and proves their fundamental algebraic properties.

Given an observable $O$, we define two projectors $P_0, P_1$ corresponding to the outcomes $\{0, 1\} \subseteq \mathbb{F}_2$:

• $P_0 = \frac{1}{2}(I + O)$
• $P_1 = \frac{1}{2}(I - O)$

These projectors form a complete binary measurement system.

noncomputable def ObservableToProjector {R : Type u_1} [Ring R] [Algebra ℂ R] (O : R) (a : Fin 2) : R

Converts an observable $O$ and an outcome $a \in \{0, 1\}$ to a projector $P = (1/2)(I + (-1)^a O)$.

Equations

• ObservableToProjector O a = (1 / 2) • (1 + observableSign a • O)

theorem star_observableToProjector {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] (O : R) (hO : IsObservable O) (a : Fin 2) : star (ObservableToProjector O a) = ObservableToProjector O a

If $O$ is an observable, then the projector $P_a = (1/2)(1 + (-1)^a O)$ is self-adjoint.

theorem idempotent_observableToProjector {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] (O : R) (hO : IsObservable O) (a : Fin 2) : ObservableToProjector O a * ObservableToProjector O a = ObservableToProjector O a

If $O$ is an observable, then each $\mathrm{ObservableToProjector}(O,a)$ is idempotent, so it is a projector.

theorem orthogonal_observableToProjector {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] (O : R) (hO : IsObservable O) : ObservableToProjector O 0 * ObservableToProjector O 1 = 0

The two projectors associated to the two outcomes of a single observable are orthogonal: $P_0 P_1 = 0$.

theorem sum_one_observableToProjector {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] (O : R) : ObservableToProjector O 0 + ObservableToProjector O 1 = 1

The two projectors associated to a single observable form a complete binary measurement: $P_0 + P_1 = 1$.

theorem observable_mul_observableToProjector {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] (O : R) (hO : IsObservable O) (a : Fin 2) : O * ObservableToProjector O a = (-1) ^ ↑a • ObservableToProjector O a

theorem commute_observableToProjector {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {O1 O2 : R} (h : Commute O1 O2) (a b : Fin 2) : Commute (ObservableToProjector O1 a) (ObservableToProjector O2 b)

If observables $O₁$ and $O₂$ commute, then all corresponding projectors $P_a(O₁)$ and $P_b(O₂)$ commute as well.

theorem isMeasurementSystem_observableToProjector {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] (O : R) (hO : IsObservable O) : IsMeasurementSystem (ObservableToProjector O)

Given an observable $O$, the mapping ObservableToProjector O is a measurement system.