PhyslibAlpha.ProbabilisticTheory.Representation.PVM

Given a measurable space $\Omega$ and an order unit space $E$, a **positive-operator-valued measure (POVM)** is a measure that maps each measurable subset of $\Omega$ to an "effect" in $E$. An effect is an element $x \in E$ satisfying $0 \le x \le 1$, where $1$ denotes the order unit of $E$. This is the physical terminology for an `EffectValuedMeasure`.

Given a positive-operator-valued measure (POVM) $\mu$ defined on a measurable space $\Omega$ with values in an order unit space $E$, the property `IsPVM` signifies that $\mu$ is a **projection-valued measure (PVM)**. This occurs if, for every measurable subset $S \subseteq \Omega$, the effect $\mu(S)$ assigned by the measure is sharp.

Let $\Omega$ be a measurable space and $E$ be an order unit space. For any positive-operator-valued measure (POVM) $\mu$ defined on $\Omega$, the effect assigned to the empty set $\emptyset$ (representing the impossible event) is sharp.

Let $\Omega$ be a measurable space and $E$ be an order unit space. For any positive-operator-valued measure (POVM) $\mu$ on $\Omega$ taking values in $E$, the effect $\mu(\Omega)$ assigned to the universal set $\Omega$ (the certain event) is sharp.

Let $\Omega$ be a measurable space and $A$ be a unital $C^*$-algebra. Let $\mu$ be a positive-operator-valued measure (POVM) on $\Omega$ taking values in the space of self-adjoint elements of $A$. If for every measurable set $S \subseteq \Omega$, the element $\mu(S)$ is idempotent (that is, $\mu(S)^2 = \mu(S)$), then $\mu$ is a projection-valued measure (PVM).

Given a measurable space $\Omega$ and an order unit space $E$, a **projection-valued measure (PVM)** is a positive-operator-valued measure (POVM) $\mu$ such that for every measurable subset $S \subseteq \Omega$, the effect $\mu(S)$ is sharp.

A projection-valued measure (PVM) is a specific type of positive-operator-valued measure (POVM). This instance provides a natural coercion from the type of PVMs to the type of POVMs, effectively viewing a PVM as a POVM by forgetting the requirement that its effects must be sharp.

Let $\Omega$ be a measurable space and $E$ be an order unit space. For any two projection-valued measures (PVMs) $\pi$ and $\rho$ on $\Omega$ taking values in $E$, if $\pi(S) = \rho(S)$ for every measurable subset $S \subseteq \Omega$, then $\pi = \rho$.

Let $\Omega$ be a measurable space and $E$ be an order unit space. For any projection-valued measure (PVM) $\pi$ on $\Omega$ and any measurable subset $s \subseteq \Omega$, the effect $\pi(s)$ assigned to that subset is a sharp effect.