PhyslibAlpha.Mathematics.Order.PositiveDual.UpperEnvelope

Given a family of elements $\{s_i\}_{i \in \iota}$ in a directed ordered real vector space $E$ and a positive linear functional $\alpha: E \to \mathbb{R}$, the **upper envelope** of the family at $\alpha$ is the infimum of the values $\alpha(b)$ over all common upper bounds $b \in E$ of the family. That is, $$\inf \{ \alpha(b) \mid b \in E, \forall i \in \iota, s_i \leq b \}.$$ According to the Hahn-Banach theorem, for a finite family, this value is attained by some splitting of the functional $\alpha$.

Let $E$ be a directed ordered real vector space. For any finite family of elements $\{s_i\}_{i \in \iota}$ in $E$, the set of upper bounds of the range of $s$ is non-empty.

Let $E$ be a directed ordered real vector space, $\iota$ a non-empty index set, and $\{s_i\}_{i \in \iota}$ a family of elements in $E$. For any positive linear functional $\alpha : E \to \mathbb{R}$ and any common upper bound $b \in E$ of the family $\{s_i\}_{i \in \iota}$ (meaning $s_i \leq b$ for all $i \in \iota$), the upper envelope of the family at $\alpha$ is less than or equal to $\alpha(b)$: $$\text{upperEnvelope}(s, \alpha) \leq \alpha(b).$$

Let $E$ be a directed ordered real vector space and $\{s_i\}_{i \in \iota}$ be a family of elements in $E$. Let $\alpha: E \to \mathbb{R}$ be a positive linear functional and $r$ be a real number. If $r \leq \alpha(b)$ for every common upper bound $b \in E$ of the family $\{s_i\}$ (i.e., for every $b$ such that $s_i \leq b$ for all $i \in \iota$), then $r$ is less than or equal to the upper envelope of the family $\{s_i\}$ at $\alpha$.

Let $E$ be a directed ordered real vector space and $\alpha: E \to \mathbb{R}$ be a positive linear functional. For a family of elements $\{s_i\}_{i \in \iota}$ in $E$, the upper envelope at $\alpha$ is defined as the infimum of the values $\alpha(b)$ over all common upper bounds $b$ of the family. If this upper envelope is strictly less than a real number $r$, then there exists a common upper bound $b \in E$ for the family (satisfying $s_i \leq b$ for all $i \in \iota$) such that $\alpha(b) < r$.

Let $E$ be an ordered vector space and $\iota$ be an index set. Let $c, c' : \iota \to E$ be families of elements in $E$. If $b \in E$ is an upper bound for the range of $c$ (i.e., $c_i \le b$ for all $i \in \iota$) and $b' \in E$ is an upper bound for the range of $c'$ (i.e., $c'_i \le b'$ for all $i \in \iota$), then $b + b'$ is an upper bound for the range of the pointwise sum family $c + c'$, where $(c + c')_i = c_i + c'_i$.

Let $E$ be an ordered real vector space. If $b \in E$ is an upper bound for the range of a family of elements $c: \iota \to E$, then for any non-negative real number $t \ge 0$, the scalar product $t \cdot b$ is an upper bound for the range of the scaled family $t \cdot c$.

