PhyslibAlpha.ProbabilisticTheory.Measurement.BoundedIntegral

Given a bound $M \in \mathbb{R}$ and a natural number $n$ (where the mesh width is defined as $1/(n+1)$), this function returns the number of mesh cells required to cover the interval from $0$ to $M$. It is defined as the ceiling of the product of $M$ and $n+1$, expressed as $\lceil (n+1)M \rceil$.

Given a bound $M \in \mathbb{R}$ and a discretization parameter $n \in \mathbb{N}$, the type `MeshIndex M n` is the set of integer labels for the mesh cells used to partition the interval $[-M, M]$. It is defined as the set of integers $k$ such that $-\lceil (n+1)M \rceil \le k \le \lceil (n+1)M \rceil$, where $\lceil (n+1)M \rceil$ is the value determined by `meshBound M n`.

Given a bound $M \in \mathbb{R}$, a discretization parameter $n \in \mathbb{N}$, and an index $k$ from the set of mesh indices $\text{MeshIndex}(M, n)$, the function returns the real value $\frac{k}{n + 1}$. This value represents the "weight" of the $k$-th mesh cell, corresponding to the left endpoint of that cell.

Given a function $f : \Omega \to \mathbb{R}$, a real bound $M$, a discretization parameter $n \in \mathbb{N}$ (defining a mesh width of $1/(n+1)$), and a mesh index $k \in \text{MeshIndex } M \ n$, the set `meshPiece f M n k` is the subset of $\Omega$ consisting of all points $x$ such that $\lfloor (n+1)f(x) \rfloor = k$. This set is the pullback along $f$ of the $k$-th mesh interval, representing the points where $f(x)$ lies in the half-open interval $[\frac{k}{n+1}, \frac{k+1}{n+1})$.

For a function $f: \Omega \to \mathbb{R}$, a real bound $M$, a discretization parameter $n \in \mathbb{N}$, and a mesh index $k \in \text{MeshIndex}(M, n)$, a point $x \in \Omega$ belongs to the $k$-th mesh piece $\text{meshPiece}(f, M, n, k)$ if and only if the floor of $(n + 1) f(x)$ is equal to $k$: $$x \in \text{meshPiece}(f, M, n, k) \iff \lfloor (n + 1) f(x) \rfloor = k$$

Let $f : \Omega \to \mathbb{R}$ be a measurable function. For any discretization parameter $n \in \mathbb{N}$ and any mesh index $k \in \text{MeshIndex } M \ n$, the $k$-th mesh piece defined by the set $\{x \in \Omega \mid \lfloor (n+1)f(x) \rfloor = k\}$ is a measurable set.

Given a function $f: \Omega \to \mathbb{R}$ bounded by $M$ (such that $|f(x)| \le M$ for all $x \in \Omega$) and a discretization parameter $n \in \mathbb{N}$ (where the mesh width is $1/(n+1)$), this function maps a point $x \in \Omega$ to its corresponding mesh cell index $k = \lfloor (n+1) f(x) \rfloor$. This index is guaranteed to lie within the range of the mesh index set $[- \lceil (n+1)M \rceil, \lceil (n+1)M \rceil]$.

For a function $f: \Omega \to \mathbb{R}$ bounded by $M$, a natural number $n$, and a point $x \in \Omega$, the mesh index of $x$ (viewed as an integer) is equal to the floor of the value $(n + 1) f(x)$, expressed as: $$\text{meshIndexOf}(x) = \lfloor (n + 1) f(x) \rfloor$$

Let $f: \Omega \to \mathbb{R}$ be a function and $M$ be a real number such that $|f(x)| \le M$ for all $x \in \Omega$. For any $n \in \mathbb{N}$ and any $x \in \Omega$, let $k = \lfloor (n+1)f(x) \rfloor$ be the mesh index of $x$ (denoted as `meshIndexOf hM n x`). Then $x$ is an element of the $k$-th mesh piece of $f$ at scale $n$, which is defined as the set $\{y \in \Omega \mid \lfloor (n+1)f(y) \rfloor = k\}$.

