PhyslibAlpha.ProbabilisticTheory.Measurement.Integral

Given a finite index set $\iota$, a collection of real coefficients $c_i$, and a family of sets $s_i \subseteq \Omega$ for $i \in \iota$, this function calculates the value of the simple function $\sum_{i \in \iota} c_i \mathbb{1}_{s_i}$ at a point $x \in \Omega$, where $\mathbb{1}_{s_i}$ denotes the indicator function of the set $s_i$.

Let $\iota$ be a finite index set and $\{s_j\}_{j \in \iota}$ be a partition of the space $\Omega$. For a family of real coefficients $c_j$ and the simple function defined by $f(x) = \sum_{j \in \iota} c_j \mathbb{1}_{s_j}(x)$, if a point $x \in \Omega$ lies in the piece $s_i$ for some $i \in \iota$, then the function evaluates to $c_i$. This holds because, since the pieces of the partition are pairwise disjoint, the indicator functions $\mathbb{1}_{s_j}(x)$ vanish for all $j \neq i$.

Let $\mu$ be an effect-valued measure. For any two sets $s$ and $t$ such that $s = t$, the value of the measure applied to $s$ is equal to the value of the measure applied to $t$ (i.e., $\mu(s) = \mu(t)$). This equality holds regardless of the specific proofs of measurability provided for $s$ and $t$.

Let $\Omega$ be a measurable space and $E$ be a type representing effects. Let $\mu$ be an effect-valued measure on $\Omega$ taking values in $E$. Suppose $\{t_n\}_{n \in \mathbb{N}}$ is a sequence of pairwise disjoint measurable sets in $\Omega$. If there exists a natural number $N$ such that $t_n = \emptyset$ for all $n \geq N$, then the effect-valued measure of their union is equal to the finite sum of their individual measures: $$\mu\left(\bigcup_{n=0}^\infty t_n\right) = \sum_{n=0}^{N-1} \mu(t_n)$$

Let $\mu$ be an effect-valued measure on a measurable space $\Omega$ taking values in a type $E$. For any two measurable sets $A, B \subseteq \Omega$ that are disjoint ($A \cap B = \emptyset$), the measure of their union is the sum of their individual measures: $$\mu(A \cup B) = \mu(A) + \mu(B)$$ where the addition is performed in the space of effects $E$.

Let $\mu$ be an effect-valued measure on a measurable space $\Omega$ taking values in a type $E$ of effects. Let $\{f_i\}_{i \in \iota}$ be a family of measurable sets in $\Omega$. For any finite set of indices $s$, if the sets are pairwise disjoint for all $i, j \in s$ (i.e., $f_i \cap f_j = \emptyset$ whenever $i \neq j$), then the measure of their union over $s$ is the sum of their individual measures: $$\mu\left( \bigcup_{i \in s} f_i \right) = \sum_{i \in s} \mu(f_i)$$

Let $\mu$ be an effect-valued measure on a measurable space $\Omega$ taking values in a type $E$ of effects. Let $I$ be a finite index set and let $\{f_i\}_{i \in I}$ be a family of measurable sets in $\Omega$ that are pairwise disjoint (i.e., $f_i \cap f_j = \emptyset$ for all $i \neq j$). Then the measure of the union of these sets is equal to the sum of the measures of the individual sets: $$\mu\left(\bigcup_{i \in I} f_i\right) = \sum_{i \in I} \mu(f_i).$$

Let $\mu$ be an effect-valued measure on a measurable space $\Omega$ taking values in a type of effects $E$. Given a finite index set $I$, a collection of real coefficients $c_i$ for $i \in I$, and a collection of sets $\{s_i\}_{i \in I}$ that form a finite measurable partition of $\Omega$, the integral of the simple function $f = \sum_{i \in I} c_i \mathbf{1}_{s_i}$ against $\mu$ is defined as the sum: $$\sum_{i \in I} c_i \cdot \mu(s_i)$$ where $\mathbf{1}_{s_i}$ is the indicator function of $s_i$, and $c_i \cdot \mu(s_i)$ denotes the scalar multiplication of the effect $\mu(s_i)$ by the real number $c_i$. This construction is well-defined independently of the specific partition used to represent the simple function.

