PhyslibAlpha.Mathematics.Order.PositiveDual.Basic

Let $E$ be an ordered real vector space and let $E \to_{p} \mathbb{R}$ denote the space of positive linear functionals on $E$. This definition provides the scalar multiplication of a positive linear functional $\phi$ by a non-negative real number $c \in \mathbb{R}_{\geq 0}$, such that for any $f \in E$, the result $(c \cdot \phi)(f)$ is given by $c \cdot \phi(f)$.

Let $E$ be an ordered real vector space. For any non-negative real number $c \in \mathbb{R}_{\geq 0}$, any positive linear functional $\phi$ (a linear functional that is non-negative on the positive cone of $E$), and any element $f \in E$, the scalar multiplication of the functional is defined pointwise such that $(c \cdot \phi)(f) = c \cdot \phi(f)$.

For an element $f$ in an ordered real vector space $E$, this function selects an element in $E$ that is greater than or equal to both $f$ and the zero element $0$. Specifically, it satisfies $f \le \text{dominator } f$ and $0 \le \text{dominator } f$.

Let $E$ be an ordered real vector space. For any element $f \in E$, it holds that $f \le \text{dominator}(f)$, where $\text{dominator}(f)$ is defined as an element in $E$ that is greater than or equal to both $f$ and the zero element $0$.

Let $E$ be an ordered real vector space. For any element $f \in E$, its dominator is non-negative, satisfying $0 \le \text{dominator } f$. Here, the dominator of $f$ is an element in $E$ defined to be greater than or equal to both $f$ and the zero element $0$.

For an ordered real vector space $E$, the space of positive linear functionals $E \to_p \mathbb{R}$ is equipped with a partial order. A positive functional $\phi$ is defined to be less than or equal to $\psi$ ($\phi \leq \psi$) if and only if $\phi(f) \leq \psi(f)$ for every element $f$ in the positive cone of $E$ (i.e., for all $f \geq 0$).

Let $E$ be an ordered real vector space. For any two positive linear functionals $\phi, \psi: E \to_p \mathbb{R}$, the inequality $\phi \leq \psi$ holds if and only if for every element $f \in E$ in the positive cone (i.e., $f \geq 0$), the values satisfy $\phi(f) \leq \psi(f)$.

Let $E$ be an ordered real vector space. For any positive linear functional $\phi$ from $E$ to $\mathbb{R}$, it holds that $0 \leq \phi$ under the partial order of positive linear maps.

Let $E$ be an ordered real vector space. For any two positive linear functionals $\phi, \psi$ from $E$ to $\mathbb{R}$, it holds that $\phi \leq \phi + \psi$ under the partial order of positive linear functionals.

Let $E$ be an ordered real vector space. Let $\{\psi_j\}_{j \in \iota}$ be a collection of positive linear functionals from $E$ to $\mathbb{R}$ (denoted as $E \to_p \mathbb{R}$), where $\iota$ is an indexing set. For any finite subset $t \subseteq \iota$ and any index $i \in t$, the functional $\psi_i$ is less than or equal to the sum of the functionals in $t$ under the partial order on positive linear functionals: $$\psi_i \le \sum_{j \in t} \psi_j$$ This means that for all elements $f$ in the positive cone of $E$ ($f \ge 0$), the inequality $\psi_i(f) \le \sum_{j \in t} \psi_j(f)$ holds.

Given an ordered real vector space $E$ and two positive linear functionals $\phi, \psi: E \to \mathbb{R}$ such that $\psi \leq \phi$ (meaning $\psi(f) \leq \phi(f)$ for all $f$ in the positive cone of $E$), this definition constructs the positive linear functional representing their difference $\phi - \psi$. The resulting functional is defined by $(\phi - \psi)(f) = \phi(f) - \psi(f)$ for all $f \in E$, and its positivity is guaranteed by the condition $\psi \leq \phi$.

Let $E$ be an ordered real vector space. Suppose $\phi$ and $\psi$ are positive linear functionals from $E$ to $\mathbb{R}$ such that $\psi \leq \phi$ (meaning $\psi(g) \leq \phi(g)$ for all $g$ in the positive cone of $E$). For any element $f \in E$, the positive linear functional representing their difference $\phi - \psi$ (denoted as `subOfLE φ ψ h`) satisfies: $$(\phi - \psi)(f) = \phi(f) - \psi(f)$$

