PhyslibAlpha.ProbabilisticTheory.Measurement.BornRule

Let $\Omega$ be a measurable space and let $\nu$ be an effect-valued measure on $\Omega$ with values in $\mathbb{R}$. For any sequence of pairwise disjoint measurable sets $s_n \subseteq \Omega$, the measure of their countable union satisfies the additivity property $$\text{ofReal}\left(\nu\left(\bigcup_{n \in \mathbb{N}} s_n\right)\right) = \sum_{n=1}^{\infty} \text{ofReal}(\nu(s_n))$$ where $\text{ofReal}: \mathbb{R} \to [0, \infty]$ denotes the standard conversion from real numbers to extended non-negative reals. This confirms that when the value space is $\mathbb{R}$, an effect-valued measure (where each $\nu(s) \in [0, 1]$) satisfies the countable additivity requirement of a standard measure.

Given a measurable space $\Omega$ and an effect-valued measure $\nu$ on $\Omega$ taking values in the interval $[0, 1] \subseteq \mathbb{R}$, this definition constructs a standard measure $\mu$ on $\Omega$. For any measurable set $s \subseteq \Omega$, the measure $\mu(s)$ is defined as $\text{ofReal}(\nu(s))$, where $\text{ofReal} \colon \mathbb{R} \to [0, \infty]$ is the standard map from real numbers to the extended non-negative real numbers.

Let $\Omega$ be a measurable space and $\nu$ be an effect-valued measure on $\Omega$ taking values in the effects of the real numbers $\mathbb{R}$ (the interval $[0, 1]$). For any measurable set $s \subseteq \Omega$, the measure $\mu$ associated with $\nu$ (denoted $\nu.\text{toMeasure}$) evaluated at $s$ is given by $$\mu(s) = \text{ofReal}(\nu(s))$$ where $\nu(s)$ is the effect value assigned to $s$ and $\text{ofReal} \colon \mathbb{R} \to [0, \infty]$ is the standard map from real numbers to the extended non-negative real numbers.

Let $\Omega$ be a measurable space and let $\nu$ be an effect-valued measure on $\Omega$ taking values in the effects of the real numbers $\mathbb{R}$ (where the effects correspond to the interval $[0, 1]$). Then the measure $\mu$ on $\Omega$ associated with $\nu$ (defined by $\mu(s) = \nu(s)$ for any measurable set $s \subseteq \Omega$) is a probability measure.

Let $\Omega$ be a measurable space. Given an effect-valued measure $\nu$ on $\Omega$ taking values in the effects of $\mathbb{R}$ (the unit interval $[0, 1] \subset \mathbb{R}$), this definition constructs the corresponding probability measure on $\Omega$.

Let $\Omega$ be a measurable space and $E$ be an ordered vector space. Given an effect-valued measure $\mu$ on $\Omega$ with values in $E$ and a normal state $\omega : E \to \mathbb{R}$ (a unital positive linear map that preserves the suprema of directed sets), the **scalarization** of $\mu$ with respect to $\omega$ is the effect-valued measure on $\Omega$ taking values in $\mathbb{R}$ obtained by pushing $\mu$ forward along $\omega$. For any measurable set $s \subseteq \Omega$, the scalarized measure assigns the value $\omega(\mu(s))$.

Let $\Omega$ be a measurable space and $E$ be an ordered vector space. Given an effect-valued measure $\mu$ on $\Omega$ taking values in $E$, a normal state $\omega: E \to \mathbb{R}$, and a measurable set $s \subseteq \Omega$, the value of the scalarization of $\mu$ with respect to $\omega$ at $s$ is equal to the result of applying $\omega$ to the effect $\mu(s)$, expressed as: $$(\mu.\text{scalarize}(\omega))(s) = \omega(\mu(s))$$

Let $\Omega$ be a measurable space and $E$ be an ordered vector space. Given an effect-valued measure $\mu$ on $\Omega$ with values in $E$ and a normal state $\omega: E \to \mathbb{R}$ (a unital positive linear map that preserves the suprema of directed sets), the **probability law** (or outcome distribution) of $\mu$ in the state $\omega$ is the probability measure on $\Omega$ that assigns to each measurable set $s \subseteq \Omega$ the probability value $\omega(\mu(s))$.

Let $\Omega$ be a measurable space and $E$ be an ordered vector space. Given an effect-valued measure $\mu$ on $\Omega$ taking values in $E$, a normal state $\omega: E \to \mathbb{R}$ (a unital positive linear map that preserves suprema), and a measurable set $s \subseteq \Omega$, the probability law of $\mu$ in state $\omega$ assigns to the set $s$ the probability value $\omega(\mu(s))$. Mathematically, this is expressed as: $$(\mu.\text{probabilityLaw}(\omega))(s) = \omega(\mu(s))$$

Let $\Omega'$ and $\Omega$ be measurable spaces and $E$ be an ordered vector space. Suppose $N$ is an effect-valued measure on $\Omega'$ with values in $E$, and $f: \Omega' \to \Omega$ is a measurable function. For any normal state $\omega: E \to \mathbb{R}$, the probability law of the relabeled effect-valued measure (the push-forward of $N$ under $f$) in state $\omega$ is equal to the push-forward of the probability law of $N$ in state $\omega$ under $f$. That is, $$\text{Law}(f_* N, \omega) = f_* (\text{Law}(N, \omega))$$ where $\text{Law}(N, \omega)$ is the probability measure on $\Omega'$ defined by $s \mapsto \omega(N(s))$, and $f_*$ denotes the push-forward (or relabeling) operation.