PhyslibAlpha.Mathematics.MeasureTheory.BoundedMeasurable

The submodule of the $\mathbb{R}$-vector space of functions $\Omega \to \mathbb{R}$ consisting of functions $f$ that are measurable and bounded. A function $f$ is in this submodule if it is measurable and there exists a constant $C$ such that $|f(x)| \le C$ for all $x \in \Omega$.

For a measurable space $\Omega$, the type `BoundedMeasurable Ω` represents the set of all real-valued functions $f: \Omega \to \mathbb{R}$ that are both measurable and bounded. A function $f$ is bounded if there exists a constant $C \in \mathbb{R}$ such that $|f(x)| \le C$ for all $x \in \Omega$.

The set of bounded measurable functions $f: \Omega \to \mathbb{R}$ on a measurable space $\Omega$, denoted as $\text{BoundedMeasurable } \Omega$, forms an additive commutative group. The group operations (addition, negation, and the zero element) are defined pointwise.

The set of bounded measurable functions $f: \Omega \to \mathbb{R}$ on a measurable space $\Omega$, denoted as $\text{BoundedMeasurable } \Omega$, forms a vector space (a module) over the real numbers $\mathbb{R}$. The scalar multiplication is defined pointwise, such that for any $c \in \mathbb{R}$ and $f \in \text{BoundedMeasurable } \Omega$, $(c \cdot f)(x) = c \cdot f(x)$ for all $x \in \Omega$.

The type $\text{BoundedMeasurable } \Omega$ of bounded measurable functions on a measurable space $\Omega$ is equipped with a structure that allows its elements to be treated as functions from $\Omega$ to the real numbers $\mathbb{R}$. For any $f \in \text{BoundedMeasurable } \Omega$, the evaluation at $x \in \Omega$ is denoted by $f(x) \in \mathbb{R}$. This mapping is injective, meaning that if two bounded measurable functions $f$ and $g$ satisfy $f(x) = g(x)$ for all $x \in \Omega$, then $f = g$.

Let $\Omega$ be a measurable space. For any two bounded measurable functions $f, g \in \text{BoundedMeasurable } \Omega$, if $f(x) = g(x)$ for all $x \in \Omega$, then $f = g$.

Let $\Omega$ be a measurable space. For any function $f$ in the space of bounded measurable functions $\text{BoundedMeasurable } \Omega$, the function $f: \Omega \to \mathbb{R}$ is measurable.

For any bounded measurable function $f \in \text{BoundedMeasurable } \Omega$ on a measurable space $\Omega$, there exists a constant $C \in \mathbb{R}$ such that for all $x \in \Omega$, the absolute value of the function satisfies $|f(x)| \le C$.

Given a function $f: \Omega \to \mathbb{R}$ on a measurable space $\Omega$, a proof that $f$ is measurable, and a proof that $f$ is bounded (i.e., there exists a constant $C$ such that $|f(x)| \le C$ for all $x \in \Omega$), this function constructs an element of the type `BoundedMeasurable Ω`.

Let $\Omega$ be a measurable space. Given a function $f: \Omega \to \mathbb{R}$, a proof $h_f$ that $f$ is measurable, and a proof $h_b$ that $f$ is bounded, let $\text{mk}(f, h_f, h_b)$ denote the element of the space of bounded measurable functions $\text{BoundedMeasurable } \Omega$ constructed from $f$. For any $x \in \Omega$, the evaluation of this constructed function at $x$ satisfies $(\text{mk}(f, h_f, h_b))(x) = f(x)$.

Let $\Omega$ be a measurable space. For any $x \in \Omega$, the value of the zero function $0 \in \text{BoundedMeasurable } \Omega$ evaluated at $x$ is $0$.

Let $\Omega$ be a measurable space. For any two bounded measurable functions $f, g \in \text{BoundedMeasurable } \Omega$ and any $x \in \Omega$, the sum $(f + g)$ evaluated at $x$ satisfies $(f + g)(x) = f(x) + g(x)$.

