PhyslibAlpha.AlgebraicFramework.Measurement.ProbabilityLaw

Let $\Omega$ be a measurable space and $\nu$ be an effect-valued measure on $\Omega$ taking values in the effects of $\mathbb{R}$ (the interval $[0, 1] \subset \mathbb{R}$). This definition constructs a standard measure $\mu$ on $\Omega$ such that for every measurable set $s \subseteq \Omega$, the measure is given by $\mu(s) = \nu(s)$, where the value is treated as an extended non-negative real number ($\text{ENNReal}$).

Let $\Omega$ be a measurable space and let $\nu$ be an effect-valued measure on $\Omega$ taking values in the real interval $[0, 1] \subset \mathbb{R}$. For any measurable set $s \subseteq \Omega$, the measure $\nu.\text{toMeasure}$ (the standard measure associated with $\nu$) evaluated at $s$ is equal to the value of $\nu(s)$ converted to an extended non-negative real number, written as $\nu.\text{toMeasure}(s) = \text{ENNReal.ofReal}(\nu(s))$.

Let $\Omega$ be a measurable space and $\nu$ be a real-valued effect-valued measure on $\Omega$. Then the standard measure $\mu$ associated with $\nu$ (denoted as `ν.toMeasure`) is a probability measure, which implies its total mass is one ($\mu(\Omega) = 1$).

Let $\Omega$ be a measurable space and $\nu$ be an effect-valued measure on $\Omega$ taking values in the interval $[0, 1] \subset \mathbb{R}$. This definition constructs an ordinary probability measure on $\Omega$ such that for every measurable set $s \subseteq \Omega$, the measure of $s$ is equal to the real value $\nu(s)$.

Let $\Omega$ be a measurable space and $C$ be an ordered vector space. Given an effect-valued measure $\mu$ on $\Omega$ with values in $C$ and a normal state $\omega: C \to \mathbb{R}$ (a normal unital positive linear map), the **probability law** is the probability measure on $\Omega$ defined by: $$s \mapsto \omega(\mu(s))$$ for every measurable set $s \subseteq \Omega$. This represents the probability distribution obtained by measuring the observable $\mu$ while the system is in the state $\omega$.

Let $\Omega$ be a measurable space and $C$ be an ordered vector space. Let $\mu$ be an effect-valued measure on $\Omega$ with values in $C$, and let $\omega: C \to \mathbb{R}$ be a normal state (a normal unital positive linear map). For any measurable set $s \subseteq \Omega$, the probability measure defined by the probability law of $\mu$ in the state $\omega$ evaluates on $s$ as: $$(\mu.\text{probabilityLaw}(\omega))(s) = \omega(\mu(s))$$