PhyslibAlpha.AlgebraicFramework.Representation.PVM

Given a finite set of outcomes $X$ and a finite-dimensional Hilbert space of dimension $d$, a Positive Operator-Valued Measure (POVM) is defined as a collection of positive semidefinite operators $\{E_x\}_{x \in X}$ acting on the space $\mathbb{C}^d$ such that they sum to the identity operator, i.e., $\sum_{x \in X} E_x = I$.

Let $\mu$ be a Positive Operator-Valued Measure (POVM) defined on a measurable space $\Omega$ with values in an ordered space $E$. The property `IsPVM` holds for $\mu$ if for every measurable set $S \subseteq \Omega$, the effect $\mu(S)$ is **sharp**. An effect is considered sharp if it is an extreme point of the unit interval $[0, 1]$ in $E$; in the context of operator algebras, this means $\mu(S)$ is a projection.

For any Positive Operator-Valued Measure (POVM) $\mu$ defined on a measurable space $\Omega$, the effect $\mu(\emptyset)$ assigned to the empty set $\emptyset$ (representing the impossible event) is sharp. In this context, an effect is sharp if it is an extreme point of the set of effects $[0, 1]$.

For any positive operator-valued measure (POVM) $\mu$ defined on a measurable space $\Omega$, the effect $\mu(\Omega)$ assigned to the universal set (representing the certain event) is a sharp effect.

Let $\Omega$ be a measurable space and $A$ be a unital $C^*$-algebra. Let $\mu$ be a Positive Operator-Valued Measure (POVM) on $\Omega$ with values in the self-adjoint part of $A$. If for every measurable set $S \subseteq \Omega$, the effect $\mu(S)$ is an idempotent element in $A$ (that is, $\mu(S)^2 = \mu(S)$), then $\mu$ is a Projection-Valued Measure (PVM).

A Projection-Valued Measure (PVM) is a Positive Operator-Valued Measure (POVM) $\mu$ defined on a measurable space $\Omega$ with values in an order-unit space $E$, such that for every measurable set $S \subseteq \Omega$, the effect $\mu(S)$ is **sharp**. In the context of operator algebras, an effect being sharp is equivalent to it being a genuine projection (a self-adjoint idempotent operator).

This definition provides an automatic coercion that allows a Projection-Valued Measure (PVM) on a measurable space $\Omega$ with values in an order-unit space $E$ to be treated as a Positive Operator-Valued Measure (POVM). It maps the PVM to its underlying measure, effectively forgetting the property that all assigned effects are sharp.

Let $\Omega$ be a measurable space and $E$ be an order-unit space. For any two projection-valued measures (PVMs) $\pi, \rho$ from $\Omega$ to $E$, if for every measurable set $S \subseteq \Omega$, the assigned effects are equal, i.e., $\pi(S) = \rho(S)$, then the projection-valued measures themselves are equal ($\pi = \rho$).

Let $\pi$ be a projection-valued measure (PVM) defined on a measurable space $\Omega$ with values in an order-unit space $E$. For any measurable set $s \subseteq \Omega$, the resulting effect $\pi(s)$ is sharp. An effect is said to be sharp if it is an extreme point of the unit interval $[0, 1]$ in $E$, which in the context of operator algebras corresponds to the effect being a projection (a self-adjoint idempotent operator).