Let $\Omega$ be a measurable space and $\text{BoundedMeasurable } \Omega$ be the space of bounded measurable functions $f: \Omega \to \mathbb{R}$. For any function $f \in \text{BoundedMeasurable } \Omega$ and any point $x \in \Omega$, the negation of the function evaluated at $x$ is equal to the negative of the value of $f$ at $x$: $$(-f)(x) = -f(x)$$

Let $\Omega$ be a measurable space. For any two bounded measurable functions $f, g \in \text{BoundedMeasurable } \Omega$ and any point $x \in \Omega$, the subtraction operation $(f - g)$ is defined pointwise such that $(f - g)(x) = f(x) - g(x)$.

Let $\Omega$ be a measurable space. For any real number $c \in \mathbb{R}$, any bounded measurable function $f \in \text{BoundedMeasurable } \Omega$, and any point $x \in \Omega$, the scalar multiplication $(c \cdot f)$ evaluated at $x$ is equal to the product of $c$ and the value of $f$ at $x$: $$(c \cdot f)(x) = c \cdot f(x)$$

Let $\Omega$ be a measurable space. For any natural number $n \in \mathbb{N}$, any bounded measurable function $f \in \text{BoundedMeasurable } \Omega$, and any point $x \in \Omega$, the evaluation of the natural scalar multiplication $n \cdot f$ at $x$ satisfies $(n \cdot f)(x) = n \cdot f(x)$.

Let $\Omega$ be a measurable space. For any finite index set $t$, any family of functions $f_i$ in the space of bounded measurable functions $\text{BoundedMeasurable } \Omega$ indexed by $i \in t$, and any point $x \in \Omega$, the value of the finite sum at $x$ is equal to the sum of the values of each function at $x$: $$\left( \sum_{i \in t} f_i \right)(x) = \sum_{i \in t} f_i(x)$$

For a measurable space $\Omega$, the constant function $f: \Omega \to \mathbb{R}$ defined by $f(x) = 1$ for all $x \in \Omega$ is both measurable and bounded. This definition provides the multiplicative identity element $1$ for the space of bounded measurable functions on $\Omega$.

Let $\Omega$ be a measurable space. For any $x \in \Omega$, the evaluation of the constant function $1$ in the space of bounded measurable functions $\text{BoundedMeasurable } \Omega$ at the point $x$ is equal to the real number $1$: $$1(x) = 1$$

For bounded measurable functions $f, g \in \text{BoundedMeasurable } \Omega$, the relation $f \le g$ is defined pointwise, meaning $f(x) \le g(x)$ for all $x \in \Omega$.

For bounded measurable functions $f, g \in \text{BoundedMeasurable } \Omega$, the strict inequality $f < g$ is defined by the condition that $f \le g$ holds pointwise and $g \le f$ does not hold. Explicitly, this means $f(x) \le g(x)$ for all $x \in \Omega$ and there exists at least one $x \in \Omega$ such that $f(x) < g(x)$.

The space of bounded measurable functions $\text{BoundedMeasurable } \Omega$ is equipped with a maximum operation. For any functions $f, g \in \text{BoundedMeasurable } \Omega$, their maximum $\max(f, g)$ is defined pointwise by $(\max(f, g))(x) = \max(f(x), g(x))$ for all $x \in \Omega$.

The space of bounded measurable functions $\text{BoundedMeasurable } \Omega$ is equipped with a minimum operation. For any two functions $f, g \in \text{BoundedMeasurable } \Omega$, their minimum $\min(f, g)$ is defined pointwise by $(\min(f, g))(x) = \min(f(x), g(x))$ for all $x \in \Omega$. This operation results in another bounded measurable function.

The space of bounded measurable functions $\text{BoundedMeasurable } \Omega$ on a measurable space $\Omega$ forms a lattice under the pointwise partial order. For any two functions $f, g \in \text{BoundedMeasurable } \Omega$, the relation $f \le g$ holds if $f(x) \le g(x)$ for all $x \in \Omega$. The supremum $f \sqcup g$ and infimum $f \sqcap g$ are defined by the pointwise maximum and minimum functions, respectively.