Let $\mu$ be an effect-valued measure on a space $\Omega$ taking values in $E$ (where $E$ is an additive commutative group). Let $\{s_i\}_{i \in I}$ and $\{s'_j\}_{j \in J}$ be two finite measurable partitions of $\Omega$. For any index $i \in I$, the measure of the set $s_i$ is equal to the sum of the measures of its intersections with each piece of the second partition: $$\mu(s_i) = \sum_{j \in J} \mu(s_i \cap s'_j).$$ This result follows from the finite additivity of $\mu$, as the set $s_i$ is the disjoint union of the sets $\{s_i \cap s'_j\}_{j \in J}$.

Let $\Omega$ be a space and $E$ be a type of effects. Let $\mu$ be an effect-valued measure on $\Omega$ taking values in $E$. Suppose $\{s_i\}_{i \in \iota}$ and $\{s'_j\}_{j \in \iota'}$ are two finite measurable partitions of $\Omega$. For any index $j \in \iota'$, the measure of the set $s'_j$ is equal to the sum of the measures of its intersections with every set in the partition $\{s_i\}$: $$\mu(s'_j) = \sum_{i \in \iota} \mu(s_i \cap s'_j)$$

Let $\mu$ be an effect-valued measure on a measurable space $\Omega$ taking values in a type of effects $E$. Suppose we have two finite measurable partitions of $\Omega$, denoted by $\{s_i\}_{i \in I}$ and $\{s'_j\}_{j \in J}$, with corresponding real coefficients $c_i$ and $c'_j$. If the simple functions defined by these partitions are pointwise equal, that is, for all $x \in \Omega$: $$\sum_{i \in I} c_i \mathbb{1}_{s_i}(x) = \sum_{j \in J} c'_j \mathbb{1}_{s'_j}(x)$$ where $\mathbb{1}_s$ is the indicator function of the set $s$, then their integrals against $\mu$ are equal: $$\sum_{i \in I} c_i \mu(s_i) = \sum_{j \in J} c'_j \mu(s'_j)$$

Let $\mu$ be an effect-valued measure on a measurable space $\Omega$ taking values in a type of effects $E$. Let $\{s_i\}_{i \in \iota}$ be a finite measurable partition of $\Omega$. For any two weight functions $c_1, c_2: \iota \to \mathbb{R}$, the integral of the simple function against $\mu$ is additive with respect to the weights over the fixed partition: $$\sum_{i \in \iota} (c_1(i) + c_2(i)) \cdot \mu(s_i) = \sum_{i \in \iota} c_1(i) \cdot \mu(s_i) + \sum_{i \in \iota} c_2(i) \cdot \mu(s_i)$$ where $c \cdot \mu(s)$ denotes the scalar multiplication of the effect $\mu(s)$ by the real number $c$.

Let $\mu$ be an effect-valued measure on a measurable space $\Omega$ taking values in a type of effects $E$. Let $\{s_i\}_{i \in I}$ be a finite measurable partition of $\Omega$ indexed by a finite set $I$, $c: I \to \mathbb{R}$ be a collection of weights, and $r \in \mathbb{R}$ be a scalar. The integral of the simple function with weights $(r \cdot c)_i = r \cdot c_i$ against $\mu$ is equal to $r$ times the integral of the simple function with weights $c_i$: $$\sum_{i \in I} (r \cdot c_i) \mu(s_i) = r \cdot \sum_{i \in I} c_i \mu(s_i)$$ where the left-hand side represents the integral of the weighted function $r \cdot c$ and the right-hand side represents scalar multiplication of the resulting effect in $E$ by $r$.

Let $\mu$ be an effect-valued measure on a measurable space $\Omega$ taking values in a space of effects $E$. Given a finite collection of non-negative real coefficients $c_i \ge 0$ for $i \in I$ and a collection of sets $\{s_i\}_{i \in I}$ that form a finite measurable partition of $\Omega$, the simple integral of the function $\sum_{i \in I} c_i \mathbf{1}_{s_i}$ against $\mu$ is non-negative, such that: $$0 \le \sum_{i \in I} c_i \cdot \mu(s_i)$$ where the inequality refers to the partial order on the effect space $E$.