PhyslibAlpha.AlgebraicFramework.OrderUnit.Effect.BoundedIntegral

For a given real-valued bound $M$ and a natural number $n$, the mesh bound is the natural number $\lceil (n+1)M \rceil$. This value represents the number of mesh cells, each of width $\frac{1}{n+1}$, required to cover the distance from $0$ up to $M$.

For a real-valued bound $M$ and a natural number $n$ representing the scale, the mesh index set is the type of integers $k$ such that $-\lceil (n+1)M \rceil \leq k \leq \lceil (n+1)M \rceil$. This set provides the labels for the mesh cells of width $\frac{1}{n+1}$ used to partition the range $[-M, M]$ during the approximation of a bounded measurable function.

For a given real-valued bound $M$, a scale $n \in \mathbb{N}$, and a mesh index $k$ (where $|k| \leq \lceil (n+1)M \rceil$), the mesh weight is defined as the real number $\frac{k}{n+1}$. This value represents the left endpoint of the $k$-th cell in a uniform partition of width $\frac{1}{n+1}$ used to approximate a bounded measurable function.

For a function $f: \Omega \to \mathbb{R}$, a real-valued bound $M$, a scale $n \in \mathbb{N}$, and an index $k$ belonging to the mesh index set (where $|k| \le \lceil (n+1)M \rceil$), the mesh piece is the set of points $x \in \Omega$ such that the floor of $(n+1)f(x)$ is equal to $k$. Mathematically, this is the pre-image $\{x \in \Omega \mid \lfloor (n+1)f(x) \rfloor = k\}$, representing the subset of the domain where $f(x)$ falls into the $k$-th mesh interval $[\frac{k}{n+1}, \frac{k+1}{n+1})$.

Let $f: \Omega \to \mathbb{R}$ be a function, $M \in \mathbb{R}$ be a bound, and $n \in \mathbb{N}$ be a scale parameter. For any point $x \in \Omega$ and any index $k$ in the mesh index set $\text{MeshIndex } M \text{ } n$, $x$ belongs to the mesh cell $\text{meshPiece}(f, M, n, k)$ if and only if the floor of $(n+1)f(x)$ is equal to $k$, i.e., $\lfloor (n+1)f(x) \rfloor = k$.

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

For a measurable function $f : \Omega \to \mathbb{R}$ bounded by $M$ (such that $|f(x)| \le M$ for all $x \in \Omega$) and a scale $n \in \mathbb{N}$, the function `meshIndexOf` assigns to each point $x \in \Omega$ an integer index $k = \lfloor (n+1) f(x) \rfloor$. This index $k$ represents the mesh cell that contains the value $f(x)$ and is proven to satisfy the bound $|k| \le \lceil (n+1)M \rceil$, making it a valid element of the mesh index set $\text{MeshIndex } M \text{ } n$.

Let $f: \Omega \to \mathbb{R}$ be a measurable function bounded by $M$, such that $|f(x)| \le M$ for all $x \in \Omega$. For any scale $n \in \mathbb{N}$ and any point $x \in \Omega$, the integer value of the mesh index assigned to $x$ is equal to $\lfloor (n+1) f(x) \rfloor$.

Let $f: \Omega \to \mathbb{R}$ be a function bounded by $M$ (i.e., $|f(x)| \le M$ for all $x \in \Omega$). For any scale $n \in \mathbb{N}$ and any point $x \in \Omega$, $x$ belongs to the mesh piece (cell) corresponding to the index $k = \lfloor (n+1) f(x) \rfloor$.

For a function $f: \Omega \to \mathbb{R}$ bounded by $M$ (such that $|f(x)| \leq M$ for all $x \in \Omega$) and a scale $n \in \mathbb{N}$, the collection of mesh pieces $\{x \in \Omega \mid \lfloor (n+1)f(x) \rfloor = k\}$, where $k$ ranges over the mesh index set $\{k \in \mathbb{Z} \mid |k| \leq \lceil (n+1)M \rceil \}$, forms a partition of the domain $\Omega$.