Let $f$ and $g$ be bounded measurable functions from a measurable space $\Omega$ to the real numbers $\mathbb{R}$. The relation $f \le g$ holds if and only if $f(x) \le g(x)$ for all $x \in \Omega$.

Let $\Omega$ be a measurable space, and let $f$ and $g$ be bounded measurable functions in the space $\text{BoundedMeasurable } \Omega$. For any $x \in \Omega$, the value of their supremum (join) $f \sqcup g$ evaluated at $x$ is equal to the maximum of their individual values at $x$, i.e., $(f \sqcup g)(x) = \max(f(x), g(x))$.

For any two bounded measurable functions $f, g: \Omega \to \mathbb{R}$ and any point $x \in \Omega$, the value of their infimum $f \sqcap g$ evaluated at $x$ is equal to the minimum of the values of $f$ and $g$ at that point, i.e., $(f \sqcap g)(x) = \min(f(x), g(x))$.

Let $\Omega$ be a measurable space, and let $f$ be a bounded measurable function in $\text{BoundedMeasurable } \Omega$. For any $x \in \Omega$, the value of its positive part $f^+$ evaluated at $x$ is equal to the maximum of $f(x)$ and $0$, i.e., $f^+(x) = \max(f(x), 0)$.

For any bounded measurable function $f: \Omega \to \mathbb{R}$ and any point $x \in \Omega$, the value of its negative part $f^-$ evaluated at $x$ is equal to the maximum of $-f(x)$ and $0$, which is $f^-(x) = \max(-f(x), 0)$.

The space of bounded measurable functions $\text{BoundedMeasurable } \Omega$ on a measurable space $\Omega$ forms an ordered additive monoid. This means that the pointwise addition and the pointwise partial order $\le$ are compatible: for any functions $f, g, h \in \text{BoundedMeasurable } \Omega$, if $f \le g$ (i.e., $f(x) \le g(x)$ for all $x \in \Omega$), then $f + h \le g + h$.

Let $\Omega$ be a measurable space. In the space of bounded measurable functions $\text{BoundedMeasurable } \Omega$, scalar multiplication by a non-negative real number preserves the pointwise ordering. Specifically, for any $c \in \mathbb{R}$ such that $c \ge 0$ and any functions $f, g \in \text{BoundedMeasurable } \Omega$, if $f(x) \le g(x)$ for all $x \in \Omega$, then $(c \cdot f)(x) \le (c \cdot g)(x)$ for all $x \in \Omega$.

For a sequence of bounded measurable functions $(f_n)_{n \in \mathbb{N}}$ on a measurable space $\Omega$ and a bounded measurable function $g$ such that $f_n \le g$ pointwise for all $n$, the pointwise supremum $\sup_{n \in \mathbb{N}} f_n$ is the bounded measurable function defined by $x \mapsto \sup_{n \in \mathbb{N}} f_n(x)$.

Let $\Omega$ be a measurable space. Let $(f_n)_{n \in \mathbb{N}}$ be a sequence of bounded measurable functions in $\text{BoundedMeasurable } \Omega$ and let $g \in \text{BoundedMeasurable } \Omega$. Then $g$ is the least upper bound of the set $\{f_n : n \in \mathbb{N}\}$ if and only if for every $x \in \Omega$, $g(x)$ is the least upper bound of the set of real values $\{f_n(x) : n \in \mathbb{N}\}$ in $\mathbb{R}$. This means that a sequence has a least upper bound $g$ exactly when $g$ is its pointwise supremum.

For a measurable set $s \subseteq \Omega$ with a proof of measurability $h_s$, this definition constructs the indicator function $\mathbb{1}_s: \Omega \to \mathbb{R}$ as an element of the space of bounded measurable functions. The function $\mathbb{1}_s$ is defined to be $1$ if $x \in s$ and $0$ if $x \notin s$.

