PhyslibAlpha.ProbabilisticTheory.Measurement.Postprocessing

A measurement $M$ with outcome space $\Omega$ is a **post-processing** of a measurement $N$ with outcome space $\Omega'$ if there exists a normal channel $K: \text{BoundedMeasurable}(\Omega) \to \text{BoundedMeasurable}(\Omega')$ such that the unital positive linear map associated with $M$ (the Born law/channel $\Phi_M$) is equal to the composition of the map associated with $N$ ($\Phi_N$) and $K$, i.e., $\Phi_M = \Phi_N \circ K$. This indicates that $M$ can be simulated by performing $N$ and applying classical processing to the outcomes.

The notation $M \le_p N$ represents the information preorder on measurements, indicating that the measurement $M$ is a post-processing of the measurement $N$. This relation signifies that $N$ is at least as informative as $M$, as $M$ can be simulated by performing $N$ and applying a classical processing channel to its outcomes.

For any measurement $M$ with outcome space $\Omega$ acting on a system $E$, $M$ is a post-processing of itself, denoted by $M \le_p M$.

Let $M$, $N$, and $P$ be measurements. If $M$ is a post-processing of $N$ (denoted $M \le_p N$) and $N$ is a post-processing of $P$ (denoted $N \le_p P$), then $M$ is a post-processing of $P$ ($M \le_p P$). This confirms that the post-processing relation between measurements is transitive.

Let $M$ and $N$ be measurements on an order unit space $E$ with outcome spaces $\Omega$ and $\Omega'$ respectively. $M$ is a post-processing of $N$ (denoted $M \le_p N$) if and only if there exists a Markov kernel $\kappa$ from $\Omega'$ to $\Omega$ such that the associated channel $\Phi_M$ is equal to the composition of the channel $\Phi_N$ and the classical channel $\Phi_\kappa$ induced by the kernel $\kappa$, i.e., $\Phi_M = \Phi_N \circ \Phi_\kappa$.

Two measurements $M$ (with outcome space $\Omega$) and $N$ (with outcome space $\Omega'$) are **post-processing equivalent** if $M$ is a post-processing of $N$ ($M \le_p N$) and $N$ is a post-processing of $M$ ($N \le_p M$). This equivalence relation implies that each measurement can be simulated by performing the other and applying a classical channel (Markov kernel) to the outcomes, meaning $M$ and $N$ are equally informative.

Let $M$ be a measurement on an order unit space $E$ with outcome space $\Omega$. Then $M$ is post-processing equivalent to itself, denoted as $M \approx_p M$.

Let $M$ and $N$ be measurements with outcome spaces $\Omega$ and $\Omega'$, respectively, both taking values in the same space $E$. If $M$ and $N$ are post-processing equivalent ($M \approx_p N$), then $N$ and $M$ are post-processing equivalent ($N \approx_p M$).

Let $M$, $N$, and $P$ be measurements with outcome spaces $\Omega$, $\Omega'$, and $\Omega''$ respectively, all taking values in the same order unit space $E$. If $M$ is post-processing equivalent to $N$ (denoted $M \approx_p N$) and $N$ is post-processing equivalent to $P$ ($N \approx_p P$), then $M$ is post-processing equivalent to $P$ ($M \approx_p P$).

Given a measurement $N$ on a measurable space $\Omega'$ taking values in an order unit space $E$, and a measurable map $f: \Omega' \to \Omega$ between outcome spaces, this definition constructs a new measurement on $\Omega$. The channel (unital positive linear map) associated with this new measurement is obtained by composing the channel of $N$ with the pull-back channel $f^*$ induced by $f$. Explicitly, for any measurable set $S \subseteq \Omega$, the effect assigned to $S$ by the new measurement is the effect assigned to the preimage $f^{-1}(S)$ by the original measurement $N$.

Let $N$ be a measurement with outcome space $\Omega'$ taking values in an order unit space $E$, and let $f: \Omega' \to \Omega$ be a measurable map. For any measurable set $s \subseteq \Omega$, the effect assigned to $s$ by the deterministically relabeled measurement (denoted as `N.mapOutcome f`) is equal to the effect assigned by the original measurement $N$ to the preimage $f^{-1}(s)$.

Let $N$ be a measurement on a measurable space $\Omega'$ and $f : \Omega' \to \Omega$ be a measurable map. The measurement $N.\text{mapOutcome } f$, obtained by deterministically relabeling the outcomes of $N$ according to $f$ (such that the effect assigned to a set $S \subseteq \Omega$ is the effect assigned to the preimage $f^{-1}(S)$ by $N$), is a post-processing of $N$, denoted $N.\text{mapOutcome } f \le_p N$.

Let $M$ and $N$ be measurements on an order unit space $E$ with outcome spaces $\Omega$ and $\Omega'$, respectively. Let $K : \text{BoundedMeasurable}(\Omega) \to \text{BoundedMeasurable}(\Omega')$ be a normal channel. If the channel associated with $M$ is the composition of the channel associated with $N$ and the channel $K$ (i.e., $\Phi_M = \Phi_N \circ K$), then for every normal state $\omega$ of the system, the Born law (probability measure) of $M$ is equal to the composition of the Markov kernel $\kappa$ (associated with $K$) and the Born law of $N$: $$\text{Law}(M, \omega) = \kappa \circ_m \text{Law}(N, \omega)$$

Let $M$ and $N$ be measurements on a system $E$ with outcome spaces $\Omega$ and $\Omega'$, respectively. If $M$ is a post-processing of $N$ (denoted $M \le_p N$), then there exists a Markov kernel $\kappa$ from $\Omega'$ to $\Omega$ such that for every normal state $\omega$ of the system, the probability law (Born law) of $M$ given $\omega$ is the composition of the kernel $\kappa$ with the probability law of $N$ given $\omega$: $$\text{Law}(M, \omega) = \kappa \circ_m \text{Law}(N, \omega)$$

Let $N$ be a measurement on a system $E$ with outcome space $\Omega'$. Let $f: \Omega' \to \Omega$ be a measurable map used to relabel the outcomes of $N$, and let $N.\text{mapOutcome}(f)$ be the resulting measurement on $\Omega$. For any normal state $\omega$ of the system, the Born law (probability measure) of the relabeled measurement is the push-forward of the Born law of the original measurement $N$ along the map $f$. That is, $$\text{Law}(N.\text{mapOutcome}(f), \omega) = f_* (\text{Law}(N, \omega)),$$ where $f_*$ denotes the push-forward operation on measures.