For a real-valued function $f: \Omega \to \mathbb{R}$, a bound $M \in \mathbb{R}$, and a scale $n \in \mathbb{N}$, the value of the mesh simple function at a point $x \in \Omega$—constructed using the weights $\text{meshWeight}(k) = \frac{k}{n+1}$ and the partition $\text{meshPiece}(k) = \{x \in \Omega \mid \lfloor (n+1)f(x) \rfloor = k\}$—is given by $$\operatorname{simpleValue}(\operatorname{meshWeight}, \operatorname{meshPiece}, x) = \frac{\lfloor (n+1)f(x) \rfloor}{n+1}.$$

For a function $f: \Omega \to \mathbb{R}$ and a real-valued bound $M$, let $f_n$ be the mesh simple function approximation at scale $n \in \mathbb{N}$, which is defined by the weights $\frac{k}{n+1}$ and the mesh pieces $\{x \in \Omega \mid \lfloor (n+1)f(x) \rfloor = k\}$. For any point $x \in \Omega$, the absolute difference between the simple function value and the function value satisfies: $$|f_n(x) - f(x)| \le \frac{1}{n+1}$$ where $n+1$ represents the mesh resolution.

For an index set $\iota$, a collection of sets $s : \iota \to \mathcal{P}(\Omega)$, weight functions $a, b : \iota \to \mathbb{R}$, and a point $x \in \Omega$, the evaluation of the simple function at $x$ is additive with respect to the weights. That is, $$\operatorname{simpleValue}(a + b, s, x) = \operatorname{simpleValue}(a, s, x) + \operatorname{simpleValue}(b, s, x),$$ where $(a + b)_i = a_i + b_i$ denotes the pointwise addition of the weights.

Let $r \in \mathbb{R}$ be a scalar, $c: \iota \to \mathbb{R}$ be a function representing weights, $s: \iota \to \mathcal{P}(\Omega)$ be a collection of sets, and $x \in \Omega$ be a point. The value of the simple function (defined by the weights $c$ and the sets $s$) at the point $x$ is homogeneous with respect to the weights. That is, $$\text{simpleValue}(r \cdot c, s, x) = r \cdot \text{simpleValue}(c, s, x),$$ where $r \cdot c$ denotes the pointwise scalar multiplication of the weights.

