PhyslibAlpha.ProbabilisticTheory.Classical.BoundedMeasurable

The space of bounded measurable functions on a sample space $\Omega$, denoted by $\text{BoundedMeasurable}(\Omega)$, forms an order unit space. In this space, the order is defined pointwise, and the constant function $\mathbf{1}$ serves as the order unit. This means that $\mathbf{1} \ge 0$ and for any bounded measurable function $f$, there exists a natural number $n$ such that $f \le n \cdot \mathbf{1}$.

The space of bounded measurable functions on a sample space $\Omega$, denoted by $\text{BoundedMeasurable}(\Omega)$, forms an Archimedean order unit space. This property ensures that the order unit space $\text{BoundedMeasurable}(\Omega)$ satisfies the Archimedean property: for any bounded measurable function $f$, if $f \le \epsilon \cdot \mathbf{1}$ for all $\epsilon > 0$ (where $\mathbf{1}$ is the constant identity function and the inequality is pointwise), then $f \le 0$.

The space of bounded measurable functions on a sample space $\Omega$, denoted by $\text{BoundedMeasurable}(\Omega)$, forms an order-unit lattice. This structure means that $\text{BoundedMeasurable}(\Omega)$ is both an Archimedean order unit space (with the constant function $\mathbf{1}$ as the order unit) and a lattice under the pointwise partial order. Specifically, for any two functions $f, g \in \text{BoundedMeasurable}(\Omega)$, their pointwise supremum $f \vee g$ and pointwise infimum $f \wedge g$ are also bounded measurable functions within the space.

Given a measurable subset $s \subseteq \Omega$ of a sample space, the indicator effect is the indicator function $\mathbf{1}_s$ regarded as an element of the space of bounded measurable functions $\text{BoundedMeasurable}(\Omega)$. This function takes the value $1$ if the outcome is in $s$ and $0$ otherwise. It constitutes an effect because it satisfies the condition $0 \le \mathbf{1}_s \le 1$ within the order-unit space of bounded measurable functions.

For any measurable subset $s \subseteq \Omega$, the indicator effect of $s$, denoted as $\text{indicatorEffect}(s, h_s)$, is equal to the indicator function $\mathbf{1}_s$ when viewed as an element of the space of bounded measurable functions $\text{BoundedMeasurable}(\Omega)$.

For a sample space $\Omega$, the outcome measurement is the effect-valued measure that maps each measurable set $A \subseteq \Omega$ to its corresponding indicator effect $\mathbf{1}_A$. This measure takes values in the order-unit space of bounded measurable functions $\text{BoundedMeasurable}(\Omega)$, where an effect is a function $f$ satisfying $0 \le f \le 1$.