PhyslibAlpha.Mathematics.Order.PositiveDual.Bidual

The `bidualSubmodule` is the $\mathbb{R}$-submodule of the space of real-valued functions on the set of positive functionals of an ordered real vector space $E$ (denoted $E \to_p \mathbb{R}$). A function $x: (E \to_p \mathbb{R}) \to \mathbb{R}$ belongs to this submodule if it satisfies the following three conditions: 1. **Additivity**: $x(\phi + \psi) = x(\phi) + x(\psi)$ for all positive functionals $\phi, \psi$. 2. **Positive homogeneity**: $x(c \cdot \phi) = c \cdot x(\phi)$ for all $c \in \mathbb{R}_{\ge 0}$ and positive functionals $\phi$. 3. **Domination**: There exists an element $f \in E$ such that $|x(\phi)| \leq \phi(f)$ for all positive functionals $\phi$.

Let $E$ be an ordered real vector space and let $E \to_p \mathbb{R}$ denote the set of positive linear functionals on $E$. The bidual of $E$, denoted as $\text{Bidual } E$, is defined as the $\mathbb{R}$-submodule of functions $x: (E \to_p \mathbb{R}) \to \mathbb{R}$ that satisfy the following conditions: 1. **Additivity**: $x(\phi + \psi) = x(\phi) + x(\psi)$ for all $\phi, \psi \in E \to_p \mathbb{R}$. 2. **Positive homogeneity**: $x(c \cdot \phi) = c \cdot x(\phi)$ for all $c \in \mathbb{R}_{\ge 0}$ and $\phi \in E \to_p \mathbb{R}$. 3. **Domination**: There exists an element $f \in E$ such that $|x(\phi)| \leq \phi(f)$ for all $\phi \in E \to_p \mathbb{R}$.

The bidual $\text{Bidual } E$ of an ordered real vector space $E$ carries the structure of an additive commutative group, where addition and negation are defined pointwise on the functions from positive linear functionals to $\mathbb{R}$ that constitute the space.

The bidual $\text{Bidual } E$ of an ordered real vector space $E$ carries the structure of a vector space (module) over the real numbers $\mathbb{R}$. The addition and scalar multiplication are defined pointwise, inheriting the module structure from the space of functions $(E \to_p \mathbb{R}) \to \mathbb{R}$.

Let $E$ be an ordered real vector space and let $E \to_p \mathbb{R}$ denote the set of positive linear functionals on $E$. Given a function $x: (E \to_p \mathbb{R}) \to \mathbb{R}$ that satisfies: 1. **Additivity**: $x(\phi + \psi) = x(\phi) + x(\psi)$ for all $\phi, \psi \in E \to_p \mathbb{R}$, 2. **Positive homogeneity**: $x(c \cdot \phi) = c \cdot x(\phi)$ for all $c \in \mathbb{R}_{\ge 0}$ and $\phi \in E \to_p \mathbb{R}$, 3. **Domination**: There exists an element $f \in E$ such that $|x(\phi)| \le \phi(f)$ for all $\phi \in E \to_p \mathbb{R}$, this definition constructs the corresponding element in the bidual $\text{Bidual } E$.

Given an element $x$ of the bidual $\text{Bidual } E$ of an ordered real vector space $E$, this function maps $x$ to its representation as an element of the $\mathbb{R}$-submodule of functions $(E \to_p \mathbb{R}) \to \mathbb{R}$ that are additive, positively homogeneous, and dominated by some element of $E$.

Let $E$ be an ordered real vector space. This instance allows an element $x$ of the bidual $\text{Bidual } E$ to be treated as a function mapping from the set of positive linear functionals $E \to_p \mathbb{R}$ to the real numbers $\mathbb{R}$. Thus, for a positive linear functional $\phi \in E \to_p \mathbb{R}$, the value $x(\phi)$ is defined.

Let $E$ be an ordered real vector space and let $E \to_p \mathbb{R}$ denote the set of positive linear functionals on $E$. Suppose $x: (E \to_p \mathbb{R}) \to \mathbb{R}$ is a function that is additive, positively homogeneous, and dominated by an element of $E$. Then the element of the bidual $\text{Bidual } E$ constructed from $x$ (denoted as $\text{mk } x$), when evaluated at a positive functional $\phi \in E \to_p \mathbb{R}$, is equal to $x(\phi)$.

Let $E$ be an ordered real vector space and $\text{Bidual } E$ be its bidual. For any elements $x, y \in \text{Bidual } E$, if $x(\phi) = y(\phi)$ for every positive linear functional $\phi \in E \to_p \mathbb{R}$, then $x = y$.

Let $E$ be an ordered real vector space and $\text{Bidual } E$ be its bidual. For any element $x \in \text{Bidual } E$ and any two positive linear functionals $\phi, \psi: E \to_p \mathbb{R}$, the function $x$ preserves addition, such that $x(\phi + \psi) = x(\phi) + x(\psi)$.