Let $\Omega$ be a set, and let $\iota$ and $\iota'$ be finite index sets. If $\{s_i\}_{i \in \iota}$ and $\{s'_j\}_{j \in \iota'}$ are both partitions of $\Omega$, then the collection of pairwise intersections $\{s_i \cap s'_j\}_{(i, j) \in \iota \times \iota'}$ is also a partition of $\Omega$.

Let $\Omega$ be a set, and let $\{s_i\}_{i \in \iota}$ and $\{s'_j\}_{j \in \iota'}$ be two finite partitions of $\Omega$. Given a set of coefficients $c: \iota \to \mathbb{R}$, for any $x \in \Omega$, the value of the simple function defined by $(c, s)$ at $x$ is equal to the value of the simple function defined on the product partition $\{s_i \cap s'_j\}_{(i, j) \in \iota \times \iota'}$ using the coefficients $c_i$ for each pair $(i, j)$. 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 a set $A$.

Let $\Omega$ be a space, and let $\{s_i\}_{i \in \iota}$ and $\{s'_j\}_{j \in \iota'}$ be two finite partitions of $\Omega$. For any collection of coefficients $c' : \iota' \to \mathbb{R}$ and any point $x \in \Omega$, the value of the simple function associated with coefficients $c'$ and partition $s'$ at $x$ is equal to the value of the simple function defined on the product partition $\{s_i \cap s'_j\}_{(i, j) \in \iota \times \iota'}$ where the coefficient for the index $(i, j)$ is $c'_j$. That is, $$\text{simpleValue}(c', s', x) = \text{simpleValue}((i, j) \mapsto c'_j, (i, j) \mapsto s_i \cap s'_j, x)$$

Let $\Omega$ be a set, and let $I$ and $J$ be finite index sets. Let $\{s_i\}_{i \in I}$ and $\{s'_j\}_{j \in J}$ be partitions of $\Omega$. For any weight functions $a : I \to \mathbb{R}$ and $b : J \to \mathbb{R}$, and for any point $x \in \Omega$, the sum of the simple functions defined by $(a, s)$ and $(b, s')$ at $x$ is equal to the simple function defined by the common refinement partition $\{s_i \cap s'_j\}_{(i,j) \in I \times J}$ with weights $a_i + b_j$. Mathematically: $\text{simpleValue}(a, s, x) + \text{simpleValue}(b, s', x) = \text{simpleValue}((i, j) \mapsto a_i + b_j, (i, j) \mapsto s_i \cap s'_j, x)$, where $\text{simpleValue}(c, \sigma, x)$ denotes the value at $x$ of the simple function associated with weights $c$ and partition $\sigma$.

Let $\Omega$ be a set and $\mu$ be an effect-valued measure on $\Omega$ taking values in a space $E$. Let $\iota$ and $\iota'$ be finite index sets, and let $\{s_i\}_{i \in \iota}$ and $\{s'_j\}_{j \in \iota'}$ be two partitions of $\Omega$. For any collection of coefficients $c : \iota \to \mathbb{R}$, the integral of the simple function defined by the weights $c$ and the partition $s$ is equal to the integral of the simple function defined on the product partition $\{s_i \cap s'_j\}_{(i, j) \in \iota \times \iota'}$ where the weight for the index $(i, j)$ is given by $c_i$. That is, $$\text{simpleIntegral}(\mu, c, s) = \text{simpleIntegral}(\mu, (i, j) \mapsto c_i, (i, j) \mapsto s_i \cap s'_j)$$

Let $\mu$ be an effect-valued measure on a space $\Omega$ with values in $E$. Let $\{s_i\}_{i \in \iota}$ and $\{s'_j\}_{j \in \iota'}$ be two finite partitions of $\Omega$. For any weight function $c' : \iota' \to \mathbb{R}$, the simple integral of $c'$ with respect to the partition $\{s'_j\}$ is equal to the simple integral over the common refinement partition $\{s_i \cap s'_j\}_{(i, j) \in \iota \times \iota'}$ where the weights are given by the second component $c'_j$. Mathematically: $$\text{simpleIntegral}(\mu, c', s') = \text{simpleIntegral}(\mu, (i, j) \mapsto c'_j, (i, j) \mapsto s_i \cap s'_j)$$

Let $\mu$ be an effect-valued measure on a space $\Omega$ taking values in $E$. Suppose $\{s_i\}_{i \in \iota}$ and $\{s'_j\}_{j \in \iota'}$ are two finite partitions of $\Omega$ with corresponding weight functions $c: \iota \to \mathbb{R}$ and $c': \iota' \to \mathbb{R}$. The difference of the two simple integrals is equal to the simple integral over the common refinement partition $\{s_i \cap s'_j\}_{(i, j) \in \iota \times \iota'}$ with weights given by the pointwise difference $c_i - c'_j$. That is: $$\text{simpleIntegral}(\mu, c, s) - \text{simpleIntegral}(\mu, c', s') = \text{simpleIntegral}(\mu, (i, j) \mapsto c_i - c'_j, (i, j) \mapsto s_i \cap s'_j)$$

