PhyslibAlpha.Mathematics.Order.Freudenthal

Let $G$ be a real vector lattice. For any elements $w, v, v' \in G$ such that $w \ge 0$, $v \ge 0$, and $v \le v'$, if $w$ and $v'$ are disjoint (i.e., their infimum $w \sqcap v'$ is $0$), then $w$ and $v$ are also disjoint ($w \sqcap v = 0$). This confirms that disjointness is preserved when replacing one of the elements with a smaller nonnegative element.

Given an element $u$ in a vector lattice $G$, a collection of elements $\{s_i\}_{i \in \iota}$ indexed by a finite set $\iota$ is a partition of $u$ if: 1. Each element is non-negative, i.e., $s_i \geq 0$ for all $i \in \iota$. 2. The elements are pairwise disjoint, meaning the infimum $s_i \sqcap s_j = 0$ for all $i \neq j$. 3. The sum of the elements equals $u$, i.e., $\sum_{i \in \iota} s_i = u$.

Let $G$ be a vector lattice and $\{s_j\}_{j \in \iota}$ be a partition of an element $u \in G$ indexed by a finite set $\iota$. For any $i \in \iota$, the piece $s_i$ is disjoint from the sum of all other pieces in the partition, meaning their infimum is zero: $$s_i \sqcap \sum_{j \in \iota, j \neq i} s_j = 0$$

Let $u$ be an element of a vector lattice $G$. If $\{s_i\}_{i \in \iota}$ is a partition of $u$ indexed by a finite set $\iota$, then for every $i \in \iota$, the element $s_i$ satisfies $s_i \leq u$.

Let $u$ be an element in a vector lattice $G$. Suppose $\{s_i\}_{i \in \iota}$ is a partition of $u$ (meaning $s_i \geq 0$ for all $i$, $s_i \sqcap s_j = 0$ for $i \neq j$, and $\sum_{i \in \iota} s_i = u$). Then for any index $i \in \iota$, the piece $s_i$ is disjoint from its complement relative to $u$, such that the infimum $s_i \sqcap (u - s_i) = 0$.

Let $G$ be a vector lattice and $u \in G$. Let $e: \mathbb{N} \to G$ be an antitone sequence such that $e_0 = u$ and $e_N = 0$ for some natural number $N$. Suppose that for every $j \in \mathbb{N}$, the following conditions hold: 1. $0 \leq e_j \leq u$, and 2. $e_j \sqcap (u - e_j) = 0$ (meaning each $e_j$ is a component of $u$). Then the sequence of differences $s_j = e_j - e_{j+1}$ for $j \in \{0, 1, \dots, N-1\}$ forms a partition of $u$. (A partition of $u$ consists of a finite collection of non-negative, pairwise disjoint elements whose sum is $u$.)

Let $G$ be a real vector lattice and $u$ be an element in $G$. Let $\{s_i\}_{i \in \iota}$ and $\{t_j\}_{j \in \kappa}$ be two partitions of $u$ indexed by finite sets $\iota$ and $\kappa$, respectively. Then the collection of pairwise infima $\{s_i \sqcap t_j\}_{(i, j) \in \iota \times \kappa}$ is also a partition of $u$. Here, a collection of elements is a partition of $u$ if they are non-negative, pairwise disjoint (their infimum is zero), and their sum equals $u$.

Let $G$ be a real vector lattice and $u$ be an element in $G$. Suppose $\{s_i\}_{i \in \iota}$ is a partition of $u$ indexed by a finite set $\iota$, meaning that $s_i \geq 0$ for all $i$, $s_i \sqcap s_j = 0$ for $i \neq j$, and $\sum_{i \in \iota} s_i = u$. For any finite set $\kappa$ and any bijection $e : \kappa \simeq \iota$, the reindexed collection $\{s_{e(k)}\}_{k \in \kappa}$ is also a partition of $u$.

Let $G$ be a real vector lattice and $u \in G$ be an element. Suppose $\{s_i\}_{i \in \iota}$ is a partition of $u$ indexed by a finite set $\iota$ (meaning $s_i \ge 0$, $s_i \sqcap s_j = 0$ for $i \neq j$, and $\sum_{i \in \iota} s_i = u$). For any non-negative element $x \in G$ and any non-negative real number $M \geq 0$, the following identity holds: $$x \sqcap (M \cdot u) = \sum_{i \in \iota} (x \sqcap (M \cdot s_i))$$ where $\sqcap$ denotes the infimum operation in the vector lattice.

