PhyslibAlpha.ProbabilisticTheory.Measurement.Finite

In the space of bounded measurable functions on a finite outcome space $\Omega$, the sum of the indicator functions $\mathbb{1}_{\{x\}}$ for all individual outcomes $x \in \Omega$ is equal to the unit function $1$.

Let $\Omega$ be a finite sample space and $\text{BoundedMeasurable}(\Omega)$ be the space of bounded measurable functions on $\Omega$. Suppose $f : \mathbb{N} \to \text{BoundedMeasurable}(\Omega)$ is a monotone increasing sequence of functions and $g \in \text{BoundedMeasurable}(\Omega)$ is the least upper bound (supremum) of the range of $f$. Then for any real number $\varepsilon > 0$, there exists a natural number $n$ such that $g \le f_n + \varepsilon \mathbf{1}$, where $\mathbf{1}$ denotes the constant unit function.

Let $\Omega$ be a finite sample space. Let $\text{BoundedMeasurable}(\Omega)$ be the space of bounded measurable functions on $\Omega$, and let $E$ be an Archimedean order unit space. Any channel $\Phi : \text{BoundedMeasurable}(\Omega) \to E$ (that is, a unital positive linear map) is normal, meaning that it preserves the suprema of directed sets.

For a finite outcome space $\Omega$ and an order unit space $E$, given a family of effects $\{a_x\}_{x \in \Omega}$ in $E$ (where each $0 \le a_x \le 1$) such that they satisfy the normalization condition $\sum_{x \in \Omega} a_x = 1$, this definition constructs a quantum channel (a unital positive linear map) $\Phi: \text{BoundedMeasurable}(\Omega) \to E$. For any observable $f \in \text{BoundedMeasurable}(\Omega)$, the channel is defined by the mapping: $$\Phi(f) = \sum_{x \in \Omega} f(x) \cdot a_x$$ where $f(x)$ are the values of the observable at each outcome $x$.

For a finite outcome space $\Omega$ and an order unit space $E$, let $\{a_x\}_{x \in \Omega}$ be a family of effects in $E$ (where $0 \le a_x \le 1$) such that they satisfy the normalization condition $\sum_{x \in \Omega} a_x = 1$. This definition constructs a measurement $M$ whose underlying channel $\Phi: \text{BoundedMeasurable}(\Omega) \to E$ maps an observable $f$ to the weighted sum of effects: $$\Phi(f) = \sum_{x \in \Omega} f(x) a_x$$ In this measurement, each outcome $x \in \Omega$ corresponds to the effect $a_x$.

Let $\Omega$ be a finite outcome space and $E$ be an order unit space. Suppose $\{a_x\}_{x \in \Omega}$ is a family of effects in $E$ (where $0 \le a_x \le 1$) that satisfy the normalization condition $\sum_{x \in \Omega} a_x = 1$. For the measurement $M$ constructed from these effects, the associated quantum channel $\Phi: \text{BoundedMeasurable}(\Omega) \to E$ maps any observable $f$ to the weighted sum of effects: $$\Phi(f) = \sum_{x \in \Omega} f(x) a_x$$ where $f(x)$ are the values of the observable at each outcome $x$.

Let $\Omega$ be a finite outcome space and $E$ be an order unit space. Given a family of effects $\{a_x\}_{x \in \Omega}$ in $E$ satisfying the normalization condition $\sum_{x \in \Omega} a_x = 1$, let $M$ be the measurement constructed from these atomic effects. For any measurable subset $s \subseteq \Omega$, the value of the measurement $M$ evaluated on $s$ is the sum of the effects of the outcomes contained in $s$: $$M(s) = \sum_{x \in s} a_x$$

Let $\Omega$ be a finite sample space and $E$ be an order unit space. Suppose we have a family of effects $\{a_x\}_{x \in \Omega}$ in $E$ that satisfy the normalization condition $\sum_{x \in \Omega} a_x = 1$. Let $M$ be the measurement constructed from these effects (defined via `ofAtoms`). For any outcome $x \in \Omega$ such that the singleton set $\{x\}$ is measurable, the effect assigned by the measurement $M$ to the outcome $x$ is exactly $a_x$: $$M(\{x\}) = a_x$$

Let $\Omega$ be a finite sample space and $M$ be a measurement on $\Omega$ with values in an order unit space $E$. For each outcome $x \in \Omega$, let $M(\{x\})$ denote the effect associated with the singleton set $\{x\}$. Then the sum of these effects over all possible outcomes in $\Omega$ is equal to the unit element $1$ of $E$: $$\sum_{x \in \Omega} M(\{x\}) = 1$$

Let $\Omega$ be a finite outcome space and $E$ an order unit space. Suppose $M$ and $N$ are two measurements from $\Omega$ to $E$. If for every individual outcome $x \in \Omega$, the effect assigned by $M$ to the singleton set $\{x\}$ is equal to the effect assigned by $N$ to $\{x\}$, then the measurements $M$ and $N$ are equal.