Let $\mu$ be an effect-valued measure on a space $\Omega$ taking values in $E$. Suppose $\{s_i\}_{i \in \iota}$ and $\{s'_j\}_{j \in \iota'}$ are two finite partitions of $\Omega$ with corresponding weights $c: \iota \to \mathbb{R}$ and $c': \iota' \to \mathbb{R}$. The sum of the two simple integrals is equal to the simple integral over the common refinement partition $\{s_i \cap s'_j\}_{(i,j) \in \iota \times \iota'}$ with weights given by the pointwise sum $c_i + c'_j$. That is: $$\text{simpleIntegral}(\mu, c, s) + \text{simpleIntegral}(\mu, c', s') = \text{simpleIntegral}(\mu, (i, j) \mapsto c_i + c'_j, (i, j) \mapsto s_i \cap s'_j)$$

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

Let $\mu$ be an effect-valued measure on a space $\Omega$ with values in an ordered space $E$ possessing an Archimedean order unit. Let $\{s_i\}_{i \in \iota}$ be a finite partition of $\Omega$ and $c_i \in \mathbb{R}$ be a set of weights. If there exists a constant $\delta \ge 0$ such that $|c_i| \le \delta$ for every $i \in \iota$ where $s_i$ is non-empty, then the order-unit norm of the simple integral of these weights against $\mu$ is bounded by $\delta$: $$\left\| \sum_{i \in \iota} c_i \mu(s_i) \right\| \le \delta$$ where $\|\cdot\|$ denotes the order-unit norm.

Let $\mu$ be an effect-valued measure on a space $\Omega$ taking values in an ordered space $E$. Let $\{s_i\}_{i \in \iota}$ be a finite partition of $\Omega$ and let $c_i \in \mathbb{R}$ be a collection of weights. If for every $i \in \iota$ such that the set $s_i$ is non-empty, the weight $c_i$ is non-negative ($c_i \ge 0$), then the simple integral of these weights against $\mu$ is non-negative: $$0 \le \sum_{i \in \iota} c_i \mu(s_i)$$