Let $G$ be a real vector lattice and $\{s_i\}_{i \in \iota}$ be a partition of an element $u \in G$ indexed by a finite set $\iota$. For any collection of real coefficients $c_i$ and a real number $\varepsilon$, if $c_i \leq \varepsilon$ for all $i$ such that $s_i \neq 0$, then it holds that $$\sum_{i \in \iota} c_i s_i \leq \varepsilon u.$$ A partition of $u$ is defined as a set of non-negative, pairwise disjoint elements that sum to $u$.

Let $u$ be an element in a real vector lattice $G$ and let $\{s_i\}_{i \in \iota}$ be a partition of $u$ indexed by a finite set $\iota$ (meaning $s_i \ge 0$, the elements are pairwise disjoint, and $\sum_{i \in \iota} s_i = u$). For any real number $\epsilon$ and any set of real coefficients $\{c_i\}_{i \in \iota}$, if $c_i \ge \epsilon$ for every $i$ such that $s_i \neq 0$, then it holds that $$\epsilon \cdot u \le \sum_{i \in \iota} c_i \cdot s_i.$$

Let $G$ be a real vector lattice and let $\{s_j\}_{j \in \iota}$ be a finite partition of an element $u \in G$ (meaning $s_j \geq 0$, the elements are pairwise disjoint, and $\sum_{j \in \iota} s_j = u$). For any element $x \in G$ and any set of real coefficients $\{b_j\}_{j \in \iota}$, the following inequality holds for any index $i \in \iota$: $$x - \sum_{j \in \iota} b_j s_j \leq (x - b_i u)^+ + \sum_{j \neq i} |b_i - b_j| s_j$$ where $(\cdot)^+$ denotes the positive part of an element in the lattice. This bound indicates that the difference between $x$ and its step function approximation is bounded by the positive part of the difference from a specific level $b_i$ plus the weighted sum of level variations on the other pieces of the partition.

Let $G$ be a real vector lattice and $\{s_j\}_{j \in \iota}$ be a partition of an element in $G$ indexed by a finite set $\iota$. For any collection of non-negative real coefficients $\{c_j\}_{j \in \iota}$, any specific index $i \in \iota$, and any non-negative real number $M$, it holds that $$\left( \sum_{j \in \iota \setminus \{i\}} c_j s_j \right) \sqcap (M s_i) = 0,$$ where $\sqcap$ denotes the infimum (greatest lower bound) in the lattice.

Let $G$ be a real vector lattice and $\{s_i\}_{i \in \iota}$ be a partition of an element $u \in G$ (that is, $s_i \geq 0$, $s_i \sqcap s_j = 0$ for $i \neq j$, and $\sum_{i \in \iota} s_i = u$). Let $x \in G$ and $b: \iota \to \mathbb{R}$ be a collection of coefficients. If for every $i \in \iota$, the positive part of $x - b_i u$ is disjoint from $s_i$ (i.e., $(x - b_i u)^+ \sqcap s_i = 0$), then for any $i \in \iota$ and any non-negative real number $M \geq 0$, the positive part of the difference between $x$ and the step function $\sum_{j \in \iota} b_j s_j$ is disjoint from $M s_i$: $$(x - \sum_{j \in \iota} b_j s_j)^+ \sqcap (M s_i) = 0.$$

Let $G$ be a real vector lattice and let $u \in G$ be a strong unit. Suppose $\{s_i\}_{i \in \iota}$ is a finite partition of $u$, meaning $s_i \geq 0$, $s_i \sqcap s_j = 0$ for $i \neq j$, and $\sum_{i \in \iota} s_i = u$. For any element $x \in G$ and real coefficients $b_i$, if $x$ is locally bounded by $b_i$ on each piece $s_i$ in the sense that $(x - b_i \cdot u)^+ \sqcap s_i = 0$ for all $i \in \iota$, then $x$ is globally bounded by the corresponding step function: $$x \le \sum_{i \in \iota} b_i \cdot s_i$$ where $(\cdot)^+$ denotes the positive part and $\sqcap$ denotes the infimum in the vector lattice.