Let $E$ be a directed ordered real vector space and $\alpha: E \to \mathbb{R}$ be a positive linear functional. Given two families of elements $c, c' : \iota \to E$, let $c + c'$ denote the pointwise sum family defined by $(c + c')_i = c_i + c'_i$ for all $i \in \iota$. The upper envelope of the sum family at $\alpha$ is less than or equal to the sum of the individual upper envelopes of $c$ and $c'$ at $\alpha$: $$\text{upperEnvelope}(c + c', \alpha) \le \text{upperEnvelope}(c, \alpha) + \text{upperEnvelope}(c', \alpha).$$

Let $E$ be a directed ordered real vector space and $\alpha: E \to \mathbb{R}$ be a positive linear functional. For any family of elements $c: \iota \to E$ and any positive real number $t > 0$, the upper envelope of the scaled family $t \cdot c$ at $\alpha$ is equal to $t$ times the upper envelope of the family $c$ at $\alpha$. That is, $$\text{upperEnvelope}(t \cdot c, \alpha) = t \cdot \text{upperEnvelope}(c, \alpha).$$

Let $E$ be a directed ordered real vector space and $\alpha: E \to \mathbb{R}$ be a positive linear functional. For any element $x \in E$, the upper envelope of the constant family $s$ (where $s_i = x$ for all $i \in \iota$) at $\alpha$ is less than or equal to $\alpha(x)$.

Let $E$ be a directed ordered real vector space and $\alpha: E \to \mathbb{R}$ be a positive linear functional. Let $\{s_j\}_{j \in \iota}$ be a family of elements in $E$ defined such that for a fixed index $i \in \iota$, $s_i = x$ and $s_j = 0$ for all $j \neq i$. If $x \leq 0$, then the upper envelope of this family at $\alpha$ is less than or equal to $0$: $$\text{upperEnvelope}(\{s_j\}_{j \in \iota}, \alpha) \leq 0.$$ Here, the upper envelope of a family at a positive functional $\alpha$ is the infimum of $\alpha(b)$ over all common upper bounds $b \in E$ of the family.

Let $E$ be a directed ordered real vector space and $\{s_i\}_{i \in \iota}$ be a finite family of elements in $E$. Let $\alpha: E \to \mathbb{R}$ be a positive linear functional. If $\{\psi_i\}_{i \in \iota}$ is a collection of positive linear functionals such that $\sum_{i \in \iota} \psi_i = \alpha$, then the sum of the evaluations of each piece on its corresponding element is bounded by the upper envelope of the family at $\alpha$: $$\sum_{i \in \iota} \psi_i(s_i) \leq \text{upperEnvelope}(s, \alpha)$$ where $\text{upperEnvelope}(s, \alpha) = \inf \{ \alpha(b) \mid b \in E, \forall i \in \iota, s_i \leq b \}$.

Given a directed ordered real vector space $E$, an index set $\iota$, and a positive linear functional $\alpha: E \to \mathbb{R}$, let $g: E^\iota \to \mathbb{R}$ be a linear map such that for every family of elements $\{c_j\}_{j \in \iota} \in E^\iota$, the value $g(\{c_j\})$ is less than or equal to the upper envelope of the family at $\alpha$. For a specific index $i \in \iota$, the function **piece** defines a positive linear functional $\psi_i: E \to \mathbb{R}$ by evaluating $g$ on the family where the $i$-th component is $x \in E$ and all other components are zero. That is, $\psi_i(x) = g(\delta_i(x))$, where $\delta_i(x)_j = x$ if $j = i$ and $0$ otherwise.

Let $E$ be a directed ordered real vector space, $\iota$ be a finite index set, and $\alpha: E \to \mathbb{R}$ be a positive linear functional. Let $g: E^\iota \to \mathbb{R}$ be a linear map such that for every family of elements $c = \{c_j\}_{j \in \iota} \in E^\iota$, the value $g(c)$ is bounded by the upper envelope of the family at $\alpha$: $$g(c) \leq \text{upperEnvelope}(c, \alpha)$$ where $\text{upperEnvelope}(c, \alpha) = \inf \{ \alpha(b) \mid b \in E, \forall i \in \iota, c_i \leq b \}$. If $\psi_i: E \to \mathbb{R}$ is the $i$-th component positive linear functional defined by evaluating $g$ on the family where the $i$-th component is $x$ and all other components are zero (i.e., $\psi_i(x) = g(\delta_i(x))$), then the sum of these component functionals equals $\alpha$: $$\sum_{i \in \iota} \psi_i = \alpha$$

Let $E$ be a directed ordered real vector space and $\alpha: E \to \mathbb{R}$ be a positive linear functional. For a finite family of elements $\{s_i\}_{i \in \iota}$ in $E$, there exists a family of positive linear functionals $\{\psi_i\}_{i \in \iota}$ such that $\sum_{i \in \iota} \psi_i = \alpha$ and $$\sum_{i \in \iota} \psi_i(s_i) = \inf \{ \alpha(b) \mid b \in E, \forall i \in \iota, s_i \leq b \}.$$ The value on the right-hand side is known as the **upper envelope** of the family $\{s_i\}$ at the functional $\alpha$, representing the minimum value of $\alpha$ over all common upper bounds of the elements $s_i$.