Let $\mu$ be an effect-valued measure on a space $\Omega$ with values in an ordered space $E$ possessing an Archimedean order unit. Let $f: \Omega \to \mathbb{R}$ be a function. Suppose $g$ and $g'$ are two real-valued simple functions on $\Omega$ defined by finite partitions $\{s_i\}_{i \in \iota}$ and $\{s'_j\}_{j \in \iota'}$ with weights $c_i$ and $c'_j$, respectively. If there exist non-negative real numbers $\epsilon, \epsilon' \ge 0$ such that the simple functions satisfy $|g(x) - f(x)| \le \epsilon$ and $|g'(x) - f(x)| \le \epsilon'$ for all $x \in \Omega$, then the order-unit norm $\|\cdot\|$ of the difference of their simple integrals satisfies: $$\left\| \sum_{i \in \iota} c_i \mu(s_i) - \sum_{j \in \iota'} c'_j \mu(s'_j) \right\| \le \epsilon + \epsilon'$$ where $\sum c_i \mu(s_i)$ and $\sum c'_j \mu(s'_j)$ are the simple integrals of $g$ and $g'$ against $\mu$.

Let $E$ be an ordered space with an Archimedean order unit $1$. For any real scalar $c \in \mathbb{R}$ and any element $x \in E$, the order-unit norm $\| \cdot \|$ satisfies the inequality: $$\|c \cdot x\| \le |c| \cdot \|x\|$$ where the order-unit norm $\|x\|$ is defined as the infimum of all $r \ge 0$ such that $-r \cdot 1 \le x \le r \cdot 1$.

Let $E$ be an ordered space with an Archimedean order unit $1$. For any element $y \in E$ and any real number $r \in \mathbb{R}$, if the order-unit norm of $y$ (denoted $\|y\|$) satisfies $\|y\| < r$, then $y \leq r \cdot 1$.

The space $E$ is equipped with the structure of a normed additive commutative group. This structure is induced by the order-unit norm $\|\cdot\|$ associated with an Archimedean order unit $1 \in E$, where the norm of an element $x \in E$ is defined as $\|x\| = \inf \{r \in \mathbb{R}_{\ge 0} \mid -r \cdot 1 \le x \le r \cdot 1\}$. This structure provides the necessary metric and topological framework for the space, where the distance between two elements is given by $d(x, y) = \|x - y\|$.

For any elements $x, y$ in the space $E$, the distance $d(x, y)$ is equal to the order-unit norm of their difference, $\|x - y\|$.

Let $E$ be a space equipped with an Archimedean order-unit norm $\|\cdot\|$. For any sequence $(a_n)_{n \in \mathbb{N}}$ in $E$ and any limit $L \in E$, if $a_n$ converges to $L$ (with respect to the topology induced by the order-unit norm), then for any real scalar $c \in \mathbb{R}$, the scaled sequence $(c \cdot a_n)_{n \in \mathbb{N}}$ converges to $c \cdot L$.

Let $f: \Omega \to \mathbb{R}$ be a measurable function such that $|f(x)| \leq M$ for some bound $M \in \mathbb{R}$ and all $x \in \Omega$. Let $\mu$ be an effect-valued measure on $\Omega$ taking values in an Archimedean order-unit space $E$ equipped with the order-unit norm $\|\cdot\|$. For each $n \in \mathbb{N}$, let $I_n$ be the integral of the simple function approximating $f$ at scale $n$, defined as: $$I_n = \sum_{k} \frac{k}{n+1} \mu\left(\left\{x \in \Omega \mid \left\lfloor (n+1)f(x) \right\rfloor = k\right\}\right)$$ where the sum ranges over the mesh index set $\{k \in \mathbb{Z} \mid |k| \leq \lceil (n+1)M \rceil \}$. Then the sequence $(I_n)_{n \in \mathbb{N}}$ is a Cauchy sequence in $E$.

Let $f: \Omega \to \mathbb{R}$ be a measurable function bounded by a constant $M$ (such that $|f(x)| \leq M$ for all $x \in \Omega$), and let $\mu$ be an effect-valued measure on $\Omega$ taking values in a space $E$ that is complete with respect to its order-unit norm. The **integral** of $f$ against $\mu$ is defined as the limit of the integrals of a sequence of simple functions that approximate $f$ uniformly. Specifically, it is the limit as $n \to \infty$ of the mesh simple integrals: $$\lim_{n \to \infty} \sum_{k} \frac{k}{n+1} \mu\left(\left\{x \in \Omega \mid \lfloor (n+1)f(x) \rfloor = k\right\}\right)$$ where the sum is taken over integers $k$ such that $|k| \leq \lceil (n+1)M \rceil$. This limit exists because the sequence of simple integrals is Cauchy in the complete space $E$.

Let $f: \Omega \to \mathbb{R}$ be a measurable function bounded by $M \in \mathbb{R}$, such that $|f(x)| \leq M$ for all $x \in \Omega$. Let $\mu$ be an effect-valued measure on $\Omega$ taking values in a space $E$ that is complete with respect to its order-unit norm. For each $n \in \mathbb{N}$, consider the mesh simple integral $I_n$ defined as: $$I_n = \sum_{k} \frac{k}{n+1} \mu\left(\left\{x \in \Omega \mid \lfloor (n+1)f(x) \rfloor = k\right\}\right)$$ where the sum is taken over the mesh index set $\{k \in \mathbb{Z} \mid |k| \leq \lceil (n+1)M \rceil \}$. Then the sequence $(I_n)_{n \in \mathbb{N}}$ converges to the integral of $f$ against $\mu$ as $n \to \infty$ in the topology of the order-unit norm: $$\lim_{n \to \infty} I_n = \int f \, d\mu$$

Let $\Omega$ be a sample space and $E$ be an order-unit space that is complete with respect to its order-unit norm. Let $\mu$ be an effect-valued measure on $\Omega$ taking values in $E$, and let $f: \Omega \to \mathbb{R}$ be a measurable function bounded by a constant $M$ (i.e., $|f(x)| \leq M$ for all $x \in \Omega$). Consider a sequence of simple functions $g_n: \Omega \to \mathbb{R}$, each defined by a finite index set $\iota_n$, real weights $c_{n,i}$, and a measurable partition $\{s_{n,i}\}_{i \in \iota_n}$ of $\Omega$, such that $g_n(x) = \sum_{i \in \iota_n} c_{n,i} \mathbb{1}_{s_{n,i}}(x)$. If the sequence $g_n$ converges to $f$ uniformly—specifically, if there exists a sequence of non-negative real numbers $\epsilon_n$ such that $\epsilon_n \to 0$ as $n \to \infty$ and $|g_n(x) - f(x)| \leq \epsilon_n$ for all $n$ and $x \in \Omega$—then the sequence of simple integrals of $g_n$ against $\mu$ converges to the integral of $f$ against $\mu$ in the norm of $E$: $$\lim_{n \to \infty} \sum_{i \in \iota_n} c_{n,i} \mu(s_{n,i}) = \int f d\mu$$ This result ensures that the integral of $f$ is independent of the specific choice of approximating simple functions, provided they converge uniformly to $f$.

Let $f: \Omega \to \mathbb{R}$ be a measurable function and $\mu$ be an effect-valued measure on $\Omega$ taking values in a space $E$ that is complete with respect to its order-unit norm. Suppose $M$ and $M'$ are real numbers such that $|f(x)| \leq M$ and $|f(x)| \leq M'$ for all $x \in \Omega$. Then the integral of $f$ against $\mu$ constructed using the bound $M$ is equal to the integral constructed using the bound $M'$, i.e., $$\text{integral } hf \, hM \, \mu = \text{integral } hf \, hM' \, \mu$$ where $hf$ is the proof of measurability of $f$, and $hM, hM'$ are the proofs of boundedness by $M$ and $M'$ respectively.

Let $\mu$ be an effect-valued measure on a space $\Omega$ taking values in a complete space $E$ equipped with an order-unit norm. Let $f: \Omega \to \mathbb{R}$ be a measurable function such that $|f(x)| \leq M$ for some $M \in \mathbb{R}$. If $f$ is a simple function defined by a finite partition $\{s_i\}_{i \in \iota}$ of $\Omega$ and weights $c_i \in \mathbb{R}$ such that $f(x) = \sum_{i \in \iota} c_i \mathbb{1}_{s_i}(x)$ for all $x \in \Omega$, then the integral of $f$ against $\mu$ (constructed via uniform limits) is equal to its simple integral: $$\int f \, d\mu = \sum_{i \in \iota} c_i \mu(s_i)$$

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

Let $\Omega$ be a measurable space and $E$ be a space that is complete with respect to its order-unit norm. Let $f, g: \Omega \to \mathbb{R}$ be measurable functions such that $|f(x)| \leq M$ and $|g(x)| \leq M'$ for all $x \in \Omega$ and constants $M, M' \in \mathbb{R}$. For an effect-valued measure $\mu$ on $\Omega$ taking values in $E$, the integral of the sum $f + g$ is equal to the sum of the individual integrals: $$\int (f + g) \, d\mu = \int f \, d\mu + \int g \, d\mu$$ This property holds assuming the measurability and boundedness of $f+g$ (with bound $M + M'$), which are derived from the properties of $f$ and $g$.

Let $f: \Omega \to \mathbb{R}$ be a measurable function bounded by a constant $M$ (i.e., $|f(x)| \leq M$ for all $x \in \Omega$), and let $\mu$ be an effect-valued measure taking values in a complete order-unit space $E$. For any scalar $c \in \mathbb{R}$, let $c \cdot f$ be the function $x \mapsto c \cdot f(x)$. If $c \cdot f$ is measurable and bounded by $|c| \cdot M$, then the integral of $c \cdot f$ against $\mu$ satisfies: $$\int (c \cdot f) \, d\mu = c \cdot \int f \, d\mu$$