Let $G$ be a real vector lattice and $u \in G$ be a strong unit. Suppose $\{s_i\}_{i \in \iota}$ is a partition of $u$ indexed by a finite set $\iota$. For any element $x \in G$ and any scalars $a_i \in \mathbb{R}$, if for every $i \in \iota$ the condition $(a_i u - x)^+ \sqcap s_i = 0$ holds, then $$\sum_{i \in \iota} a_i s_i \le x$$ where $(y)^+ = y \vee 0$ denotes the positive part of $y$ and $\sqcap$ denotes the infimum (meet) in the lattice. This theorem expresses that if $x$ is locally bounded below by $a_i$ on each piece $s_i$ of the partition, then $x$ is globally bounded below by the step function formed by these values.

In a vector lattice $G$ with a fixed element $u$, the property `HasMonotoneSups` holds if every monotonically increasing sequence $(a_n)_{n \in \mathbb{N}}$ that is bounded above by $u$ (i.e., $a_n \le u$ for all $n$) has a least upper bound (supremum) $c = \sup_{n \in \mathbb{N}} a_n$ in $G$.

In a real vector lattice $G$ with a fixed nonnegative element $u$, for any element $y \in G$, the sequence defined by $n \mapsto (n \cdot y^+) \wedge u$ for $n \in \mathbb{N}$ is monotone (non-decreasing). Here $y^+ = y \vee 0$ denotes the positive part of $y$, and $\wedge$ denotes the infimum (meet) operation in the lattice.

In a real vector lattice $G$ with a fixed nonnegative element $u$, if every monotone sequence bounded by $u$ has a least upper bound, then for any element $y \in G$, the set $\{ (n \cdot y^+) \wedge u \mid n \in \mathbb{N} \}$ has a least upper bound in $G$. Here $y^+ = y \vee 0$ denotes the positive part of $y$ and $\wedge$ denotes the infimum operation in the lattice.

In a real vector lattice $G$ with a fixed nonnegative element $u$, assuming that every monotone sequence bounded above by $u$ has a least upper bound, the function maps an element $y \in G$ to its support, defined as the supremum (least upper bound) $\sup_{n \in \mathbb{N}} (n \cdot y^+ \wedge u)$. Here $y^+ = y \vee 0$ is the positive part of $y$, and $\wedge$ denotes the infimum (meet) operation in the lattice. This element represents the part of $u$ where $y$ is positive.

Let $G$ be a real vector lattice with a fixed nonnegative element $u$. Assume that $G$ satisfies the property that every monotonically increasing sequence bounded by $u$ has a least upper bound. For any element $y \in G$, let $y^+ = y \vee 0$ denote its positive part. The support of $y$, denoted as $\text{support}(y)$, is the least upper bound (supremum) of the set $\{ (n \cdot y^+) \wedge u \mid n \in \mathbb{N} \}$, where $\wedge$ denotes the infimum operation in the lattice.

Let $G$ be a real vector lattice with a fixed nonnegative element $u$, such that every monotone sequence bounded above by $u$ has a supremum. For any element $y \in G$ and any natural number $n$, the element $(n \cdot y^+) \wedge u$ is less than or equal to the support of $y$, where $y^+ = y \vee 0$ is the positive part of $y$ and $\text{support}(y)$ is defined as $\sup_{k \in \mathbb{N}} (k \cdot y^+ \wedge u)$.

Let $G$ be a real vector lattice and $u \in G$ be a fixed nonnegative element. Suppose that every monotonically increasing sequence in $G$ that is bounded above by $u$ has a least upper bound. For any element $y \in G$, its support, defined as $\text{support}(y) = \sup_{n \in \mathbb{N}} (n \cdot y^+ \wedge u)$, satisfies $\text{support}(y) \le u$.