Let $f: \Omega \to \mathbb{R}$ be a function bounded by $M \in \mathbb{R}$ (i.e., $|f(x)| \le M$ for all $x \in \Omega$). For any natural number $n$, the collection of mesh pieces $S_k = \{x \in \Omega \mid \lfloor (n+1)f(x) \rfloor = k\}$, indexed by $k \in \mathbb{Z}$ such that $-\lceil (n+1)M \rceil \le k \le \lceil (n+1)M \rceil$, forms a partition of the space $\Omega$.

Given a function $f : \Omega \to \mathbb{R}$, a bound $M \in \mathbb{R}$, and a discretization parameter $n \in \mathbb{N}$, let the $k$-th mesh piece be $s_k = \{x \in \Omega \mid \lfloor (n+1)f(x) \rfloor = k\}$ and the corresponding mesh weight be $c_k = \frac{k}{n+1}$. For any $x \in \Omega$, the value of the simple function $\sum_k c_k \mathbb{1}_{s_k}$ at $x$ is given by $$\frac{\lfloor (n + 1)f(x) \rfloor}{n + 1}$$ where $\lfloor \cdot \rfloor$ denotes the floor function.

For any function $f : \Omega \to \mathbb{R}$, a real bound $M$, and a discretization parameter $n \in \mathbb{N}$, the mesh-based simple function approximation (with mesh width $1/(n+1)$) evaluated at any point $x \in \Omega$ satisfies the inequality: $$\left| \text{simpleValue}(\text{meshWeight } M \ n, \text{meshPiece } f \ M \ n, x) - f(x) \right| \le \frac{1}{n + 1}$$ Here, `meshPiece f M n` partitions $\Omega$ into sets where the value of $f(x)$ falls into the $k$-th mesh interval, and `meshWeight M n` assigns the value $\frac{k}{n+1}$ to the $k$-th piece. In essence, the mesh approximation $g_n(x)$ stays within $1/(n+1)$ of $f(x)$ for all $x$.

For a finite index set $\iota$, real coefficients $a, b : \iota \to \mathbb{R}$, a family of sets $s : \iota \to \mathcal{P}(\Omega)$, and a point $x \in \Omega$, the value of the simple function $\sum_{i \in \iota} c_i \mathbb{1}_{s_i}(x)$ is additive with respect to its coefficients: $$\sum_{i \in \iota} (a_i + b_i) \mathbb{1}_{s_i}(x) = \sum_{i \in \iota} a_i \mathbb{1}_{s_i}(x) + \sum_{i \in \iota} b_i \mathbb{1}_{s_i}(x)$$ where $\mathbb{1}_{s_i}$ is the indicator function of the set $s_i$.

Let $\iota$ be a finite index set, $r \in \mathbb{R}$ be a scalar, and $c : \iota \to \mathbb{R}$ be a collection of coefficients. For any family of sets $s : \iota \to \mathcal{P}(\Omega)$ and any point $x \in \Omega$, the value of the simple function with scaled coefficients $r \cdot c$ at $x$ is equal to $r$ times the value of the simple function with coefficients $c$ at $x$. In terms of the indicator function $\mathbb{1}_{s_i}$, this states: $$\sum_{i \in \iota} (r c_i) \mathbb{1}_{s_i}(x) = r \sum_{i \in \iota} c_i \mathbb{1}_{s_i}(x)$$

Let $\Omega$ be a set, and let $\iota$ and $\iota'$ be finite index sets. Suppose $\{s_i\}_{i \in \iota}$ and $\{s'_j\}_{j \in \iota'}$ are partitions of $\Omega$. Then the collection of pairwise intersections $\{s_i \cap s'_j\}$ indexed by the product set $\iota \times \iota'$ is also a partition of $\Omega$.

