PhyslibAlpha.AlgebraicFramework.Measurement.MeasurableOutcome

Let $\Omega$ be a measurable space and $C, E$ be ordered vector spaces (typically representing effects in a quantum system). Given an effect-valued measure $\mu$ on $\Omega$ with values in $C$, and a normal positive unital map $\phi : C \to E$ (representing a normal channel), the push-forward measure $\text{map}(\mu, \phi)$ is an effect-valued measure on $\Omega$ with values in $E$ defined by the composition: $$S \mapsto \phi(\mu(S))$$ for every measurable set $S \subseteq \Omega$. The normality of $\phi$ ensures that the resulting map remains countably additive.

Let $\Omega$ be a measurable space and $C, E$ be ordered vector spaces. Given an effect-valued measure $\mu$ on $\Omega$ with values in $C$, a normal unital positive linear map $\phi : C \to E$, and a measurable set $s \subseteq \Omega$, the push-forward measure $\text{map}(\mu, \phi)$ evaluated at $s$ is equal to the result of applying $\phi$ to the value of $\mu$ at $s$: $$(\text{map}(\mu, \phi))(s) = \phi(\mu(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 **scalarization** of $\mu$ by $\omega$ is a real-valued measure on $\Omega$ (specifically an effect-valued measure with values in the classical order-unit space $\mathbb{R}$) defined by: $$S \mapsto \omega(\mu(S))$$ for every measurable set $S \subseteq \Omega$. This represents the ordinary real-valued probability law of the measurement $\mu$ in the state $\omega$ according to the abstract Born rule.

Let $\Omega$ be a measurable space and $C$ be an ordered vector space. For an effect-valued measure $\mu$ on $\Omega$ taking values in $C$, a normal state $\omega: C \to \mathbb{R}$, and a measurable set $s \subseteq \Omega$, the value of the scalarized measure $(\mu.\text{scalarize } \omega)$ at $s$ is equal to the state $\omega$ applied to the value of the original measure $\mu$ at $s$: $$(\mu.\text{scalarize } \omega)(s) = \omega(\mu(s))$$

Let $\Omega$ be a measurable space and $C, E$ be ordered vector spaces. Let $\mu$ be an effect-valued measure on $\Omega$ with values in $C$, and let $\phi : C \to E$ be a normal unital positive linear map (representing a normal channel). For any finite partition of $\Omega$ into measurable sets $\{s_i\}_{i \in \iota}$ and real coefficients $\{c_i\}_{i \in \iota}$, the following equality holds: $$\phi\left( \sum_{i \in \iota} c_i \mu(s_i) \right) = \sum_{i \in \iota} c_i \phi(\mu(s_i))$$ This identity demonstrates that pushing the effect-valued measure $\mu$ forward through the normal channel $\phi$ commutes with the calculation of its finite simple integral.

Let $\Omega$ be a measurable space and $C$ be an ordered vector space. Suppose $\mu$ is an effect-valued measure on $\Omega$ with values in $C$, and $\omega : C \to \mathbb{R}$ is a normal state. For a simple function defined by a finite partition $\{s_i\}_{i \in \iota}$ of $\Omega$ and real coefficients $\{c_i\}_{i \in \iota}$, applying the state $\omega$ to the simple integral against $\mu$ is equal to the ordinary real simple integral against the scalarized measure $\mu_\omega$: $$\omega \left( \sum_{i \in \iota} c_i \mu(s_i) \right) = \sum_{i \in \iota} c_i \omega(\mu(s_i))$$ where $\mu_\omega$ is the measure defined by $\mu_\omega(s) = \omega(\mu(s))$.