For a measurable space $\Omega$, let $s \subseteq \Omega$ be a measurable set and let $\mathbb{1}_s$ denote its indicator function in the space of bounded measurable functions. For any point $x \in \Omega$, the value $\mathbb{1}_s(x)$ is equal to $1$ if $x \in s$ and $0$ if $x \notin s$.

For any measurable set $s \subseteq \Omega$ in a measurable space $\Omega$, the indicator function $\mathbb{1}_s$ is non-negative, meaning that for all $x \in \Omega$, $0 \le \mathbb{1}_s(x)$.

Let $s$ be a measurable subset of a measurable space $\Omega$. The indicator function $\mathbb{1}_s$ of the set $s$ satisfies $\mathbb{1}_s \le 1$, where the inequality is defined pointwise as $\mathbb{1}_s(x) \le 1$ for all $x \in \Omega$.

Let $\{s_n\}_{n \in \mathbb{N}}$ be a sequence of pairwise disjoint subsets of a space $\Omega$. For any point $x \in \Omega$, the sum of the indicator functions $\mathbb{1}_{s_n}(x)$ converges to the indicator function of the union of these sets, $\mathbb{1}_{\bigcup_{n \in \mathbb{N}} s_n}(x)$. That is, $$\sum_{n=0}^{\infty} \mathbb{1}_{s_n}(x) = \mathbb{1}_{\bigcup_{n=0}^{\infty} s_n}(x)$$

Let $\Omega$ be a measurable space and $\{s_n\}_{n \in \mathbb{N}}$ be a sequence of pairwise disjoint measurable subsets of $\Omega$. Let $\mathbb{1}_{s_n}$ denote the indicator function of $s_n$ in the space of bounded measurable functions. Then, the indicator function of the union of these sets, $\mathbb{1}_{\bigcup_{n=0}^\infty s_n}$, is the least upper bound (supremum) of the set of partial sums $\left\{ \sum_{n=0}^{N-1} \mathbb{1}_{s_n} \mid N \in \mathbb{N} \right\}$ with respect to the pointwise ordering.

For a bounded measurable function $g: \Omega \to \mathbb{R}$ and natural numbers $N$ and $K$, the staircase function $\text{staircase}(g, N, K)$ is a bounded measurable function defined as the sum of indicator functions of superlevel sets: $$\text{staircase}(g, N, K) = \sum_{k=1}^{NK} \frac{1}{N} \mathbb{1}_{\{x \in \Omega \mid g(x) \ge \frac{k}{N}\}}$$ where $\mathbb{1}_S$ is the indicator function of the set $S$. For a nonnegative function $g$ bounded above by $K$, this construction yields the value $\frac{\lfloor N \cdot g(x) \rfloor}{N}$ at each point $x \in \Omega$.

Let $\Omega$ be a measurable space and $g: \Omega \to \mathbb{R}$ be a bounded measurable function. For any natural numbers $N$ and $K$ where $N > 0$, and any point $x \in \Omega$ such that $0 \le g(x) \le K$, the value of the staircase function $\text{staircase}(g, N, K)$ at $x$ is given by: $$\text{staircase}(g, N, K)(x) = \frac{\lfloor N \cdot g(x) \rfloor}{N}$$ where $\text{staircase}(g, N, K)$ is defined as the sum of indicator functions $\sum_{k=1}^{NK} \frac{1}{N} \mathbb{1}_{\{x \in \Omega \mid g(x) \ge \frac{k}{N}\}}$.

Let $\Omega$ be a measurable space and $g: \Omega \to \mathbb{R}$ be a bounded measurable function. Suppose $g$ is nonnegative and bounded above by a natural number $K$, such that $0 \le g(x) \le K$ for all $x \in \Omega$. For any natural number $N > 0$, the staircase approximation $\text{staircase}(g, N, K)$ satisfies the uniform error bound: $$|g(x) - \text{staircase}(g, N, K)(x)| \le \frac{1}{N}$$ for all $x \in \Omega$.

Let $\Omega$ be a measurable space and $\mu$ be a finite measure on $\Omega$. For any bounded measurable function $f: \Omega \to \mathbb{R}$, it holds that $f$ is integrable with respect to $\mu$.