Let $\iota$ and $\iota'$ be finite index sets, and let $\{s_i\}_{i \in \iota}$ and $\{s'_j\}_{j \in \iota'}$ be partitions of a space $\Omega$. For any coefficients $c_i \in \mathbb{R}$ and any point $x \in \Omega$, the value of the simple function defined by coefficients $c_i$ and the partition $s_i$ at $x$ is equal to the value of the simple function defined by the same coefficients $c_i$ and the refined partition $\{s_i \cap s'_j\}_{(i,j) \in \iota \times \iota'}$ at $x$. That is: $$\sum_{i \in \iota} c_i \mathbb{1}_{s_i}(x) = \sum_{(i, j) \in \iota \times \iota'} c_i \mathbb{1}_{s_i \cap s'_j}(x),$$ where $\mathbb{1}_A$ denotes the indicator function of the set $A$.

Let $\Omega$ be a space, and let $\{s_i\}_{i \in \iota}$ and $\{s'_j\}_{j \in \iota'}$ be partitions of $\Omega$ indexed by finite sets $\iota$ and $\iota'$. For any point $x \in \Omega$ and any collection of real coefficients $\{c'_j\}_{j \in \iota'}$, the value of the simple function defined by the coefficients $c'_j$ and the partition $s'_j$ at $x$ is equal to the value of the simple function defined over the product partition $\{s_i \cap s'_j\}_{(i,j) \in \iota \times \iota'}$ using the coefficients from the second index (i.e., $c'_j$). That is, $$\sum_{j \in \iota'} c'_j \mathbb{1}_{s'_j}(x) = \sum_{(i, j) \in \iota \times \iota'} c'_j \mathbb{1}_{s_i \cap s'_j}(x),$$ where $\mathbb{1}_A$ denotes the indicator function of the set $A$.

Let $\Omega$ be a set and let $s = \{s_i\}_{i \in \iota}$ and $s' = \{s'_j\}_{j \in \iota'}$ be two partitions of $\Omega$ indexed by finite sets $\iota$ and $\iota'$. Let $a: \iota \to \mathbb{R}$ and $b: \iota' \to \mathbb{R}$ be coefficients. For any $x \in \Omega$, the sum of the values of the two simple functions at $x$ is equal to the value of the simple function defined by the common refinement partition $\{s_i \cap s'_j\}_{(i, j) \in \iota \times \iota'}$ with summed weights: $$\left(\sum_{i \in \iota} a_i \mathbb{1}_{s_i}(x)\right) + \left(\sum_{j \in \iota'} b_j \mathbb{1}_{s'_j}(x)\right) = \sum_{(i, j) \in \iota \times \iota'} (a_i + b_j) \mathbb{1}_{s_i \cap s'_j}(x)$$ where $\mathbb{1}_S$ denotes the indicator function of a set $S$.

Let $\Omega$ be a space and $\mu$ be an effect-valued measure on $\Omega$ taking values in $E$. Let $\{s_i\}_{i \in \iota}$ and $\{s'_j\}_{j \in \iota'}$ be partitions of $\Omega$ indexed by finite sets $\iota$ and $\iota'$. For any collection of real coefficients $\{c_i\}_{i \in \iota}$, the simple integral of the function defined by $c$ and $s$ is equal to the simple integral defined over the product partition $\{s_i \cap s'_j\}_{(i, j) \in \iota \times \iota'}$ with coefficients determined by the first index of the product. Specifically, $$\sum_{i \in \iota} c_i \mu(s_i) = \sum_{(i, j) \in \iota \times \iota'} c_i \mu(s_i \cap s'_j).$$

Let $\Omega$ be a measurable space and $E$ be a space of effects. Let $\mu$ be an effect-valued measure on $\Omega$ taking values in $E$. Let $\iota$ and $\iota'$ be finite index sets. Suppose $\{s_i\}_{i \in \iota}$ and $\{s'_j\}_{j \in \iota'}$ are two partitions of $\Omega$. For any collection of real coefficients $\{c'_j\}_{j \in \iota'}$, the simple integral of the function defined by $c'$ on the partition $s'$ is equal to the simple integral defined on the product refinement partition $\{s_i \cap s'_j\}_{(i, j) \in \iota \times \iota'}$ using the coefficients from the second index ($c'_j$): $$\sum_{j \in \iota'} c'_j \mu(s'_j) = \sum_{(i, j) \in \iota \times \iota'} c'_j \mu(s_i \cap s'_j)$$