Let $E$ be an ordered real vector space. For any two positive linear functionals $\phi, \psi: E \to \mathbb{R}$, if $\psi \leq \phi$ (meaning $\psi(f) \leq \phi(f)$ for all $f$ in the positive cone of $E$), then the sum of $\psi$ and the positive linear functional representing the difference $\phi - \psi$ is equal to $\phi$.

For an ordered real vector space $E$ and a function $F$ defined on its positive cone $\{x \in E \mid x \geq 0\}$, the function `coneExt` extends $F$ to the entire space $E$. For any element $f \in E$, it is defined as $F(b) - F(b - f)$, where $b$ is a chosen "dominator" satisfying $b \geq f$ and $b \geq 0$.

Let $E$ be an ordered real vector space and let $F$ be an additive function defined on its positive cone (the set of elements $x \in E$ such that $x \geq 0$). Then the value of $F$ at the zero element is zero, i.e., $F(0) = 0$.

Let $E$ be an ordered real vector space and let $F$ be a function defined on its positive cone $\{x \in E \mid x \geq 0\}$. For any element $f \in E$ and any element $b \in E$ satisfying $b \geq 0$ and $b \geq f$, the extension of $F$ to the whole space $E$, denoted by $\text{coneExt}(F, f)$, is given by: $$\text{coneExt}(F, f) = F(b) - F(b - f)$$ This formula characterizes the extension of $F$ using a "dominator" element $b$ that is greater than or equal to both $f$ and $0$, ensuring that both $b$ and $b - f$ lie within the positive cone where $F$ is defined.

Let $E$ be an ordered real vector space and $F$ be a function defined on its positive cone $\{x \in E \mid x \geq 0\}$. For any element $f \in E$ such that $f \geq 0$, the value of the extension $\text{coneExt}(F)$ at $f$ is equal to the value of the original function $F$ at $f$, i.e., $\text{coneExt}(F)(f) = F(f)$.

Let $E$ be an ordered real vector space and let $F$ be a function defined on its positive cone. The extension of $F$ to the entire space $E$, denoted by $\text{coneExt}_F$, is additive. That is, for any vectors $f, g \in E$, it holds that $\text{coneExt}_F(f + g) = \text{coneExt}_F(f) + \text{coneExt}_F(g)$.

Let $E$ be an ordered real vector space and $F$ be a function defined on its positive cone $\{x \in E \mid x \geq 0\}$. Let $\text{coneExt } F: E \to \mathbb{R}$ denote the extension of $F$ to the entire space $E$. For any element $f \in E$, the extension satisfies $$\text{coneExt } F (-f) = - \text{coneExt } F (f).$$

Let $E$ be an ordered real vector space and let $F$ be a function defined on its positive cone. Let $\text{coneExt } F: E \to \mathbb{R}$ be the extension of $F$ to the entire space $E$. For any positive real scalar $c > 0$ and any vector $f \in E$, the extension satisfies the property $\text{coneExt } F (c \cdot f) = c \cdot \text{coneExt } F(f)$.

Let $E$ be an ordered real vector space and $F$ be a function defined on its positive cone $\{x \in E \mid x \geq 0\}$. Let $\text{coneExt}_F: E \to \mathbb{R}$ denote the extension of $F$ to the entire space $E$. For any scalar $c \in \mathbb{R}$ and any element $f \in E$, the extension satisfies $\text{coneExt}_F(c \cdot f) = c \cdot \text{coneExt}_F(f)$.

Let $E$ be an ordered real vector space. Given a function $F$ defined on the positive cone $\{x \in E \mid x \geq 0\}$, the definition `ofCone` constructs a positive linear functional $\varphi: E \to \mathbb{R}$ by extending $F$ to the entire space. This construction requires $F$ to be nonnegative ($F(x) \geq 0$), additive ($F(x + y) = F(x) + F(y)$), and positively homogeneous ($F(c \cdot x) = c \cdot F(x)$ for $c \geq 0$) on the cone.

Let $E$ be an ordered real vector space and $F$ be a function defined on the positive cone $\{x \in E \mid x \geq 0\}$ that is nonnegative, additive, and positively homogeneous. Let $\text{ofCone}(F)$ be the positive linear functional on $E$ constructed by extending $F$. For any element $f \in E$ in the positive cone (i.e., $f \geq 0$), the value of the extended functional at $f$ matches the original function: $(\text{ofCone}(F))(f) = F(f)$.