Let $E$ be an ordered real vector space and $\text{Bidual } E$ be its bidual. For any element $x \in \text{Bidual } E$, any non-negative real number $c \in \mathbb{R}_{\ge 0}$, and any positive linear functional $\phi$ on $E$, the evaluation of $x$ at the scaled functional $c \cdot \phi$ satisfies $x(c \cdot \phi) = c \cdot x(\phi)$.

Let $E$ be an ordered real vector space and $\text{Bidual } E$ denote its bidual. For every element $x \in \text{Bidual } E$, there exists an element $f \in E$ such that for all positive linear functionals $\phi$ on $E$, we have $|x(\phi)| \leq \phi(f)$.

Let $E$ be an ordered real vector space and $\text{Bidual } E$ its bidual. For any element $x \in \text{Bidual } E$ and any $f \in E$, if the condition $|x(\phi)| \leq \phi(f)$ holds for all positive functionals $\phi : E \to_p \mathbb{R}$, then it follows that $0 \leq \phi(f)$ for every such $\phi$.

Let $E$ be an ordered real vector space. For any two elements $x, y$ in the bidual $\text{Bidual } E$ and any positive linear functional $\phi \in E \to_p \mathbb{R}$, the addition in the bidual is defined pointwise such that $(x + y)(\phi) = x(\phi) + y(\phi)$.

Let $E$ be an ordered real vector space and $\text{Bidual } E$ its bidual. For any elements $x, y \in \text{Bidual } E$ and any positive linear functional $\phi \in E \to_p \mathbb{R}$, the evaluation of the difference $x - y$ at $\phi$ satisfies $(x - y)(\phi) = x(\phi) - y(\phi)$.

Let $E$ be an ordered real vector space and $\text{Bidual } E$ its bidual. For any element $x \in \text{Bidual } E$ and any positive linear functional $\phi \in E \to_p \mathbb{R}$, the evaluation of the negated element $-x$ at $\phi$ is equal to the negation of the value of $x$ at $\phi$: $$(-x)(\phi) = -x(\phi)$$

Let $E$ be an ordered real vector space and $\text{Bidual } E$ be its bidual. For any positive linear functional $\phi \in E \to_p \mathbb{R}$, the evaluation of the zero element $0 \in \text{Bidual } E$ at $\phi$ is equal to $0$.

Let $E$ be an ordered real vector space and $\text{Bidual } E$ its bidual. For any scalar $c \in \mathbb{R}$, any element $x \in \text{Bidual } E$, and any positive linear functional $\phi \in E \to_p \mathbb{R}$, the evaluation of the scalar product $c \cdot x$ at $\phi$ is equal to the product of $c$ and the value of $x$ at $\phi$: $$(c \cdot x)(\phi) = c \cdot x(\phi)$$

Let $E$ be an ordered real vector space and let $E \to_p \mathbb{R}$ denote the set of positive linear functionals on $E$. For any element $x$ of the bidual $\text{Bidual } E$, the evaluation of $x$ at the zero functional $0 \in E \to_p \mathbb{R}$ is zero, i.e., $x(0) = 0$.

Let $E$ be an ordered real vector space and $\text{Bidual } E$ be its bidual. For any element $x \in \text{Bidual } E$, any finite set of indices $s$, and any collection of positive functionals $\{\phi_i\}_{i \in s}$ where each $\phi_i \in E \to_p \mathbb{R}$, the value of $x$ applied to the sum of the functionals is equal to the sum of the values of $x$ applied to each functional: $$x\left(\sum_{i \in s} \phi_i\right) = \sum_{i \in s} x(\phi_i)$$

The bidual $\text{Bidual } E$ of an ordered real vector space $E$ is equipped with a partial order defined pointwise. For any two elements $x, y \in \text{Bidual } E$, the relation $x \leq y$ holds if and only if $x(\phi) \leq y(\phi)$ for every positive linear functional $\phi$ on $E$.

Let $E$ be an ordered real vector space and $\text{Bidual } E$ be its bidual. For any two elements $x, y \in \text{Bidual } E$, the relation $x \le y$ holds if and only if $x(\phi) \le y(\phi)$ for every positive linear functional $\phi$ on $E$.

Let $E$ be an ordered real vector space. The bidual space $\text{Bidual } E$, equipped with its pointwise addition and pointwise partial order, forms an ordered additive monoid. Specifically, for any elements $x, y, z \in \text{Bidual } E$, if $x \leq y$, then $x + z \leq y + z$.

Let $E$ be an ordered real vector space. In the bidual $\text{Bidual } E$, scalar multiplication by non-negative real numbers preserves the order relation. Specifically, for any real number $c \ge 0$ and any elements $x, y \in \text{Bidual } E$, if $x \le y$, then $c \cdot x \le c \cdot y$.