Let $G$ be a real vector lattice with a fixed element $u$. Assume that every monotonically increasing sequence in $G$ bounded above by $u$ has a supremum. For any elements $y, y' \in G$, if $y \leq y'$, then their supports satisfy $\text{support}(y) \leq \text{support}(y')$, where the support is defined as $\text{support}(y) = \sup_{n \in \mathbb{N}} (n \cdot y^+ \wedge u)$.

Let $G$ be a real vector lattice with a fixed nonnegative element $u$. Assume that every monotonically increasing sequence in $G$ bounded above by $u$ has a least upper bound. For any element $y \in G$, its support, defined as $\text{support}(y) = \sup_{n \in \mathbb{N}} (n y^+ \wedge u)$, satisfies $0 \le \text{support}(y)$.

Let $G$ be a real vector lattice and let $u \in G$ be a fixed nonnegative element. Assume that every monotonically increasing sequence in $G$ that is bounded above by $u$ has a least upper bound (supremum). For any element $y \in G$, its support relative to $u$ is defined as $\text{support}(y) = \sup_{n \in \mathbb{N}} (n y^+ \wedge u)$. This support is a component of $u$, meaning it is disjoint from its complement relative to $u$: $$\text{support}(y) \wedge (u - \text{support}(y)) = 0$$ where $\wedge$ denotes the infimum (meet) operation in the lattice.

Let $G$ be a real vector lattice and $u$ a fixed nonnegative element such that every monotonically increasing sequence in $G$ bounded above by $u$ has a least upper bound. For any elements $w, y \in G$ where $w$ is nonnegative ($0 \leq w$), if $w$ is disjoint from the positive part $y^+ = y \vee 0$ (that is, $w \wedge y^+ = 0$), then $w$ is also disjoint from the support of $y$. Here, the support is defined as $\text{support}(y) = \sup_{n \in \mathbb{N}} (n \cdot y^+ \wedge u)$, and $\wedge$ denotes the infimum operation.

Let $G$ be a real vector lattice and $u \in G$ be a fixed nonnegative element (a strong unit). Suppose that $G$ has the property that every monotonically increasing sequence bounded above by $u$ has a least upper bound. For any $y \in G$, let $y^+ = \max(y, 0)$ denote its positive part and let $\text{support}(y) = \sup_{n \in \mathbb{N}} (n y^+ \wedge u)$ denote the support of $y$ relative to $u$. Then the positive part $y^+$ is disjoint from the complement of the support of $y$ relative to $u$: $$y^+ \wedge (u - \text{support}(y)) = 0$$ where $\wedge$ denotes the infimum (meet) operation in the lattice.

In a real vector lattice $G$ with a fixed nonnegative element $u$, where every monotone sequence bounded above by $u$ has a least upper bound, let the support of an element $y \in G$ be defined as $\sup_{n \in \mathbb{N}} (n \cdot y^+ \wedge u)$. If $y \le 0$, then the support of $y$ is $0$.

Let $G$ be a real vector lattice and let $u \in G$ be a nonnegative element. Suppose that every monotonically increasing sequence in $G$ that is bounded above by $u$ has a least upper bound. For any element $y \in G$, if $u \le y$, then the support of $y$ relative to $u$, defined as $\text{support}(y) = \sup_{n \in \mathbb{N}} (n y^+ \wedge u)$, is equal to $u$.

In a real vector lattice $G$ with a fixed nonnegative element $u$, assume that every monotonically increasing sequence bounded above by $u$ has a least upper bound. For any element $x \in G$ and any real number $a$, let $y^+ = y \vee 0$ denote the positive part of $y$ and let $\text{support}(y) = \sup_{n \in \mathbb{N}} (n y^+ \wedge u)$ denote the support of $y$ relative to $u$. Then the positive part of $a u - x$ and the support of $x - a u$ are disjoint: $$(a u - x)^+ \wedge \text{support}(x - a u) = 0$$ where $\wedge$ denotes the infimum (meet) operation in the lattice.

In a real vector lattice $G$ with a fixed strong unit $u$, for a given element $x \in G$, a base level $L \in \mathbb{R}$, and a step size $\delta \in \mathbb{R}$, this function maps a natural number $j$ to the support of $x - (L + j \delta) \cdot u$. Specifically, it is defined as $\text{support}(x - (L + j \delta) \cdot u) = \sup_{n \in \mathbb{N}} (n(x - (L + j \delta) \cdot u)^+ \wedge u)$, which represents the component of $u$ on which $x$ exceeds the $j$-th level $L + j \delta$.

In a real vector lattice $G$ with a fixed nonnegative element $u$, assume that every monotonically increasing sequence in $G$ bounded above by $u$ has a least upper bound. For any element $x \in G$, real number $L$, and step size $\delta \ge 0$, let $S(j) = \text{support}(x - (L + j \delta) \cdot u)$ be the component of $u$ on which $x$ exceeds the level $L + j\delta$. Then the mapping $j \mapsto S(j)$ is antitone; that is, for any natural numbers $j$ and $k$, if $j \le k$, then $S(k) \le S(j)$.

In a real vector lattice $G$ with an element $u$ satisfying the property that every monotone increasing sequence bounded by $u$ has a supremum, let $x \in G$ be an element, $L \in \mathbb{R}$ be a base level, and $\delta \in \mathbb{R}$ be a step size. For a natural number $N$, let $w_j = \text{levelSupport}(x, L, \delta, j)$ denote the support of $x$ exceeding the level $L + j\delta$, defined as $\sup_{n \in \mathbb{N}} (n(x - (L + j\delta) \cdot u)^+ \wedge u)$. If $u \leq x - L \cdot u$ and $x \leq (L + N\delta) \cdot u$, then the collection of elements $\{s_j\}_{j=0}^{N-1}$ defined by the differences $s_j = w_j - w_{j+1}$ constitutes a partition of $u$.

Let $G$ be a real vector lattice and $u \in G$ be a fixed element. Suppose $G$ satisfies the property that every monotone increasing sequence bounded above by $u$ has a supremum. For an element $x \in G$, a base level $L \in \mathbb{R}$, and a step size $\delta \in \mathbb{R}$, let $S_j$ denote the level support of $x$ at level $L + j\delta$ (the component of $u$ on which $x$ exceeds $L + j\delta$). For any natural number $j$, the element $x$ is bounded between the levels $L + j\delta$ and $L + (j+1)\delta$ on the piece $S_j - S_{j+1}$ in the sense that: $$(x - (L + (j + 1)\delta) \cdot u)^+ \sqcap (S_j - S_{j+1}) = 0 \quad \text{and} \quad ((L + j\delta) \cdot u - x)^+ \sqcap (S_j - S_{j+1}) = 0$$ where $(\cdot)^+$ denotes the positive part and $\sqcap$ denotes the infimum in the lattice.

Let $G$ be a real vector lattice and $u \in G$ be a non-negative strong unit (meaning for every $x \in G$, there exists $n \in \mathbb{N}$ such that $x \le n \cdot u$). Assume that $G$ satisfies the property that every monotone increasing sequence bounded above by $u$ has a supremum in $G$. For any element $x \in G$ and any real number $\delta > 0$, there exists a natural number $N$, a partition $\{s_j\}_{j=1}^N$ of $u$, and real numbers $\{a_j\}_{j=1}^N$ such that for each $j$, the following conditions hold: $$(x - (a_j + \delta) \cdot u)^+ \sqcap s_j = 0 \quad \text{and} \quad (a_j \cdot u - x)^+ \sqcap s_j = 0$$ where $(y)^+$ denotes the positive part $y \sqcup 0$ and $\sqcap$ denotes the infimum in the lattice. These conditions imply that on each piece $s_j$ of the partition, $x$ is bounded between $a_j \cdot u$ and $(a_j + \delta) \cdot u$.

Let $G$ be a real vector lattice and $u \in G$. For any elements $x, c, c' \in G$ and real numbers $a, \delta \in \mathbb{R}$, suppose $0 \leq c \leq c'$. If $x$ satisfies the approximation bounds on $c'$ defined by $(x - (a + \delta) \cdot u)^+ \sqcap c' = 0$ and $(a \cdot u - x)^+ \sqcap c' = 0$, then $x$ also satisfies the same bounds on $c$, namely $(x - (a + \delta) \cdot u)^+ \sqcap c = 0$ and $(a \cdot u - x)^+ \sqcap c = 0$.

Let $G$ be a real vector lattice and $u \in G$ be a non-negative element ($u \ge 0$). Suppose $u$ is a **strong unit** (for every $x \in G$, there exists $n \in \mathbb{N}$ such that $x \le n \cdot u$) and that $G$ satisfies the **monotone supremum property** with respect to $u$ (every monotonically increasing sequence bounded above by $u$ has a least upper bound in $G$). For any finite collection of elements $\{x_k\}_{k=1}^n$ in $G$ and any real $\delta > 0$, there exists a natural number $m$, a partition $\{s_i\}_{i=1}^m$ of $u$, and real coefficients $a_{ik}$ (for $1 \le i \le m$ and $1 \le k \le n$) such that for all $i$ and $k$: $$(x_k - (a_{ik} + \delta) \cdot u)^+ \sqcap s_i = 0 \quad \text{and} \quad (a_{ik} \cdot u - x_k)^+ \sqcap s_i = 0$$ Here, $y^+ = \sup(y, 0)$ denotes the positive part of an element, $\sqcap$ denotes the infimum, and a collection $\{s_i\}$ is a **partition** of $u$ if $s_i \ge 0$ for all $i$, $s_i \sqcap s_j = 0$ for $i \neq j$, and $\sum_{i=1}^m s_i = u$.