PhyslibAlpha.ProbabilisticTheory.Measurement.Pushforward

Given a channel $\phi : E \to F$ (defined as a unital positive linear map) and an effect $e$ in the space $E$ (an element satisfying $0 \le e \le 1$), this definition represents the image $\phi(e)$ as an effect in the space $F$. Because $\phi$ is a positive linear map and $\phi(1) = 1$, the result $\phi(e)$ is guaranteed to satisfy the bounds $0 \le \phi(e) \le 1$.

Let $E$ and $F$ be spaces and $\phi : E \to F$ be a channel (a unital positive linear map). For any effect $e \in E$ (an element satisfying $0 \le e \le 1$), the image of $e$ under $\phi$ viewed as an effect in $F$ is equal to the application of the map $\phi$ to $e$ as an element of the underlying space $F$. That is, $(\phi.\text{mapEffect}(e) : F) = \phi(e)$.

Let $E$ and $F$ be order unit spaces, and let $\phi : E \to F$ be a quantum channel (a unital positive linear map). For the zero effect $0 \in E$ (the zero element of the space, which belongs to the interval $[0, 1]$), its image under the map $\phi$ is the zero effect in $F$. That is, $\phi(0) = 0$.

For any channel $\phi : E \to F$ between order unit spaces $E$ and $F$, the image of the unit effect $1 \in E$ under the map $\phi$ is the unit effect $1 \in F$, which can be written as $\phi(1) = 1$.

Let $\Omega$ be a measurable space and $E, F$ be ordered vector spaces. Given an effect-valued measure $\mu$ on $\Omega$ with values in $E$, and a normal channel $\phi : E \to F$ (a unital positive linear map that preserves the suprema of directed sets), the push-forward $\phi \circ \mu$ is an effect-valued measure on $\Omega$ taking values in $F$. For any measurable set $s \subseteq \Omega$, the measure is defined by applying the channel to the effect assigned by the original measure, i.e., $(\phi \circ \mu)(s) = \phi(\mu(s))$.

Let $\Omega$ be a measurable space and $E, F$ be ordered vector spaces. Let $\mu$ be an effect-valued measure on $\Omega$ taking values in $E$, and let $\phi: E \to F$ be a normal channel (a unital positive linear map that preserves the suprema of directed sets). For any measurable set $s \subseteq \Omega$, the value of the push-forward effect-valued measure $\mu.\text{map } \phi$ at $s$ is equal to the image of the effect $\mu(s)$ under the channel $\phi$: $$(\mu.\text{map } \phi)(s) = \phi(\mu(s))$$ where both sides are viewed as elements of the space $F$.