Let $E$ be an ordered real vector space. The canonical $\mathbb{R}$-linear map $\text{ofE} : E \to \text{Bidual } E$ sends an element $A \in E$ to the element of the bidual defined by evaluation. Specifically, for any positive linear functional $\phi \in E \to_p \mathbb{R}$, the resulting element of the bidual maps $\phi$ to the value $\phi(A)$.

Let $E$ be an ordered real vector space. For any element $A \in E$ and any positive linear functional $\phi$ on $E$, the canonical map $\text{ofE} : E \to \text{Bidual } E$ satisfies the identity $\text{ofE}(A)(\phi) = \phi(A)$.

Let $E$ be an ordered real vector space. For any elements $A, B \in E$, if $A \leq B$, then $\text{ofE}(A) \leq \text{ofE}(B)$, where $\text{ofE} : E \to \text{Bidual } E$ is the canonical linear map from $E$ to its bidual.

Let $E$ be an ordered real vector space. If $E$ is a directed order, then the bidual $\text{Bidual } E$ is also a directed order. This means that for any two elements $x, y \in \text{Bidual } E$, there exists an element $z \in \text{Bidual } E$ such that $x \leq z$ and $y \leq z$. Specifically, if $x$ is dominated by $f \in E$ and $y$ is dominated by $g \in E$, then the element $\text{ofE}(f + g)$ serves as an upper bound for both $x$ and $y$.

For a positive linear functional $\phi$ on an ordered real vector space $E$ (denoted $\phi \in E \to_p \mathbb{R}$), this function defines a positive linear functional on the bidual $\text{Bidual } E$ by evaluation. Specifically, for an element $x \in \text{Bidual } E$, the functional maps $x$ to its value $x(\phi)$.

Let $E$ be an ordered real vector space. For any positive linear functional $\phi \in E \to_p \mathbb{R}$ and any element $x \in \text{Bidual } E$, the evaluation of $\phi$ on $x$ is defined by applying the function $x$ to $\phi$: $$\text{eval}(\phi)(x) = x(\phi)$$

Let $E$ be an ordered real vector space. For any positive linear functional $\phi : E \to_p \mathbb{R}$ and any element $A \in E$, the evaluation of the extended functional $\text{eval}(\phi)$ at the canonical image $\text{ofE}(A)$ in the bidual is equal to the value of the functional $\phi$ at $A$: $$\text{eval}(\phi)(\text{ofE}(A)) = \phi(A)$$

Let $E$ be an ordered real vector space. For any two positive linear functionals $\phi, \psi$ on $E$ (denoted $\phi, \psi \in E \to_p \mathbb{R}$), if $\phi \leq \psi$, then their extensions to the bidual by evaluation satisfy $\text{eval } \phi \leq \text{eval } \psi$. This theorem states that the extension to the bidual preserves the order of positive functionals.

Let $E$ be an ordered real vector space and $\text{Bidual } E$ its bidual. If a family of elements $\{x_i\}_{i \in I}$ in $\text{Bidual } E$ is bounded above, then for any positive linear functional $\phi$ on $E$ (denoted $\phi \in E \to_p \mathbb{R}$), the set of real values $\{x_i(\phi) \mid i \in I\}$ is bounded above in $\mathbb{R}$.

Let $E$ be an ordered real vector space and let $\text{Bidual } E$ be its bidual. For a directed family of elements $\{x_i\}_{i \in I}$ in $\text{Bidual } E$ that is bounded above, the function $\text{ciSup } \{x_i\}$ is the element of $\text{Bidual } E$ defined by the pointwise supremum of the family. Specifically, for any positive linear functional $\phi$ on $E$, the value of the supremum is given by $(\sup_{i \in I} x_i)(\phi) = \sup_{i \in I} (x_i(\phi))$.

Let $E$ be an ordered real vector space and let $\{x_i\}_{i \in I}$ be a directed family of elements in the bidual $\text{Bidual } E$ that is bounded above. For any positive linear functional $\phi$ on $E$ (denoted $\phi \in E \to_p \mathbb{R}$), the value of the supremum of the family evaluated at $\phi$ is equal to the supremum of the individual values in $\mathbb{R}$: $$(\sup_{i \in I} x_i)(\phi) = \sup_{i \in I} (x_i(\phi))$$

Let $E$ be an ordered real vector space and $\text{Bidual } E$ be its bidual. Let $\{x_i\}_{i \in I}$ be a directed family of elements in $\text{Bidual } E$ that is bounded above. Then the pointwise supremum of this family, denoted by $\sup_{i \in I} x_i$ and defined such that $(\sup_{i \in I} x_i)(\phi) = \sup_{i \in I} (x_i(\phi))$ for every positive linear functional $\phi$ on $E$, is the least upper bound of the range $\{x_i \mid i \in I\}$ in the partial order of $\text{Bidual } E$.