Let $\Omega$ be a measurable space and $E$ be an order-unit space. Let $\mu$ be an effect-valued measure on $\Omega$ taking values in $E$. Suppose $\{s_i\}_{i \in I}$ and $\{s'_j\}_{j \in J}$ are two finite partitions of $\Omega$ indexed by finite types $I$ and $J$. For any collections of real coefficients $\{c_i\}_{i \in I}$ and $\{c'_j\}_{j \in J}$, the difference between their respective simple integrals is equal to the simple integral of the difference of the coefficients over the common refinement partition $\{s_i \cap s'_j\}_{(i,j) \in I \times J}$: $$\sum_{i \in I} c_i \mu(s_i) - \sum_{j \in J} c'_j \mu(s'_j) = \sum_{(i, j) \in I \times J} (c_i - c'_j) \mu(s_i \cap s'_j)$$

Let $\Omega$ be a measurable space and $E$ be an order-unit space. Let $\mu$ be an effect-valued measure on $\Omega$ taking values in $E$. Suppose $\{s_i\}_{i \in I}$ and $\{s'_j\}_{j \in J}$ are two finite partitions of $\Omega$ with corresponding real coefficients $c_i$ and $c'_j$. The sum of their simple integrals is equal to the simple integral over the common refinement of the partitions $\{s_i \cap s'_j\}_{(i, j) \in I \times J}$ with weights $c_i + c'_j$: $$\sum_{i \in I} c_i \mu(s_i) + \sum_{j \in J} c'_j \mu(s'_j) = \sum_{(i, j) \in I \times J} (c_i + c'_j) \mu(s_i \cap s'_j)$$

Let $\mu$ be an effect-valued measure on a space $\Omega$ with values in an order-unit space $E$. For any finite partition $\{s_i\}_{i \in \iota}$ of $\Omega$ into measurable sets, the sum of the measures of the sets in the partition is equal to the unit element (the certain outcome) $1 \in E$: $$\sum_{i \in \iota} \mu(s_i) = 1$$

Let $\mu$ be an effect-valued measure on a measurable space $\Omega$ with values in an order-unit space $E$. Let $\{s_i\}_{i \in I}$ be a finite partition of $\Omega$ into measurable sets and $c_i \in \mathbb{R}$ be coefficients for each $i \in I$. If there exists a constant $\delta \geq 0$ such that $|c_i| \leq \delta$ for every $i$ where the set $s_i$ is non-empty, then the order-unit norm of the simple integral of the function $\sum_i c_i \mathbf{1}_{s_i}$ against $\mu$ is also bounded by $\delta$: $$\left\| \sum_{i \in I} c_i \mu(s_i) \right\| \leq \delta$$ where $\|\cdot\|$ denotes the order-unit norm in $E$.

Let $\mu$ be an effect-valued measure on a space $\Omega$ taking values in an order-unit space $E$. For a finite partition $\{s_i\}_{i \in I}$ of $\Omega$ and real coefficients $c_i \in \mathbb{R}$, if $c_i \geq 0$ for all indices $i$ such that $s_i$ is non-empty, then the simple integral of the function $\sum_{i \in I} c_i \mathbf{1}_{s_i}$ against $\mu$ is non-negative: $$\sum_{i \in I} c_i \mu(s_i) \geq 0$$

Let $\mu$ be an effect-valued measure on a space $\Omega$ with values in an order-unit space $E$ equipped with the order-unit norm $\|\cdot\|$. Let $f: \Omega \to \mathbb{R}$ be a function. Suppose $g$ and $g'$ are two simple functions defined by finite partitions $\{s_i\}_{i \in I}$ and $\{s'_j\}_{j \in J}$ of $\Omega$ with real coefficients $\{c_i\}_{i \in I}$ and $\{c'_j\}_{j \in J}$ respectively, such that $g(x) = \sum_{i \in I} c_i \mathbf{1}_{s_i}(x)$ and $g'(x) = \sum_{j \in J} c'_j \mathbf{1}_{s'_j}(x)$. If there exist non-negative constants $\varepsilon, \varepsilon' \geq 0$ such that $|g(x) - f(x)| \le \varepsilon$ and $|g'(x) - f(x)| \le \varepsilon'$ for all $x \in \Omega$, then the difference between their simple integrals against $\mu$ satisfies: $$\left\| \sum_{i \in I} c_i \mu(s_i) - \sum_{j \in J} c'_j \mu(s'_j) \right\| \le \varepsilon + \varepsilon'$$

Let $E$ be an order-unit space with order unit $\mathbf{1}$ and order-unit norm $\|\cdot\|$. For any element $y \in E$ and any real number $r$, if the order-unit norm of $y$ is strictly less than $r$ (i.e., $\|y\| < r$), then $y$ is bounded above by $r \cdot \mathbf{1}$ (i.e., $y \leq r \cdot \mathbf{1}$).

Let $E$ be an ordered additive commutative group equipped with an Archimedean order unit $\mathbf{1}$. The space $E$ is a normed additive commutative group under the order-unit norm $\|\cdot\|$, where for any $x \in E$, the norm is defined as $\|x\| = \inf \{ r \in \mathbb{R} \mid -r \cdot \mathbf{1} \le x \le r \cdot \mathbf{1} \}$.

Let $E$ be an ordered additive commutative group with an Archimedean order unit $\mathbf{1}$. The space $E$ is a complete metric space with respect to the order-unit norm $\|\cdot\|$, which is defined for any $x \in E$ as $\|x\| = \inf \{ r \in \mathbb{R} \mid -r \cdot \mathbf{1} \le x \le r \cdot \mathbf{1} \}$.

Let $E$ be an ordered additive commutative group equipped with an Archimedean order unit. For any two elements $x, y \in E$, the metric distance between them is equal to the order-unit norm of their difference, that is, $\operatorname{dist}(x, y) = \|x - y\|$.

Let $E$ be an ordered additive commutative group with an Archimedean order unit $\mathbf{1}$, equipped with the order-unit norm $\|\cdot\|$. If a sequence $(a_n)_{n \in \mathbb{N}}$ in $E$ converges to a limit $L \in E$ (with respect to the topology induced by the norm), then for any scalar $c \in \mathbb{R}$, the sequence of scalar multiples $(c \cdot a_n)_{n \in \mathbb{N}}$ converges to $c \cdot L$.

Let $\mu$ be an effect-valued measure on a measurable space $\Omega$ taking values in a space $E$ equipped with an order-unit norm $\|\cdot\|$. Let $f: \Omega \to \mathbb{R}$ be a measurable function bounded by $M \in \mathbb{R}$ (i.e., $|f(x)| \le M$ for all $x \in \Omega$). For each $n \in \mathbb{N}$, define the mesh pieces $S_{n,k} = \{x \in \Omega \mid \lfloor (n+1)f(x) \rfloor = k\}$ and the weights $w_{n,k} = \frac{k}{n+1}$. The sequence of simple integrals $(I_n)_{n \in \mathbb{N}}$ defined by $$I_n = \sum_k \frac{k}{n+1} \mu(S_{n,k})$$ is a Cauchy sequence in $E$ with respect to the order-unit norm.

Let $E$ be a complete Archimedean order-unit space equipped with the order-unit norm $\|\cdot\|_{\mathbf{1}}$, and let $\mu$ be an effect-valued measure on a measurable space $\Omega$ with values in $E$. Given a measurable function $f: \Omega \to \mathbb{R}$ and a real bound $M$ such that $|f(x)| \le M$ for all $x \in \Omega$, the integral of $f$ against $\mu$ is defined as the limit in $E$ of the sequence of simple integrals $(I_n)_{n \in \mathbb{N}}$ as $n \to \infty$. This sequence is defined by a uniform mesh approximation: $$I_n = \sum_k \frac{k}{n+1} \mu(\{x \in \Omega \mid \lfloor (n+1)f(x) \rfloor = k\})$$ where the sum is taken over the finite set of indices $k$ such that the resulting sets partition $\Omega$. The limit exists because the sequence $I_n$ is Cauchy and $E$ is assumed to be complete.

Let $E$ be a complete Archimedean order-unit space and $\mu$ be an effect-valued measure on a measurable space $\Omega$ taking values in $E$. Let $f: \Omega \to \mathbb{R}$ be a measurable function bounded by $M \in \mathbb{R}$ (such that $|f(x)| \le M$ for all $x \in \Omega$). For each $n \in \mathbb{N}$, define the mesh pieces $S_{n,k} = \{x \in \Omega \mid \lfloor (n+1)f(x) \rfloor = k\}$ and the mesh weights $w_{n,k} = \frac{k}{n+1}$. Then the sequence of simple integrals $$I_n = \sum_k \frac{k}{n+1} \mu(S_{n,k})$$ converges to the integral $\int f \, d\mu$ in the order-unit norm of $E$ as $n \to \infty$.

Let $\Omega$ be a measurable space and $E$ be a complete Archimedean order-unit space equipped with the order-unit norm $\|\cdot\|_{\mathbf{1}}$. Let $\mu$ be an effect-valued measure on $\Omega$ with values in $E$. Suppose $f: \Omega \to \mathbb{R}$ is a bounded measurable function. Consider a sequence of simple functions $g_n: \Omega \to \mathbb{R}$ defined by finite partitions $\{s_{n,i}\}_{i \in \iota_n}$ and coefficients $c_{n,i}$, such that $g_n(x) = \sum_{i \in \iota_n} c_{n,i} \mathbf{1}_{s_{n,i}}(x)$. If the sequence $g_n$ converges uniformly to $f$—that is, there exists a sequence of non-negative real numbers $\epsilon_n$ such that $\lim_{n \to \infty} \epsilon_n = 0$ and $|g_n(x) - f(x)| \le \epsilon_n$ for all $x \in \Omega$ and $n \in \mathbb{N}$—then the sequence of simple integrals $$\int g_n \, d\mu = \sum_{i \in \iota_n} c_{n,i} \mu(s_{n,i})$$ converges to the integral $\int f \, d\mu$ in $E$ as $n \to \infty$.

Let $E$ be a complete Archimedean order-unit space and $\mu$ be an effect-valued measure on a measurable space $\Omega$ with values in $E$. Let $f: \Omega \to \mathbb{R}$ be a measurable function. If $M$ and $M'$ are two real numbers such that $|f(x)| \le M$ and $|f(x)| \le M'$ for all $x \in \Omega$, then the integral of $f$ against $\mu$ defined using the bound $M$ is equal to the integral defined using the bound $M'$.

Let $E$ be a complete Archimedean order-unit space and $\mu$ be an effect-valued measure on a measurable space $\Omega$ with values in $E$. Let $f: \Omega \to \mathbb{R}$ be a measurable function such that $|f(x)| \le M$ for some real $M$ and all $x \in \Omega$. Suppose $f$ is a simple function represented by a finite partition $\{s_i\}_{i \in I}$ of $\Omega$ and coefficients $c_i \in \mathbb{R}$ such that $f(x) = \sum_{i \in I} c_i \mathbb{1}_{s_i}(x)$ for all $x \in \Omega$. Then the integral of $f$ against $\mu$ coincides with the simple integral: $$\int f \, d\mu = \sum_{i \in I} c_i \mu(s_i)$$ where $\mathbb{1}_{s_i}$ denotes the indicator function of the set $s_i$.

Let $\Omega$ be a measurable space and $E$ be a complete Archimedean order-unit space. Let $\mu$ be an effect-valued measure on $\Omega$ with values in $E$. For any measurable function $f: \Omega \to \mathbb{R}$ that is bounded by some $M \in \mathbb{R}$ (i.e., $|f(x)| \le M$ for all $x \in \Omega$), if $f$ is non-negative ($f(x) \ge 0$ for all $x \in \Omega$), then its integral against $\mu$ is also non-negative: $$0 \le \int f \, d\mu$$

Let $E$ be a complete Archimedean order-unit space and $\mu$ be an effect-valued measure on a measurable space $\Omega$ with values in $E$. For any two measurable functions $f, g: \Omega \to \mathbb{R}$ such that $|f(x)| \le M$ and $|g(x)| \le M'$ for all $x \in \Omega$, the integral of their sum $f + g$ against $\mu$ is equal to the sum of their individual integrals: $$\int (f + g) \, d\mu = \int f \, d\mu + \int g \, d\mu$$ where the integral is defined as the limit of simple functions approximating the bounded measurable functions in the order-unit norm.